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