let a be natural number ; :: thesis: (<*> REAL ) |^ a = <*> REAL
len ((<*> REAL ) |^ a) = len (<*> REAL ) by Def1
.= 0 ;
hence (<*> REAL ) |^ a = <*> REAL ; :: thesis: verum