let f be FinSequence of (TOP-REAL 2); :: thesis: 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 3
.= len (Rev f) by FINSEQ_5:def 3 ;
len (X_axis f) = len f by GOBOARD1:def 3;
then A2: dom (X_axis f) = dom f by FINSEQ_3:31;
A3: len f = len (Rev f) by FINSEQ_5:def 3;

now

let k be Element of NAT ; :: thesis: ( 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)) ; :: thesis: (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:27;
len f < (len f) + 1 by NAT_1:13;
then A6: (((len f) + 1) -' k) + k = (len f) + 1 by A5, XREAL_1:237, XXREAL_0:2;
A7: Rev (Rev (X_axis f)) = X_axis f by FINSEQ_6:29;
then A8: ((len f) + 1) -' k in dom (X_axis f) by A1, A3, A4, A6, FINSEQ_5:62;
thus (Rev (X_axis f)) . k = (Rev (X_axis f)) /. k by A4, PARTFUN1:def 8
.= (X_axis f) /. (((len f) + 1) -' k) by A1, A3, A4, A6, A7, FINSEQ_5:69
.= (X_axis f) . (((len f) + 1) -' k) by A8, PARTFUN1:def 8
.= (f /. (((len f) + 1) -' k)) `1 by A8, GOBOARD1:def 3
.= ((Rev f) /. k) `1 by A1, A2, A3, A4, A6, A7, FINSEQ_5:62, FINSEQ_5:69 ; :: thesis: verum

end;

hence Rev (X_axis f) = X_axis (Rev f) by A1, GOBOARD1:def 3; :: thesis: verum