theorem :: MODELC_2:82

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