let Y be set ; :: thesis: for X being non empty set
for s being sequence of X st ( for n being Nat holds s . n in Y ) holds
rng s c= Y
let X be non empty set ; :: thesis: for s being sequence of X st ( for n being Nat holds s . n in Y ) holds
rng s c= Y
let s be sequence of X; :: thesis: ( ( for n being Nat holds s . n in Y ) implies rng s c= Y )
assume A1: for n being Nat holds s . n in Y ; :: thesis: rng s c= Y
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng s or y in Y )
assume y in rng s ; :: thesis: y in Y
then consider x being object such that
A2: x in dom s and
A3: y = s . x by FUNCT_1:def 3;
x in NAT by A2, FUNCT_2:def 1;
hence y in Y by A1, A3; :: thesis: verum