I tried to figure out the proof of insertion operation in AVL-tree is O(log n), but I do not know how. I also tried to find it somewhere on the Internet, but I could not find any good results. Do you guys have any ideas how do we proof that?
Interesting question. For a better theoretical understanding of the whole theory I would suggest you to re-read "Introduction to Algorithms, Third Edition, Cormen" Chapter 12 (Trees) and Chapter 13 (Red-Black Trees). Since it is stated there that (page 311):
As an immediate consequence of this lemma, we can implement the dynamic-set operations SEARCH , MINIMUM , MAXIMUM , SUCCESSOR , and PREDECESSOR in $O(\log n)$ time on red-black trees, since each can run in $O(h)$ time on a binary search tree of height $h$ (as shown in Chapter 12) and any red-black tree on n nodes is a binary search tree with height $O(\log n)$.
Red-Black trees do not differ from AVL-trees from a strict computational point of view: https://www.geeksforgeeks.org/red-black-tree-vs-avl-tree/. An AVL tree is a subset of a Red-Black tree: http://discuss.fogcreek.com/joelonsoftware/default.asp?cmd=show&ixPost=22948. So from a theoretical point of view, you can map them together (computational-complexity wise).
Regarding a pure understanding of why the INSERTION is $O(\log n)$, check this implementation example. There you can clearly see that what makes an AVL differ from a standard BST are the rotations, that can be performed in constant time. With those you get a balanced tree, and with a balanced tree you get $O(\log n)$ INSERTION.