theorem Th14: :: WAYBEL24:14

for R, S, T being LATTICE
for f being Function of [:R,S:],T
for b being Element of S
for X being Subset of R holds (Proj (f,b)) .: X = f .: [:X,{b}:]