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

proof

let x be set ; :: 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:90;
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 x in dom (g * f) ; :: thesis: x in dom ((g | (rng f)) * f)
then ( x in dom f & f . x in dom g ) by FUNCT_1:21;
then ( x in dom f & f . x in dom g & f . x in rng f ) by FUNCT_1:def 5;
then ( x in dom f & f . x in dom (g | (rng f)) ) by A1, XBOOLE_0:def 4;
hence x in dom ((g | (rng f)) * f) by FUNCT_1:21; :: thesis: verum

end;

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

end;

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

proof

let x be set ; :: thesis: ( x in dom (g * f) implies (g * f) . x = ((g | (rng f)) * f) . x )
assume A3: x in dom (g * f) ; :: thesis: (g * f) . x = ((g | (rng f)) * f) . x
then A4: ( x in dom f & f . x in dom g ) by FUNCT_1:21;
then A5: f . x in rng f by FUNCT_1:def 5;
thus (g * f) . x = g . (f . x) by A3, FUNCT_1:22
.= (g | (rng f)) . (f . x) by A5, FUNCT_1:72
.= ((g | (rng f)) * f) . x by A4, FUNCT_1:23 ; :: thesis: verum

end;

hence g * f = (g | (rng f)) * f by A2, FUNCT_1:9; :: thesis: verum