let i1, i2, i3 be Integer; :: thesis: for G being Group
for a, b, c being Element of G holds <*a,b,c*> |^ <*(@ i1),(@ i2),(@ i3)*> = <*(a |^ i1),(b |^ i2),(c |^ i3)*>
let G be Group; :: thesis: for a, b, c being Element of G holds <*a,b,c*> |^ <*(@ i1),(@ i2),(@ i3)*> = <*(a |^ i1),(b |^ i2),(c |^ i3)*>
let a, b, c be Element of G; :: thesis: <*a,b,c*> |^ <*(@ i1),(@ i2),(@ i3)*> = <*(a |^ i1),(b |^ i2),(c |^ i3)*>
A1: ( len <*(@ i1)*> = 1 & len <*(@ i2),(@ i3)*> = 2 ) by FINSEQ_1:39, FINSEQ_1:44;
A2: ( <*a,b,c*> = <*a*> ^ <*b,c*> & <*(@ i1),(@ i2),(@ i3)*> = <*(@ i1)*> ^ <*(@ i2),(@ i3)*> ) by FINSEQ_1:43;
( len <*a*> = 1 & len <*b,c*> = 2 ) by FINSEQ_1:39, FINSEQ_1:44;
hence <*a,b,c*> |^ <*(@ i1),(@ i2),(@ i3)*> = (<*a*> |^ <*(@ i1)*>) ^ (<*b,c*> |^ <*(@ i2),(@ i3)*>) by A1, A2, Th19
.= <*(a |^ i1)*> ^ (<*b,c*> |^ <*(@ i2),(@ i3)*>) by Th22
.= <*(a |^ i1)*> ^ <*(b |^ i2),(c |^ i3)*> by Th23
.= <*(a |^ i1),(b |^ i2),(c |^ i3)*> by FINSEQ_1:43 ;
:: thesis: verum