theorem Th1: :: FILEREC1:1

for p, q, r, s being FinSequence holds
( ((p ^ q) ^ r) ^ s = (p ^ (q ^ r)) ^ s & ((p ^ q) ^ r) ^ s = (p ^ q) ^ (r ^ s) & (p ^ (q ^ r)) ^ s = (p ^ q) ^ (r ^ s) )