let m, n be Element of NAT ; :: thesis: ( ( i in dom D1 & m in dom D2 & D1 . i = D2 . m & n in dom D2 & D1 . i = D2 . n implies m = n ) & ( not i in dom D1 & m = 0 & n = 0 implies m = n ) )

hereby :: thesis: ( not i in dom D1 & m = 0 & n = 0 implies m = n )

assume that
i in dom D1 and
A2: m in dom D2 and
A3: D1 . i = D2 . m and
A4: n in dom D2 and
A5: D1 . i = D2 . n ; :: thesis: not m <> n
assume A6: m <> n ; :: thesis: contradiction

now :: thesis: contradiction

per cases ( m < n or n < m ) by A6, XXREAL_0:1;

suppose m < n ; :: thesis: contradiction

hence contradiction by A2, A3, A4, A5, SEQM_3:def 1; :: thesis: verum

end;

suppose n < m ; :: thesis: contradiction

hence contradiction by A2, A3, A4, A5, SEQM_3:def 1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

assume that
not i in dom D1 and
A7: m = 0 and
A8: n = 0 ; :: thesis: m = n
thus m = n by A7, A8; :: thesis: verum