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