let p1, p2, p3, p4, p5 be XFinSequence; :: thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ p3) ^ (p4 ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ ((p3 ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ (p3 ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (((p2 ^ p3) ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ p3) ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ ((p3 ^ p4) ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) )
thus (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ p3) ^ (p4 ^ p5) by AFINSQ_1:27; :: thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ ((p3 ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ (p3 ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (((p2 ^ p3) ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ p3) ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ ((p3 ^ p4) ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) )
thus (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ ((p3 ^ p4) ^ p5) by Lm1; :: thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ (p3 ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (((p2 ^ p3) ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ p3) ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ ((p3 ^ p4) ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) )
thus (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ (p3 ^ (p4 ^ p5)) by Lm1; :: thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (((p2 ^ p3) ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ p3) ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ ((p3 ^ p4) ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) )
thus A1: (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 by Lm1
.= p1 ^ (((p2 ^ p3) ^ p4) ^ p5) by AFINSQ_1:27 ; :: thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ p3) ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ ((p3 ^ p4) ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) )
hence (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ p3) ^ (p4 ^ p5)) by AFINSQ_1:27; :: thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ ((p3 ^ p4) ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) )
thus (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ ((p3 ^ p4) ^ p5)) by A1, Lm1; :: thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) )
thus (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) by A1, Lm1; :: thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) )
thus (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 by Lm1; :: thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) )
thus (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 by Lm1; :: thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) )
thus (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 by Lm1; :: thesis: (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5)
thus (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) by A1, Lm1; :: thesis: verum