theorem Th12: :: RFINSEQ:12

MIM (<*> REAL) = <*> REAL