theorem :: SUBSTLAT:16

for V, C being set
for A, B being Element of Fin (PFuncs (V,C))
for b, c being Element of PFuncs (V,C) st b in A & c in B & b tolerates c holds
b \/ c in A ^ B ;