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

A3: now :: thesis: for z being object st z in dom (((dom f) --> x) * h) holds
(((dom f) --> x) * h) . z = x

let z be object ; :: 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:11;
thus (((dom f) --> x) * h) . z = ((dom f) --> x) . (h . z) by A4, FUNCT_1:12
.= x by A5, Th7 ; :: thesis: verum

end;

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