let i be Nat; :: thesis: for D being set
for p being FinSequence of D st i in dom p holds
p . i in D
let D be set ; :: thesis: for p being FinSequence of D st i in dom p holds
p . i in D
let p be FinSequence of D; :: thesis: ( i in dom p implies p . i in D )
assume i in dom p ; :: thesis: p . i in D
then A1: p . i in rng p by FUNCT_1:def 3;
rng p c= D by FINSEQ_1:def 4;
hence p . i in D by A1; :: thesis: verum