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