reconsider IT = {} as FinSequence ;
take IT ; :: thesis: IT is X -valued
rng IT = X /\ {} ;
hence IT is X -valued by RELAT_1:def 19; :: thesis: verum