set A1 = NAT --> the Element of F;
reconsider A1 = NAT --> the Element of F as SetSequence of X by FUNCOP_1:45;
take A1 ; :: thesis: A1 is F -valued
thus A1 is F -valued ; :: thesis: verum