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 :: thesis: for k being Nat st k in dom <*a*> holds
<*(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;
len <*(a |^ b)*> = 1 by FINSEQ_1:40
.= len <*a*> by FINSEQ_1:39 ;
hence <*a*> |^ b = <*(a |^ b)*> by A1, Def1; :: thesis: verum