let f, g be Function; :: thesis: g * f = (g | (rng f)) * f
for x being object holds
( x in dom (g * f) iff x in dom ((g | (rng f)) * f) )

proof

let x be object ; :: thesis: ( x in dom (g * f) iff x in dom ((g | (rng f)) * f) )
A1: dom (g | (rng f)) = (dom g) /\ (rng f) by RELAT_1:61;
thus ( x in dom (g * f) implies x in dom ((g | (rng f)) * f) ) :: thesis: ( x in dom ((g | (rng f)) * f) implies x in dom (g * f) )

proof

assume A2: x in dom (g * f) ; :: thesis: x in dom ((g | (rng f)) * f)
then A3: x in dom f by FUNCT_1:11;
x in dom f by A2, FUNCT_1:11;
then A4: f . x in rng f by FUNCT_1:def 3;
f . x in dom g by A2, FUNCT_1:11;
then f . x in dom (g | (rng f)) by A1, A4, XBOOLE_0:def 4;
hence x in dom ((g | (rng f)) * f) by A3, FUNCT_1:11; :: thesis: verum

end;

assume A5: x in dom ((g | (rng f)) * f) ; :: thesis: x in dom (g * f)
then f . x in dom (g | (rng f)) by FUNCT_1:11;
then A6: f . x in dom g by A1, XBOOLE_0:def 4;
x in dom f by A5, FUNCT_1:11;
hence x in dom (g * f) by A6, FUNCT_1:11; :: thesis: verum

end;

then A7: dom (g * f) = dom ((g | (rng f)) * f) by TARSKI:2;
for x being object st x in dom (g * f) holds
(g * f) . x = ((g | (rng f)) * f) . x

proof

let x be object ; :: thesis: ( x in dom (g * f) implies (g * f) . x = ((g | (rng f)) * f) . x )
assume A8: x in dom (g * f) ; :: thesis: (g * f) . x = ((g | (rng f)) * f) . x
then A9: x in dom f by FUNCT_1:11;
then A10: f . x in rng f by FUNCT_1:def 3;
thus (g * f) . x = g . (f . x) by A8, FUNCT_1:12
.= (g | (rng f)) . (f . x) by A10, FUNCT_1:49
.= ((g | (rng f)) * f) . x by A9, FUNCT_1:13 ; :: thesis: verum

end;

hence g * f = (g | (rng f)) * f by A7; :: thesis: verum