let X, Z be set ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( X <> {} & rng f c= dom p implies (p /* f) . x = p /. (f . x) )
assume that
A1: X <> {} and
A2: rng f c= dom p ; :: thesis: (p /* f) . x = p /. (f . x)
A3: f . x in rng f by A1, Th4;
thus (p /* f) . x = p . (f . x) by A1, A2, Th107
.= p /. (f . x) by A2, A3, PARTFUN1:def 6 ; :: thesis: verum