let r, s be Real; :: thesis: r |^ <*s*> = <*(r to_power s)*>
A1: len <*s*> = 1 by FINSEQ_1:39;
( dom <*s*> = Seg 1 & Seg 1 = {1} ) by FINSEQ_1:2, FINSEQ_1:38;
then ( 1 in dom <*s*> & <*s*> . 1 = s ) ;
then (r |^ <*s*>) . 1 = r to_power s by Def4;
hence r |^ <*s*> = <*(r to_power s)*> by A1, CARD_1:def 7, FINSEQ_1:40; :: thesis: verum