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