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