theorem Th21: :: SUBSTLAT:21

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