let f, h, F be Function; :: thesis: for x being set holds (F [;] x,f) * h = F [;] x,(f * h)
let x be set ; :: thesis: (F [;] x,f) * h = F [;] x,(f * h)
A1: dom ((dom f) --> x) = dom f by Th19;
then A2: dom (((dom f) --> x) * h) = dom (f * h) by RELAT_1:198;

A3: now

let z be set ; :: thesis: ( z in dom (((dom f) --> x) * h) implies (((dom f) --> x) * h) . z = x )
assume A4: z in dom (((dom f) --> x) * h) ; :: thesis: (((dom f) --> x) * h) . z = x
then A5: h . z in dom ((dom f) --> x) by FUNCT_1:21;
thus (((dom f) --> x) * h) . z = ((dom f) --> x) . (h . z) by A4, FUNCT_1:22
.= x by A1, A5, Th13 ; :: thesis: verum

end;

thus (F [;] x,f) * h = (F .: ((dom f) --> x),f) * h
.= F .: (((dom f) --> x) * h),(f * h) by Th31
.= F [;] x,(f * h) by A2, A3, Th17 ; :: thesis: verum