let G be Group; :: thesis: for a, b being Element of G holds <*a*> |^ b = <*(a |^ b)*>

let a, b be Element of G; :: thesis: <*a*> |^ b = <*(a |^ b)*>

.= len <*a*> by FINSEQ_1:39 ;

hence <*a*> |^ b = <*(a |^ b)*> by A1, Def1; :: thesis: verum

let a, b be Element of G; :: thesis: <*a*> |^ b = <*(a |^ b)*>

A1: now :: thesis: for k being Nat st k in dom <*a*> holds

<*(a |^ b)*> . k = (<*a*> /. k) |^ b

len <*(a |^ b)*> =
1
by FINSEQ_1:40
<*(a |^ b)*> . k = (<*a*> /. k) |^ b

let k be Nat; :: thesis: ( k in dom <*a*> implies <*(a |^ b)*> . k = (<*a*> /. k) |^ b )

assume k in dom <*a*> ; :: thesis: <*(a |^ b)*> . k = (<*a*> /. k) |^ b

then k in {1} by FINSEQ_1:2, FINSEQ_1:38;

then A2: k = 1 by TARSKI:def 1;

hence <*(a |^ b)*> . k = a |^ b by FINSEQ_1:40

.= (<*a*> /. k) |^ b by A2, FINSEQ_4:16 ;

:: thesis: verum

end;assume k in dom <*a*> ; :: thesis: <*(a |^ b)*> . k = (<*a*> /. k) |^ b

then k in {1} by FINSEQ_1:2, FINSEQ_1:38;

then A2: k = 1 by TARSKI:def 1;

hence <*(a |^ b)*> . k = a |^ b by FINSEQ_1:40

.= (<*a*> /. k) |^ b by A2, FINSEQ_4:16 ;

:: thesis: verum

.= len <*a*> by FINSEQ_1:39 ;

hence <*a*> |^ b = <*(a |^ b)*> by A1, Def1; :: thesis: verum