for D being set
for f, g being XFinSequence of D
for h being FinSequence of D holds
( (f ^ g) ^ h = f ^ (g ^ h) & (f ^ h) ^ g = f ^ (h ^ g) & (h ^ f) ^ g = h ^ (f ^ g) )