let p, q, r, s be FinSequence; :: thesis: ( ((p ^ q) ^ r) ^ s = (p ^ (q ^ r)) ^ s & ((p ^ q) ^ r) ^ s = (p ^ q) ^ (r ^ s) & (p ^ (q ^ r)) ^ s = (p ^ q) ^ (r ^ s) )
((p ^ q) ^ r) ^ s = (p ^ q) ^ (r ^ s) by FINSEQ_1:32;
hence ( ((p ^ q) ^ r) ^ s = (p ^ (q ^ r)) ^ s & ((p ^ q) ^ r) ^ s = (p ^ q) ^ (r ^ s) & (p ^ (q ^ r)) ^ s = (p ^ q) ^ (r ^ s) ) by FINSEQ_1:32; :: thesis: verum