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 Th6;

A3: rng (Incr (X_axis ff)) = rng (X_axis ff) by SEQ_4:def 21

.= rng (X_axis f) by A2, FINSEQ_5:57 ;

len (Incr (X_axis ff)) = card (rng (X_axis ff)) by SEQ_4:def 21

.= card (rng (X_axis f)) by A2, FINSEQ_5:57 ;

then A4: Incr (X_axis f) = Incr (X_axis ff) by A3, SEQ_4:def 21;

A5: Rev (Y_axis f) = Y_axis ff by A1, Th7;

A6: rng (Incr (Y_axis ff)) = rng (Y_axis ff) by SEQ_4:def 21

.= rng (Y_axis f) by A5, FINSEQ_5:57 ;

len (Incr (Y_axis ff)) = card (rng (Y_axis ff)) by SEQ_4:def 21

.= card (rng (Y_axis f)) by A5, FINSEQ_5:57 ;

then Incr (Y_axis f) = Incr (Y_axis ff) by A6, SEQ_4:def 21;

hence GoB ff = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by A4, GOBOARD2:def 2

.= GoB f by GOBOARD2:def 2 ;

:: thesis: verum

assume A1: ff = Rev f ; :: thesis: GoB ff = GoB f

then A2: Rev (X_axis f) = X_axis ff by Th6;

A3: rng (Incr (X_axis ff)) = rng (X_axis ff) by SEQ_4:def 21

.= rng (X_axis f) by A2, FINSEQ_5:57 ;

len (Incr (X_axis ff)) = card (rng (X_axis ff)) by SEQ_4:def 21

.= card (rng (X_axis f)) by A2, FINSEQ_5:57 ;

then A4: Incr (X_axis f) = Incr (X_axis ff) by A3, SEQ_4:def 21;

A5: Rev (Y_axis f) = Y_axis ff by A1, Th7;

A6: rng (Incr (Y_axis ff)) = rng (Y_axis ff) by SEQ_4:def 21

.= rng (Y_axis f) by A5, FINSEQ_5:57 ;

len (Incr (Y_axis ff)) = card (rng (Y_axis ff)) by SEQ_4:def 21

.= card (rng (Y_axis f)) by A5, FINSEQ_5:57 ;

then Incr (Y_axis f) = Incr (Y_axis ff) by A6, SEQ_4:def 21;

hence GoB ff = GoB ((Incr (X_axis f)),(Incr (Y_axis f))) by A4, GOBOARD2:def 2

.= GoB f by GOBOARD2:def 2 ;

:: thesis: verum