let f, ff be non empty FinSequence of (TOP-REAL 2); ( ff = Rev f implies GoB ff = GoB f )
assume A1:
ff = Rev f
; 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
;
verum