let Z, X 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) )
assume Z: rng f c= dom p ; :: thesis: (p /* f) * g = p /* (f * g)
A: rng (f * g) c= rng f by RELAT_1:45;
thus (p /* f) * g = (p * f) * g by Z, Def12
.= p * (f * g) by RELAT_1:55
.= p /* (f * g) by A, Def12, Z, XBOOLE_1:1 ; :: thesis: verum