let p, q, r be FinSequence; :: thesis: len (p ^ q) <= len (p ^ (q ^ r))
len ((p ^ q) ^ r) = len (p ^ (q ^ r)) by FINSEQ_1:32;
hence len (p ^ q) <= len (p ^ (q ^ r)) by CALCUL_1:6; :: thesis: verum