theorem Th7: :: GOBOARD9:8
for f being FinSequence of (TOP-REAL 2) holds Rev (Y_axis f) = Y_axis (Rev f)