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