let X, Y be non empty set ; :: thesis: for Z, S, T being set
for f being Function of X,Y
for g being PartFunc of Y,Z st rng f c= dom (g | S) & S c= T holds
(g | S) /* f = (g | T) /* f
let Z, S, T be set ; :: thesis: for f being Function of X,Y
for g being PartFunc of Y,Z st rng f c= dom (g | S) & S c= T holds
(g | S) /* f = (g | T) /* f
let f be Function of X,Y; :: thesis: for g being PartFunc of Y,Z st rng f c= dom (g | S) & S c= T holds
(g | S) /* f = (g | T) /* f
let g be PartFunc of Y,Z; :: thesis: ( rng f c= dom (g | S) & S c= T implies (g | S) /* f = (g | T) /* f )
assume A1: rng f c= dom (g | S) ; :: thesis: ( not S c= T or (g | S) /* f = (g | T) /* f )
assume S c= T ; :: thesis: (g | S) /* f = (g | T) /* f
then g | S c= g | T by RELAT_1:75;
then A2: dom (g | S) c= dom (g | T) by RELAT_1:11;
thus (g | S) /* f = g /* f by A1, Th116
.= (g | T) /* f by A1, A2, Th116, XBOOLE_1:1 ; :: thesis: verum