theorem :: MODELC_2:81

for S being non empty set
for seq being sequence of S holds CastSeq ((CastSeq seq),S) = seq by Def41;