let s be n -element XFinSequence; :: thesis: s is total
card s = n by CARD_1:def 7;
hence dom s = n ; :: according to PARTFUN1:def 2 :: thesis: verum