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

now :: thesis: for n being Nat st n in dom (MIM <*r*>) holds
(MIM <*r*>) . n = <*r*> . n

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:2, TARSKI:def 1;
hence (MIM <*r*>) . n = <*r*> . n by A1, A2, Def2; :: thesis: verum

end;

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