let n be Nat; :: thesis: for D being set
for e1 being FinSequence of D holds n |-> e1 is FinSequence of D *
let D be set ; :: thesis: for e1 being FinSequence of D holds n |-> e1 is FinSequence of D *
let e1 be FinSequence of D; :: thesis: n |-> e1 is FinSequence of D *
e1 in D * by FINSEQ_1:def 11;
hence n |-> e1 is FinSequence of D * by FINSEQ_2:63; :: thesis: verum