let f, F be Function; :: thesis: for x, z being object st x in dom (F [:] (f,z)) holds
(F [:] (f,z)) . x = F . ((f . x),z)
let x, z be object ; :: thesis: ( x in dom (F [:] (f,z)) implies (F [:] (f,z)) . x = F . ((f . x),z) )
A1: dom <:f,((dom f) --> z):> = (dom f) /\ (dom ((dom f) --> z)) by FUNCT_3:def 7;
assume A2: x in dom (F [:] (f,z)) ; :: thesis: (F [:] (f,z)) . x = F . ((f . x),z)
then x in dom <:f,((dom f) --> z):> by FUNCT_1:11;
then A3: x in dom f by A1;
thus (F [:] (f,z)) . x = F . ((f . x),(((dom f) --> z) . x)) by A2, Lm1
.= F . ((f . x),z) by A3, Th7 ; :: thesis: verum