theorem Th15: :: WAYBEL24:15

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