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
A1: f in D * and
A2: x in dom f ; :: thesis: f . x in D
f is FinSequence of D by A1, Def11;
then A3: rng f c= D by Def4;
f . x in rng f by A2, FUNCT_1:3;
hence f . x in D by A3; :: thesis: verum