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)*>
( len <*a*> = 1 & len <*b,c*> = 2 & len <*(@ i1)*> = 1 & len <*(@ i2),(@ i3)*> = 2 & <*a,b,c*> = <*a*> ^ <*b,c*> & <*(@ i1),(@ i2),(@ i3)*> = <*(@ i1)*> ^ <*(@ i2),(@ i3)*> ) by FINSEQ_1:56, FINSEQ_1:60, FINSEQ_1:61;
hence <*a,b,c*> |^ <*(@ i1),(@ i2),(@ i3)*> = (<*a*> |^ <*(@ i1)*>) ^ (<*b,c*> |^ <*(@ i2),(@ i3)*>) by Th25
.= <*(a |^ i1)*> ^ (<*b,c*> |^ <*(@ i2),(@ i3)*>) by Th28
.= <*(a |^ i1)*> ^ <*(b |^ i2),(c |^ i3)*> by Th29
.= <*(a |^ i1),(b |^ i2),(c |^ i3)*> by FINSEQ_1:60 ;
:: thesis: verum