let f be Function-yielding Function; :: thesis: for g, h being Function holds (f .. g) * h = (f * h) .. (g * h)
let g, h be Function; :: thesis: (f .. g) * h = (f * h) .. (g * h)
A1: for x being set st x in dom (f * h) holds
((f .. g) * h) . x = ((f * h) . x) . ((g * h) . x)

proof

let x be set ; :: thesis: ( x in dom (f * h) implies ((f .. g) * h) . x = ((f * h) . x) . ((g * h) . x) )
assume A2: x in dom (f * h) ; :: thesis: ((f .. g) * h) . x = ((f * h) . x) . ((g * h) . x)
then A3: x in dom h by FUNCT_1:21;
A4: h . x in dom f by A2, FUNCT_1:21;
thus ((f .. g) * h) . x = (f .. g) . (h . x) by A3, FUNCT_1:23
.= (f . (h . x)) . (g . (h . x)) by A4, PRALG_1:def 17
.= ((f * h) . x) . (g . (h . x)) by A3, FUNCT_1:23
.= ((f * h) . x) . ((g * h) . x) by A3, FUNCT_1:23 ; :: thesis: verum

end;

dom (f .. g) = dom f by PRALG_1:def 17;
then dom ((f .. g) * h) = dom (f * h) by RELAT_1:198;
hence (f .. g) * h = (f * h) .. (g * h) by A1, PRALG_1:def 17; :: thesis: verum