let s be XFinSequence; :: thesis: ( s is n -element implies s is n -defined )
assume card s = n ; :: according to CARD_1:def 7 :: thesis: s is n -defined
hence dom s c= n ; :: according to RELAT_1:def 18 :: thesis: verum