let R be Relation; :: thesis: ( R is COMPLEX -valued implies R is complex-valued )
assume R is COMPLEX -valued ; :: thesis: R is complex-valued
hence rng R c= COMPLEX by RELAT_1:def 19; :: according to VALUED_0:def 1 :: thesis: verum