let p, q, r be FinSequence; :: thesis: len ((p ^ q) ^ r) = ((len p) + (len q)) + (len r)
thus len ((p ^ q) ^ r) = (len (p ^ q)) + (len r) by FINSEQ_1:22
.= ((len p) + (len q)) + (len r) by FINSEQ_1:22 ; :: thesis: verum