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