rng (f | (Seg n)) c= REAL ;
hence rng (f | n) c= REAL ; :: according to RELAT_1:def 19 :: thesis: verum