let n be Nat; :: thesis: for f being n -element FinSequence holds dom f = Seg n
let f be n -element FinSequence; :: thesis: dom f = Seg n
len f = n by CARD_1:def 7;
hence dom f = Seg n by Def3; :: thesis: verum