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

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