let x, D be set ; :: thesis: for f being Function st f in D * & x in dom f holds
f . x in D
let f be Function; :: thesis: ( f in D * & x in dom f implies f . x in D )
assume that
Z1: f in D * and
Z2: x in dom f ; :: thesis: f . x in D
f is FinSequence of D by Z1, Def11;
then A: rng f c= D by Def4;
f . x in rng f by Z2, FUNCT_1:12;
hence f . x in D by A; :: thesis: verum