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

(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