let X, Z be set ; :: thesis: for Y being non empty set
for f being Function of X,Y
for p being PartFunc of Y,Z
for g being Function of X,X st rng f c= dom p holds
(p /* f) * g = p /* (f * g)
let Y be non empty set ; :: thesis: for f being Function of X,Y
for p being PartFunc of Y,Z
for g being Function of X,X st rng f c= dom p holds
(p /* f) * g = p /* (f * g)
let f be Function of X,Y; :: thesis: for p being PartFunc of Y,Z
for g being Function of X,X st rng f c= dom p holds
(p /* f) * g = p /* (f * g)
let p be PartFunc of Y,Z; :: thesis: for g being Function of X,X st rng f c= dom p holds
(p /* f) * g = p /* (f * g)
let g be Function of X,X; :: thesis: ( rng f c= dom p implies (p /* f) * g = p /* (f * g) )
A1: rng (f * g) c= rng f by RELAT_1:26;
assume A2: rng f c= dom p ; :: thesis: (p /* f) * g = p /* (f * g)
hence (p /* f) * g = (p * f) * g by Def11
.= p * (f * g) by RELAT_1:36
.= p /* (f * g) by A2, A1, Def11, XBOOLE_1:1 ;
:: thesis: verum