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