set f = (0,n) --> (n,0);
assume
(0,n) --> (n,0) is with_fixpoint
; 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; verum