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 Z: for n being Nat holds s . n in Y ; :: thesis: rng s c= Y
let y be set ; :: 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 set such that
W1: x in dom s and
W2: y = s . x by FUNCT_1:def 5;
x in NAT by W1, FUNCT_2:def 1;
hence y in Y by Z, W2; :: thesis: verum