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: X in Si by Th11;
rng A1 = {X} by FUNCOP_1:14;
then rng A1 c= Si by X, ZFMISC_1:37;
hence A1 is Si -valued by RELAT_1:def 19; :: thesis: verum