let r, s be Real; :: thesis: MIM <*r,s*> = <*(r - s),s*>
set f = <*r,s*>;
A1: ( len <*r,s*> = 2 & <*r,s*> . 1 = r ) by FINSEQ_1:61;
A2: <*r,s*> . 2 = s by FINSEQ_1:61;
( 0 + 2 = 2 & 0 + 1 = 1 ) ;
then MIM <*r,s*> = ((MIM <*r,s*>) | 0 ) ^ <*(r - s),s*> by A1, A2, Th24;
hence MIM <*r,s*> = <*(r - s),s*> by FINSEQ_1:47; :: thesis: verum