:: deftheorem defines Inf_seq MODELC_2:def 39 :
for S being non empty set holds Inf_seq S = Funcs (NAT,S);