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