theorem Th20: :: SUBSTLAT:20

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