set f = (0,n) --> (m,0);
let x1, x2 be object ; FUNCT_1:def 4 ( not x1 in dom ((0,n) --> (m,0)) or not x2 in dom ((0,n) --> (m,0)) or not ((0,n) --> (m,0)) . x1 = ((0,n) --> (m,0)) . x2 or x1 = x2 )
assume that
A1:
x1 in dom ((0,n) --> (m,0))
and
A2:
x2 in dom ((0,n) --> (m,0))
; ( not ((0,n) --> (m,0)) . x1 = ((0,n) --> (m,0)) . x2 or x1 = x2 )
A3:
dom ((0,n) --> (m,0)) = {0,n}
by FUNCT_4:62;
then A4:
( x2 = 0 or x2 = n )
by A2, TARSKI:def 2;
A5:
((0,n) --> (m,0)) . 0 = m
by FUNCT_4:63;
( x1 = 0 or x1 = n )
by A3, A1, TARSKI:def 2;
hence
( not ((0,n) --> (m,0)) . x1 = ((0,n) --> (m,0)) . x2 or x1 = x2 )
by A4, A5, FUNCT_4:63; verum