let X, Z be set ; for Y being non empty set
for f being Function of X,Y
for p being PartFunc of Y,Z
for x being Element of X st X <> {} & rng f c= dom p holds
(p /* f) . x = p . (f . x)
let Y be non empty set ; for f being Function of X,Y
for p being PartFunc of Y,Z
for x being Element of X st X <> {} & rng f c= dom p holds
(p /* f) . x = p . (f . x)
let f be Function of X,Y; for p being PartFunc of Y,Z
for x being Element of X st X <> {} & rng f c= dom p holds
(p /* f) . x = p . (f . x)
let p be PartFunc of Y,Z; for x being Element of X st X <> {} & rng f c= dom p holds
(p /* f) . x = p . (f . x)
let x be Element of X; ( X <> {} & rng f c= dom p implies (p /* f) . x = p . (f . x) )
assume that
A1:
X <> {}
and
A2:
rng f c= dom p
; (p /* f) . x = p . (f . x)
p /* f = p * f
by A2, Def11;
hence
(p /* f) . x = p . (f . x)
by A1, Th15; verum