let z be set ; :: thesis: for f being Function
for x, y being set st z in dom f & f . z = x holds
(f +~ x,y) . z = y
let f be Function; :: thesis: for x, y being set st z in dom f & f . z = x holds
(f +~ x,y) . z = y
let x, y be set ; :: thesis: ( z in dom f & f . z = x implies (f +~ x,y) . z = y )
assume that
Z1: z in dom f and
Z2: f . z = x ; :: thesis: (f +~ x,y) . z = y
f . z in dom (x .--> y) by Z2, FUNCOP_1:89;
then A: z in dom ((x .--> y) * f) by Z1, FUNCT_1:21;
hence (f +~ x,y) . z = ((x .--> y) * f) . z by Th14
.= (x .--> y) . x by A, Z2, FUNCT_1:22
.= y by FUNCOP_1:87 ;
:: thesis: verum