let a be Real; :: thesis: for m being non zero Nat holds <*a*> |^ m = <*(a |^ m)*>
let m be non zero Nat; :: thesis: <*a*> |^ m = <*(a |^ m)*>
set f = <*a*> |^ m;
set g = <*(a |^ m)*>;
len (<*a*> |^ m) = len <*a*> by NAT_3:def 1;
then A0: dom (<*a*> |^ m) = dom <*a*> by FINSEQ_3:29
.= Seg 1 by FINSEQ_1:38 ;
then A1: dom (<*a*> |^ m) = dom <*(a |^ m)*> by FINSEQ_1:38;
for k being Nat st k in dom (<*a*> |^ m) holds
(<*a*> |^ m) . k = <*(a |^ m)*> . k

proof

let k be Nat; :: thesis: ( k in dom (<*a*> |^ m) implies (<*a*> |^ m) . k = <*(a |^ m)*> . k )
assume B1: k in dom (<*a*> |^ m) ; :: thesis: (<*a*> |^ m) . k = <*(a |^ m)*> . k
then B2: k = 1 by TARSKI:def 1, A0, FINSEQ_1:2;
(<*a*> |^ m) . k = (<*a*> . k) |^ m by B1, NAT_3:def 1
.= <*(a |^ m)*> . k by B2 ;
hence (<*a*> |^ m) . k = <*(a |^ m)*> . k ; :: thesis: verum

end;

hence <*a*> |^ m = <*(a |^ m)*> by A1, FINSEQ_1:13; :: thesis: verum