let f, g be Function; :: thesis: for C being set st rng f c= C holds
(g | C) * f = g * f
let C be set ; :: thesis: ( rng f c= C implies (g | C) * f = g * f )
assume A1: rng f c= C ; :: thesis: (g | C) * f = g * f
(g | C) * f = g * (C |` f) by MONOID_1:1
.= g * f by A1, RELAT_1:94 ;
hence (g | C) * f = g * f ; :: thesis: verum