set o = <*> REAL ;
set mo = MIM (<*> REAL );
A1: ( len (MIM (<*> REAL )) = len (<*> REAL ) & len (<*> REAL ) = 0 ) by Def3;
thus MIM (<*> REAL ) = <*> REAL by A1; :: thesis: verum