thus len the connectives of (B +* C) = len ( the connectives of B ^ the connectives of C) by Def52
.= (len the connectives of B) + (len the connectives of C) by FINSEQ_1:22
.= n1 + (len the connectives of C) by Def29
.= n1 + n2 by Def29 ; :: according to AOFA_A00:def 29 :: thesis: verum