let i, j be Integer; for G being Group
for a, b being Element of G holds <*a,b*> |^ <*(@ i),(@ j)*> = <*(a |^ i),(b |^ j)*>
let G be Group; for a, b being Element of G holds <*a,b*> |^ <*(@ i),(@ j)*> = <*(a |^ i),(b |^ j)*>
let a, b be Element of G; <*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
;
verum