let n be Nat; :: thesis: for f being n -long FinSequence holds dom f = Seg n
let f be n -long FinSequence; :: thesis: dom f = Seg n
len f = n by Def18;
hence dom f = Seg n by Def3; :: thesis: verum