let z be object ; :: thesis: for f being Function
for x, y being object st x <> y holds
(f +~ (x,y)) +~ (x,z) = f +~ (x,y)
let f be Function; :: thesis: for x, y being object st x <> y holds
(f +~ (x,y)) +~ (x,z) = f +~ (x,y)
let x, y be object ; :: thesis: ( x <> y implies (f +~ (x,y)) +~ (x,z) = f +~ (x,y) )
assume x <> y ; :: thesis: (f +~ (x,y)) +~ (x,z) = f +~ (x,y)
then not x in rng (f +~ (x,y)) by Th100;
hence (f +~ (x,y)) +~ (x,z) = f +~ (x,y) by Th103; :: thesis: verum