let i be natural Number ; :: thesis: for D being set
for p being b₁ -valued FinSequence st i in dom p holds
p . i in D
let D be set ; :: thesis: for p being D -valued FinSequence st i in dom p holds
p . i in D
let p be D -valued FinSequence; :: 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 RELAT_1:def 19;
hence p . i in D by A1; :: thesis: verum