let Z, X 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
Z1: X <> {} and
Z: rng f c= dom p ; :: thesis: (p /* f) . x = p . (f . x)
p /* f = p * f by Z, Def12;
hence (p /* f) . x = p . (f . x) by Th21, Z1; :: thesis: verum