:: deftheorem defines ^ SUBSTLAT:def 3 :
for V, C being set
for A, B being Element of Fin (PFuncs (V,C)) holds A ^ B = { (s \/ t) where s, t is Element of PFuncs (V,C) : ( s in A & t in B & s tolerates t ) } ;