let z be object ; for f being Function
for x, y being object st z in dom f & f . z = x holds
(f +~ (x,y)) . z = y
let f be Function; for x, y being object st z in dom f & f . z = x holds
(f +~ (x,y)) . z = y
let x, y be object ; ( z in dom f & f . z = x implies (f +~ (x,y)) . z = y )
assume that
A1:
z in dom f
and
A2:
f . z = x
; (f +~ (x,y)) . z = y
f . z in dom (x .--> y)
by A2, FUNCOP_1:74;
then A3:
z in dom ((x .--> y) * f)
by A1, FUNCT_1:11;
hence (f +~ (x,y)) . z =
((x .--> y) * f) . z
by Th13
.=
(x .--> y) . x
by A2, A3, FUNCT_1:12
.=
y
by FUNCOP_1:72
;
verum