let f, g be Function; :: thesis: for X, Y being set st rng g c= X holds
(f | (X \/ Y)) * g = (f | X) * g
let X, Y be set ; :: thesis: ( rng g c= X implies (f | (X \/ Y)) * g = (f | X) * g )
assume A1: rng g c= X ; :: thesis: (f | (X \/ Y)) * g = (f | X) * g
A2: for i being object holds
( i in dom ((f | (X \/ Y)) * g) iff ( i in dom g & g . i in dom (f | X) ) )

proof

let i be object ; :: thesis: ( i in dom ((f | (X \/ Y)) * g) iff ( i in dom g & g . i in dom (f | X) ) )

hereby :: thesis: ( i in dom g & g . i in dom (f | X) implies i in dom ((f | (X \/ Y)) * g) )

assume AA: i in dom ((f | (X \/ Y)) * g) ; :: thesis: ( i in dom g & g . i in dom (f | X) )
then A3: ( i in dom g & g . i in dom (f | (X \/ Y)) ) by FUNCT_1:11;
then g . i in (dom f) /\ (X \/ Y) by RELAT_1:61;
then P3: ( g . i in dom f & g . i in X \/ Y ) by XBOOLE_0:def 4;
g . i in rng g by A3, FUNCT_1:3;
then g . i in (dom f) /\ X by A1, P3, XBOOLE_0:def 4;
hence ( i in dom g & g . i in dom (f | X) ) by AA, FUNCT_1:11, RELAT_1:61; :: thesis: verum

end;

assume A4: ( i in dom g & g . i in dom (f | X) ) ; :: thesis: i in dom ((f | (X \/ Y)) * g)
then g . i in (dom f) /\ X by RELAT_1:61;
then A5: ( g . i in dom f & g . i in X ) by XBOOLE_0:def 4;
then g . i in X \/ Y by XBOOLE_0:def 3;
then g . i in (dom f) /\ (X \/ Y) by A5, XBOOLE_0:def 4;
then g . i in dom (f | (X \/ Y)) by RELAT_1:61;
hence i in dom ((f | (X \/ Y)) * g) by A4, FUNCT_1:11; :: thesis: verum

end;

for i being object st i in dom ((f | (X \/ Y)) * g) holds
((f | (X \/ Y)) * g) . i = (f | X) . (g . i)

proof

let i be object ; :: thesis: ( i in dom ((f | (X \/ Y)) * g) implies ((f | (X \/ Y)) * g) . i = (f | X) . (g . i) )
assume A7: i in dom ((f | (X \/ Y)) * g) ; :: thesis: ((f | (X \/ Y)) * g) . i = (f | X) . (g . i)
then ( i in dom g & g . i in dom (f | X) ) by A2;
then g . i in (dom f) /\ X by RELAT_1:61;
then ( g . i in dom f & g . i in X ) by XBOOLE_0:def 4;
then A9: g . i in X \/ Y by XBOOLE_0:def 3;
thus ((f | (X \/ Y)) * g) . i = (f | (X \/ Y)) . (g . i) by A7, FUNCT_1:12
.= f . (g . i) by FUNCT_1:49, A9
.= (f | X) . (g . i) by A2, A7, FUNCT_1:47 ; :: thesis: verum

end;

hence (f | (X \/ Y)) * g = (f | X) * g by FUNCT_1:10, A2; :: thesis: verum