theorem Th17: :: SUBSTLAT:17

for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi (A ^ B) c= (mi A) ^ B