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)*>

A1: now

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:4, FINSEQ_1:55;
then A2: k = 1 by TARSKI:def 1;
hence <*(a |^ b)*> . k = a |^ b by FINSEQ_1:57
.= (<*a*> /. k) |^ b by A2, FINSEQ_4:25 ;
:: thesis: verum

end;

len <*(a |^ b)*> = 1 by FINSEQ_1:57
.= len <*a*> by FINSEQ_1:56 ;
hence <*a*> |^ b = <*(a |^ b)*> by A1, Def1; :: thesis: verum