( len (p ^ q) = (len p) + (len q) & len p = n & len q = m ) by AFINSQ_1:17, CARD_1:def 7;
hence p ^ q is n + m -element by CARD_1:def 7; :: thesis: verum