:: deftheorem defines CastSeq MODELC_2:def 40 :
for S being non empty set
for t being sequence of S holds CastSeq t = t;