let F, G be Function-yielding Function; :: thesis: for f being Function holds (G ** F) * f = (G * f) ** (F * f)
let f be Function; :: thesis: (G ** F) * f = (G * f) ** (F * f)
A1: dom ((G ** F) * f) = f " (dom (G ** F)) by RELAT_1:147
.= f " ((dom G) /\ (dom F)) by PBOOLE:def 19
.= (f " (dom F)) /\ (f " (dom G)) by FUNCT_1:68
.= (f " (dom F)) /\ (dom (G * f)) by RELAT_1:147
.= (dom (F * f)) /\ (dom (G * f)) by RELAT_1:147 ;

now :: thesis: for i being object st i in dom ((G ** F) * f) holds
((G ** F) * f) . i = ((G * f) . i) * ((F * f) . i)

let i be object ; :: thesis: ( i in dom ((G ** F) * f) implies ((G ** F) * f) . i = ((G * f) . i) * ((F * f) . i) )
assume A2: i in dom ((G ** F) * f) ; :: thesis: ((G ** F) * f) . i = ((G * f) . i) * ((F * f) . i)
then A3: i in dom f by FUNCT_1:11;
A4: f . i in dom (G ** F) by A2, FUNCT_1:11;
thus ((G ** F) * f) . i = (G ** F) . (f . i) by A2, FUNCT_1:12
.= (G . (f . i)) * (F . (f . i)) by A4, PBOOLE:def 19
.= ((G * f) . i) * (F . (f . i)) by A3, FUNCT_1:13
.= ((G * f) . i) * ((F * f) . i) by A3, FUNCT_1:13 ; :: thesis: verum

end;

hence (G ** F) * f = (G * f) ** (F * f) by A1, PBOOLE:def 19; :: thesis: verum