let f be Function; :: thesis: for x, y being object st x <> y holds
not x in rng (f +~ (x,y))
let x, y be object ; :: 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 object such that
A2: z in dom (f +~ (x,y)) and
A3: (f +~ (x,y)) . z = x by FUNCT_1:def 3;
A4: z in dom f by A2, Th99;
A5: now :: thesis: z in dom ((x .--> y) * f)
assume A6: not z in dom ((x .--> y) * f) ; :: thesis: contradiction
then f . z = x by A3, Th11;
then f . z in dom (x .--> y) by FUNCOP_1:74;
hence contradiction by A4, A6, FUNCT_1:11; :: thesis: verum
end;
(x .--> y) . (f . z) = ((x .--> y) * f) . z by A4, FUNCT_1:13
.= x by A3, A5, Th13 ;
then f . z <> x by A1, FUNCOP_1:72;
then not f . z in dom (x .--> y) by FUNCOP_1:75;
hence contradiction by A5, FUNCT_1:11; :: thesis: verum