theorem Th18: :: MSAFREE5:13

for I, J being FinSequence-membered set
for f being FinSequence holds
( I c= J iff f ^^ I c= f ^^ J )