let r, s be Real; :: thesis: MIM <*r,s*> = <*(r - s),s*>
reconsider r = r, s = s as Element of REAL by XREAL_0:def 1;
set f = <*r,s*>;
A1: ( len <*r,s*> = 2 & <*r,s*> . 1 = r ) by FINSEQ_1:44;
A2: <*r,s*> . 2 = s by FINSEQ_1:44;
( 0 + 2 = 2 & 0 + 1 = 1 ) ;
then MIM <*r,s*> = ((MIM <*r,s*>) | 0) ^ <*(r - s),s*> by A1, A2, Th11;
hence MIM <*r,s*> = <*(r - s),s*> by FINSEQ_1:34; :: thesis: verum