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 A1: 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
A2: z in dom (f +~ x,y) and
A3: (f +~ x,y) . z = x by FUNCT_1:def 5;
A4: z in dom f by A2, Th105;

A5: now

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

end;

(x .--> y) . (f . z) = ((x .--> y) * f) . z by A4, FUNCT_1:23
.= x by A3, A5, Th14 ;
then f . z <> x by A1, FUNCOP_1:87;
then not f . z in dom (x .--> y) by FUNCOP_1:90;
hence contradiction by A5, FUNCT_1:21; :: thesis: verum