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

(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