take chi C,C ; :: thesis: ( dom (chi C,C) = C & rng (chi C,C) c= [.0 ,1.] )
thus ( dom (chi C,C) = C & rng (chi C,C) c= [.0 ,1.] ) by Th1, FUNCT_3:def 3; :: thesis: verum