let i be Nat; :: thesis: for D being non empty set
for M being FinSequence of D * holds M . i is FinSequence of D
let D be non empty set ; :: thesis: for M being FinSequence of D * holds M . i is FinSequence of D
let M be FinSequence of D * ; :: thesis: M . i is FinSequence of D

per cases ( not i in dom M or i in dom M ) ;

suppose not i in dom M ; :: thesis: M . i is FinSequence of D

then M . i = <*> D by FUNCT_1:def 2;
hence M . i is FinSequence of D ; :: thesis: verum

end;

suppose A1: i in dom M ; :: thesis: M . i is FinSequence of D

A2: rng M c= D * by FINSEQ_1:def 4;
M . i in rng M by A1, FUNCT_1:def 3;
hence M . i is FinSequence of D by A2, FINSEQ_1:def 11; :: thesis: verum

end;

end;