let f, g, h be Function; :: thesis: ( rng f misses dom g implies (h +* g) * f = h * f )
assume A1: rng f misses dom g ; :: thesis: (h +* g) * f = h * f
thus (h +* g) * f = (h * f) +* (g * f) by Th11
.= (h * f) +* {} by A1, RELAT_1:44
.= h * f by FUNCT_4:21 ; :: thesis: verum