let a be Nat; :: thesis: for r being Real holds <*r*> |^ a = <*(r |^ a)*>
let r be Real; :: thesis: <*r*> |^ a = <*(r |^ a)*>
A1: len (<*r*> |^ a) = len <*r*> by Def1
.= 1 by FINSEQ_1:40 ;
0 + 1 in Seg (0 + 1) ;
then 1 in dom (<*r*> |^ a) by A1, FINSEQ_1:def 3;
then (<*r*> |^ a) . 1 = (<*r*> . 1) |^ a by Def1
.= r |^ a ;
hence <*r*> |^ a = <*(r |^ a)*> by A1, FINSEQ_1:40; :: thesis: verum