let f, ff be non empty FinSequence of (TOP-REAL 2); :: thesis: ( ff = Rev f implies GoB ff = GoB f )
assume A1: ff = Rev f ; :: thesis: GoB ff = GoB f
then A2: Rev (X_axis f) = X_axis ff by Th10;
A3: rng (Incr (X_axis ff)) = rng (X_axis ff) by GOBOARD2:def 2
.= rng (X_axis f) by A2, FINSEQ_5:60 ;
len (Incr (X_axis ff)) = card (rng (X_axis ff)) by GOBOARD2:def 2
.= card (rng (X_axis f)) by A2, FINSEQ_5:60 ;
then A4: Incr (X_axis f) = Incr (X_axis ff) by A3, GOBOARD2:def 2;
A5: Rev (Y_axis f) = Y_axis ff by A1, Th11;
A6: rng (Incr (Y_axis ff)) = rng (Y_axis ff) by GOBOARD2:def 2
.= rng (Y_axis f) by A5, FINSEQ_5:60 ;
len (Incr (Y_axis ff)) = card (rng (Y_axis ff)) by GOBOARD2:def 2
.= card (rng (Y_axis f)) by A5, FINSEQ_5:60 ;
then Incr (Y_axis f) = Incr (Y_axis ff) by A6, GOBOARD2:def 2;
hence GoB ff = GoB (Incr (X_axis f)),(Incr (Y_axis f)) by A4, GOBOARD2:def 3
.= GoB f by GOBOARD2:def 3 ;
:: thesis: verum