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)*>
A1: ( len <*(@ i)*> = 1 & len <*(@ j)*> = 1 ) by FINSEQ_1:39;
A2: ( <*a,b*> = <*a*> ^ <*b*> & <*(@ i),(@ j)*> = <*(@ i)*> ^ <*(@ j)*> ) by FINSEQ_1:def 9;
( len <*a*> = 1 & len <*b*> = 1 ) by FINSEQ_1:39;
hence <*a,b*> |^ <*(@ i),(@ j)*> = (<*a*> |^ <*(@ i)*>) ^ (<*b*> |^ <*(@ j)*>) by A1, A2, Th19
.= <*(a |^ i)*> ^ (<*b*> |^ <*(@ j)*>) by Th22
.= <*(a |^ i)*> ^ <*(b |^ j)*> by Th22
.= <*(a |^ i),(b |^ j)*> by FINSEQ_1:def 9 ;
:: thesis: verum