thus len (p ^ q) = (len p) + (len q) by FINSEQ_1:35
.= n + (len q) by CIRCCOMB:def 12
.= n + m by CIRCCOMB:def 12 ; :: according to CIRCCOMB:def 12 :: thesis: verum