let z be object ; :: thesis: 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; :: thesis: for x, y being object st z in dom f & f . z = x holds
(f +~ (x,y)) . z = y
let x, y be object ; :: thesis: ( 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 ; :: thesis: (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 ;
:: thesis: verum