( len f = n & len g = m ) by CARD_1:def 7;
hence len (f ^ g) = n + m by Th22; :: according to CARD_1:def 7 :: thesis: verum