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 ( p . i in rng p & rng p c= D ) by FINSEQ_1:def 4, FUNCT_1:def 5;
hence p . i in D ; :: thesis: verum