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

assume (0,n) --> (n,0) is with_fixpoint ; :: thesis: contradiction

then consider x being object such that

A1: x is_a_fixpoint_of (0,n) --> (n,0) by ABIAN:def 5;

A2: x in dom ((0,n) --> (n,0)) by A1, ABIAN:def 3;

A3: ((0,n) --> (n,0)) . x = x by A1, ABIAN:def 3;

dom ((0,n) --> (n,0)) = {0,n} by FUNCT_4:62;

then ( x = 0 or x = n ) by A2, TARSKI:def 2;

hence contradiction by A3, FUNCT_4:63; :: thesis: verum

assume (0,n) --> (n,0) is with_fixpoint ; :: thesis: contradiction

then consider x being object such that

A1: x is_a_fixpoint_of (0,n) --> (n,0) by ABIAN:def 5;

A2: x in dom ((0,n) --> (n,0)) by A1, ABIAN:def 3;

A3: ((0,n) --> (n,0)) . x = x by A1, ABIAN:def 3;

dom ((0,n) --> (n,0)) = {0,n} by FUNCT_4:62;

then ( x = 0 or x = n ) by A2, TARSKI:def 2;

hence contradiction by A3, FUNCT_4:63; :: thesis: verum