let X be set ; :: thesis: for F being Field_Subset of X holds NAT --> X is Set_Sequence of F
let F be Field_Subset of X; :: thesis: NAT --> X is Set_Sequence of F
X in bool X by ZFMISC_1:def 1;
then reconsider G0 = NAT --> X as SetSequence of X by FUNCOP_1:45;
A1: rng (NAT --> X) = {X} by FUNCOP_1:8;
for n being Nat holds G0 . n in F
proof
let n be Nat; :: thesis: G0 . n in F
n in NAT by ORDINAL1:def 12;
then G0 . n in {X} by A1, FUNCT_2:4;
then G0 . n = X by TARSKI:def 1;
hence G0 . n in F by PROB_1:5; :: thesis: verum
end;
hence NAT --> X is Set_Sequence of F by Def2; :: thesis: verum