theorem Th13: :: SUBSTLAT:13
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds mi ((mi A) \/ B) = mi (A \/ B)