let r be Real; :: thesis: MIM <*r*> = <*r*>
set f = <*r*>;
A1: len <*r*> = 1 by FINSEQ_1:57;
then A2: len (MIM <*r*>) = 1 by Def3;
then A3: dom (MIM <*r*>) = Seg 1 by FINSEQ_1:def 3;

now

let n be Nat; :: thesis: ( n in dom (MIM <*r*>) implies (MIM <*r*>) . n = <*r*> . n )
assume n in dom (MIM <*r*>) ; :: thesis: (MIM <*r*>) . n = <*r*> . n
then n = 1 by A3, FINSEQ_1:4, TARSKI:def 1;
hence (MIM <*r*>) . n = <*r*> . n by A1, A2, Def3; :: thesis: verum

end;

hence MIM <*r*> = <*r*> by A1, A2, FINSEQ_2:10; :: thesis: verum