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

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

hence
NAT --> X is Set_Sequence of F
by Def2; :: thesis: verum
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;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