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) ) )

((f | (X \/ Y)) * g) . i = (f | X) . (g . i)

(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

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

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;hereby :: thesis: ( i in dom g & g . i in dom (f | X) implies i in dom ((f | (X \/ Y)) * g) )

assume A4:
( i in dom g & g . i in dom (f | X) )
; :: thesis: 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;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

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

((f | (X \/ Y)) * g) . i = (f | X) . (g . i)

proof

hence
(f | (X \/ Y)) * g = (f | X) * g
by FUNCT_1:10, A2; :: thesis: verum
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;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