theorem Th3: :: SUBSTLAT:3

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