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

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