let f be FinSequence of (TOP-REAL 2); Rev (X_axis f) = X_axis (Rev f)
A1: len (Rev (X_axis f)) =
len (X_axis f)
by FINSEQ_5:def 3
.=
len f
by GOBOARD1:def 1
.=
len (Rev f)
by FINSEQ_5:def 3
;
len (X_axis f) = len f
by GOBOARD1:def 1;
then A2:
dom (X_axis f) = dom f
by FINSEQ_3:29;
A3:
len f = len (Rev f)
by FINSEQ_5:def 3;
now for k being Nat st k in dom (Rev (X_axis f)) holds
(Rev (X_axis f)) . k = ((Rev f) /. k) `1 let k be
Nat;
( k in dom (Rev (X_axis f)) implies (Rev (X_axis f)) . k = ((Rev f) /. k) `1 )assume A4:
k in dom (Rev (X_axis f))
;
(Rev (X_axis f)) . k = ((Rev f) /. k) `1 set l =
((len f) + 1) -' k;
A5:
k <= len f
by A1, A3, A4, FINSEQ_3:25;
len f < (len f) + 1
by NAT_1:13;
then A6:
(((len f) + 1) -' k) + k = (len f) + 1
by A5, XREAL_1:235, XXREAL_0:2;
A7:
Rev (Rev (X_axis f)) = X_axis f
;
then A8:
((len f) + 1) -' k in dom (X_axis f)
by A1, A3, A4, A6, FINSEQ_5:59;
thus (Rev (X_axis f)) . k =
(Rev (X_axis f)) /. k
by A4, PARTFUN1:def 6
.=
(X_axis f) /. (((len f) + 1) -' k)
by A1, A3, A4, A6, A7, FINSEQ_5:66
.=
(X_axis f) . (((len f) + 1) -' k)
by A8, PARTFUN1:def 6
.=
(f /. (((len f) + 1) -' k)) `1
by A8, GOBOARD1:def 1
.=
((Rev f) /. k) `1
by A1, A2, A3, A4, A6, A7, FINSEQ_5:59, FINSEQ_5:66
;
verum end;
hence
Rev (X_axis f) = X_axis (Rev f)
by A1, GOBOARD1:def 1; verum