set f = (0,n) --> (m,0);

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( 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)) ; :: thesis: ( 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; :: thesis: verum

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( 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)) ; :: thesis: ( 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; :: thesis: verum