let f, F be Function; 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 ; ( 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))
; (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
; verum