set o = <*> REAL ;
set mo = MIM (<*> REAL );
len (MIM (<*> REAL )) = len (<*> REAL ) by Def3;
hence MIM (<*> REAL ) = <*> REAL ; :: thesis: verum