thus rng (z1 + z2) c= COMPLEX ; :: according to FINSEQ_1:def 4 :: thesis: verum