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