let f be Function-yielding Function; :: thesis: for g, h being Function st dom f = dom g holds
(f .. g) * h = (f * h) .. (g * h)
let g, h be Function; :: thesis: ( dom f = dom g implies (f .. g) * h = (f * h) .. (g * h) )
assume AA: dom f = dom g ; :: thesis: (f .. g) * h = (f * h) .. (g * h)
A0: dom ((f * h) .. (g * h)) = (dom (f * h)) /\ (dom (g * h)) by PRALG_1:def 19;
A1: for x being set st x in dom ((f * h) .. (g * h)) holds
((f .. g) * h) . x = ((f * h) . x) . ((g * h) . x)
proof
let x be set ; :: thesis: ( x in dom ((f * h) .. (g * h)) implies ((f .. g) * h) . x = ((f * h) . x) . ((g * h) . x) )
assume x in dom ((f * h) .. (g * h)) ; :: thesis: ((f .. g) * h) . x = ((f * h) . x) . ((g * h) . x)
then x in (dom (f * h)) /\ (dom (g * h)) by PRALG_1:def 19;
then a3: ( x in dom (f * h) & x in dom (g * h) ) by XBOOLE_0:def 4;
then A3: x in dom h by FUNCT_1:11;
( h . x in dom f & h . x in dom g ) by a3, FUNCT_1:11;
then h . x in (dom f) /\ (dom g) by XBOOLE_0:def 4;
then a4: h . x in dom (f .. g) by PRALG_1:def 19;
thus ((f .. g) * h) . x = (f .. g) . (h . x) by A3, FUNCT_1:13
.= (f . (h . x)) . (g . (h . x)) by PRALG_1:def 19, a4
.= ((f * h) . x) . (g . (h . x)) by A3, FUNCT_1:13
.= ((f * h) . x) . ((g * h) . x) by A3, FUNCT_1:13 ; :: thesis: verum
end;
a1: dom (f * h) = dom (g * h) by AA, RELAT_1:163;
dom (f .. g) = (dom f) /\ (dom g) by PRALG_1:def 19
.= dom f by AA ;
then dom ((f .. g) * h) = dom (f * h) by RELAT_1:163;
hence (f .. g) * h = (f * h) .. (g * h) by A1, A0, PRALG_1:def 19, a1; :: thesis: verum