let n be Nat; :: thesis: for x being n -element FinSequence holds dom x = Seg n
let x be n -element FinSequence; :: thesis: dom x = Seg n
len x = n by CARD_1:def 13;
hence dom x = Seg n by FINSEQ_1:def 3; :: thesis: verum