let X, Y be non empty set ; :: thesis: for Z, S being set
for f being Function of X,Y
for g being PartFunc of Y,Z st rng f c= dom (g | S) holds
(g | S) /* f = g /* f
let Z, S be set ; :: thesis: for f being Function of X,Y
for g being PartFunc of Y,Z st rng f c= dom (g | S) holds
(g | S) /* f = g /* f
let f be Function of X,Y; :: thesis: for g being PartFunc of Y,Z st rng f c= dom (g | S) holds
(g | S) /* f = g /* f
let g be PartFunc of Y,Z; :: thesis: ( rng f c= dom (g | S) implies (g | S) /* f = g /* f )
assume A1: rng f c= dom (g | S) ; :: thesis: (g | S) /* f = g /* f
let x be Element of X; :: according to FUNCT_2:def 8 :: thesis: ((g | S) /* f) . x = (g /* f) . x
A2: dom (g | S) c= dom g by RELAT_1:60;
A3: f . x in rng f by Th4;
thus ((g | S) /* f) . x = (g | S) . (f . x) by A1, Th107
.= g . (f . x) by A1, A3, FUNCT_1:47
.= (g /* f) . x by A1, A2, Th107, XBOOLE_1:1 ; :: thesis: verum