let i, j be Integer; :: thesis: for G being Group
for a, b being Element of G holds <*a,b*> |^ <*(@ i),(@ j)*> = <*(a |^ i),(b |^ j)*>
let G be Group; :: thesis: for a, b being Element of G holds <*a,b*> |^ <*(@ i),(@ j)*> = <*(a |^ i),(b |^ j)*>
let a, b be Element of G; :: thesis: <*a,b*> |^ <*(@ i),(@ j)*> = <*(a |^ i),(b |^ j)*>
( len <*a*> = 1 & len <*b*> = 1 & len <*(@ i)*> = 1 & len <*(@ j)*> = 1 & <*a,b*> = <*a*> ^ <*b*> & <*(@ i),(@ j)*> = <*(@ i)*> ^ <*(@ j)*> ) by FINSEQ_1:56, FINSEQ_1:def 9;
hence <*a,b*> |^ <*(@ i),(@ j)*> = (<*a*> |^ <*(@ i)*>) ^ (<*b*> |^ <*(@ j)*>) by Th25
.= <*(a |^ i)*> ^ (<*b*> |^ <*(@ j)*>) by Th28
.= <*(a |^ i)*> ^ <*(b |^ j)*> by Th28
.= <*(a |^ i),(b |^ j)*> by FINSEQ_1:def 9 ;
:: thesis: verum