thus rng (f |^ a) c= REAL ; :: according to FINSEQ_1:def 4 :: thesis: verum