set A1 = NAT --> X;
X in bool X by ZFMISC_1:def 1;
then reconsider A1 = NAT --> X as SetSequence of X by FUNCOP_1:57;
take A1 ; :: thesis: A1 is Si -valued
( X in Si & rng A1 = {X} ) by Th11, FUNCOP_1:14;
then rng A1 c= Si by ZFMISC_1:37;
hence A1 is Si -valued by RELAT_1:def 19; :: thesis: verum