let f be Function; :: thesis: for x, y being set st x <> y holds
not x in rng (f +~ x,y)
let x, y be set ; :: thesis: ( x <> y implies not x in rng (f +~ x,y) )
assume Z1: x <> y ; :: thesis: not x in rng (f +~ x,y)
assume x in rng (f +~ x,y) ; :: thesis: contradiction
then consider z being set such that
W1: z in dom (f +~ x,y) and
W2: (f +~ x,y) . z = x by FUNCT_1:def 5;
A: z in dom f by W1, Tw1;

D: now

assume Z: not z in dom ((x .--> y) * f) ; :: thesis: contradiction
then f . z = x by W2, Th12;
then f . z in dom (x .--> y) by FUNCOP_1:89;
hence contradiction by Z, A, FUNCT_1:21; :: thesis: verum

end;

(x .--> y) . (f . z) = ((x .--> y) * f) . z by A, FUNCT_1:23
.= x by W2, Th14, D ;
then f . z <> x by Z1, FUNCOP_1:87;
then not f . z in dom (x .--> y) by FUNCOP_1:90;
hence contradiction by D, FUNCT_1:21; :: thesis: verum