theorem Th19: :: SUBSTLAT:19

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