let p1, p2, p3 be FinSequence; :: thesis: ( ((len p1) + (len p2)) + (len p3) = len ((p1 ^ p2) ^ p3) & ((len p1) + (len p2)) + (len p3) = len (p1 ^ (p2 ^ p3)) & (len p1) + ((len p2) + (len p3)) = len (p1 ^ (p2 ^ p3)) & (len p1) + ((len p2) + (len p3)) = len ((p1 ^ p2) ^ p3) )
thus A1: ((len p1) + (len p2)) + (len p3) = (len (p1 ^ p2)) + (len p3) by FINSEQ_1:35
.= len ((p1 ^ p2) ^ p3) by FINSEQ_1:35 ; :: thesis: ( ((len p1) + (len p2)) + (len p3) = len (p1 ^ (p2 ^ p3)) & (len p1) + ((len p2) + (len p3)) = len (p1 ^ (p2 ^ p3)) & (len p1) + ((len p2) + (len p3)) = len ((p1 ^ p2) ^ p3) )
hence ((len p1) + (len p2)) + (len p3) = len (p1 ^ (p2 ^ p3)) by FINSEQ_1:45; :: thesis: ( (len p1) + ((len p2) + (len p3)) = len (p1 ^ (p2 ^ p3)) & (len p1) + ((len p2) + (len p3)) = len ((p1 ^ p2) ^ p3) )
thus (len p1) + ((len p2) + (len p3)) = len (p1 ^ (p2 ^ p3)) by A1, FINSEQ_1:45; :: thesis: (len p1) + ((len p2) + (len p3)) = len ((p1 ^ p2) ^ p3)
thus (len p1) + ((len p2) + (len p3)) = len ((p1 ^ p2) ^ p3) by A1; :: thesis: verum