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
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