let i be Integer; :: thesis: for G being Group
for a being Element of G holds <*a*> |^ <*(@ i)*> = <*(a |^ i)*>
let G be Group; :: thesis: for a being Element of G holds <*a*> |^ <*(@ i)*> = <*(a |^ i)*>
let a be Element of G; :: thesis: <*a*> |^ <*(@ i)*> = <*(a |^ i)*>
A1: len <*a*> = 1 by FINSEQ_1:39;
A2: now :: thesis: for k being Nat st k in dom <*a*> holds
<*(a |^ i)*> . k = (<*a*> /. k) |^ (@ (<*(@ i)*> /. k))
let k be Nat; :: thesis: ( k in dom <*a*> implies <*(a |^ i)*> . k = (<*a*> /. k) |^ (@ (<*(@ i)*> /. k)) )
A3: @ i = <*(@ i)*> /. 1 by FINSEQ_4:16;
A4: dom <*a*> = Seg (len <*a*>) by FINSEQ_1:def 3;
assume k in dom <*a*> ; :: thesis: <*(a |^ i)*> . k = (<*a*> /. k) |^ (@ (<*(@ i)*> /. k))
then A5: k = 1 by A1, A4, FINSEQ_1:2, TARSKI:def 1;
hence <*(a |^ i)*> . k = a |^ i by FINSEQ_1:40
.= (<*a*> /. k) |^ (@ (<*(@ i)*> /. k)) by A3, A5, FINSEQ_4:16 ;
:: thesis: verum
end;
len <*(a |^ i)*> = 1 by FINSEQ_1:39;
hence <*a*> |^ <*(@ i)*> = <*(a |^ i)*> by A1, A2, Def3; :: thesis: verum