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