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