let x be object ; :: thesis: for D being set
for f being Function st f in D * & x in dom f holds
f . x in D
let 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 rng f c= D by Def4;
hence f . x in D by A2, FUNCT_1:3; :: thesis: verum