let f, g be Function; :: thesis: for X being set st rng f c= X holds
(g | X) * f = g * f
let X be set ; :: thesis: ( rng f c= X implies (g | X) * f = g * f )
A1: f " (rng f) = dom f by RELAT_1:134;
assume rng f c= X ; :: thesis: (g | X) * f = g * f
then A2: f " (rng f) c= f " X by RELAT_1:143;
f " X c= dom f by RELAT_1:132;
then A3: f " X = dom f by A2, A1;
dom ((g | X) * f) = f " (dom (g | X)) by RELAT_1:147
.= f " ((dom g) /\ X) by RELAT_1:61
.= (f " (dom g)) /\ (f " X) by FUNCT_1:68
.= f " (dom g) by A3, RELAT_1:132, XBOOLE_1:28
.= dom (g * f) by RELAT_1:147 ;
hence (g | X) * f = g * f by GRFUNC_1:3, RELAT_1:64; :: thesis: verum