set f = (n,0) --> (0,m);
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom ((n,0) --> (0,m)) or not x2 in dom ((n,0) --> (0,m)) or not ((n,0) --> (0,m)) . x1 = ((n,0) --> (0,m)) . x2 or x1 = x2 )
assume that
A6: x1 in dom ((n,0) --> (0,m)) and
A7: x2 in dom ((n,0) --> (0,m)) ; :: thesis: ( not ((n,0) --> (0,m)) . x1 = ((n,0) --> (0,m)) . x2 or x1 = x2 )
A8: dom ((n,0) --> (0,m)) = {0,n} by FUNCT_4:62;
then A9: ( x2 = 0 or x2 = n ) by A7, TARSKI:def 2;
A10: ((n,0) --> (0,m)) . 0 = m by FUNCT_4:63;
( x1 = 0 or x1 = n ) by A8, A6, TARSKI:def 2;
hence ( not ((n,0) --> (0,m)) . x1 = ((n,0) --> (0,m)) . x2 or x1 = x2 ) by A9, A10, FUNCT_4:63; :: thesis: verum