theorem Th24: :: SUBSTLAT:24

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