let i1, i2, i3 be Integer; 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; 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; <*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
;
verum