let X, Y be non empty set ; 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 ; 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; 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; ( rng f c= dom (g | S) implies (g | S) /* f = g /* f )
assume A1:
rng f c= dom (g | S)
; (g | S) /* f = g /* f
let x be Element of X; FUNCT_2:def 8 ((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
; verum