theorem Th4: :: SUBSTLAT:4

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