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;

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

hence
MIM <*r*> = <*r*>
by A1, A2, FINSEQ_2:9; :: thesis: verum(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;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