theorem Th22: :: SUBSTLAT:22

for V, C being set
for K, L, M being Element of Fin (PFuncs (V,C)) holds K ^ (L \/ M) = (K ^ L) \/ (K ^ M)