:: deftheorem Def41 defines CastSeq MODELC_2:def 41 :
for S being non empty set
for t being object st t is Element of Inf_seq S holds
CastSeq (t,S) = t;