let f be FinSequence of (TOP-REAL 2); :: thesis: Rev (Y_axis f) = Y_axis (Rev f)

A1: len (Rev (Y_axis f)) = len (Y_axis f) by FINSEQ_5:def 3

.= len f by GOBOARD1:def 2

.= len (Rev f) by FINSEQ_5:def 3 ;

len (Y_axis f) = len f by GOBOARD1:def 2;

then A2: dom (Y_axis f) = dom f by FINSEQ_3:29;

A3: len f = len (Rev f) by FINSEQ_5:def 3;

A1: len (Rev (Y_axis f)) = len (Y_axis f) by FINSEQ_5:def 3

.= len f by GOBOARD1:def 2

.= len (Rev f) by FINSEQ_5:def 3 ;

len (Y_axis f) = len f by GOBOARD1:def 2;

then A2: dom (Y_axis f) = dom f by FINSEQ_3:29;

A3: len f = len (Rev f) by FINSEQ_5:def 3;

now :: thesis: for k being Nat st k in dom (Rev (Y_axis f)) holds

(Rev (Y_axis f)) . k = ((Rev f) /. k) `2

hence
Rev (Y_axis f) = Y_axis (Rev f)
by A1, GOBOARD1:def 2; :: thesis: verum(Rev (Y_axis f)) . k = ((Rev f) /. k) `2

let k be Nat; :: thesis: ( k in dom (Rev (Y_axis f)) implies (Rev (Y_axis f)) . k = ((Rev f) /. k) `2 )

assume A4: k in dom (Rev (Y_axis f)) ; :: thesis: (Rev (Y_axis f)) . k = ((Rev f) /. k) `2

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 (Y_axis f)) = Y_axis f ;

then A8: ((len f) + 1) -' k in dom (Y_axis f) by A1, A3, A4, A6, FINSEQ_5:59;

thus (Rev (Y_axis f)) . k = (Rev (Y_axis f)) /. k by A4, PARTFUN1:def 6

.= (Y_axis f) /. (((len f) + 1) -' k) by A1, A3, A4, A6, A7, FINSEQ_5:66

.= (Y_axis f) . (((len f) + 1) -' k) by A8, PARTFUN1:def 6

.= (f /. (((len f) + 1) -' k)) `2 by A8, GOBOARD1:def 2

.= ((Rev f) /. k) `2 by A1, A2, A3, A4, A6, A7, FINSEQ_5:59, FINSEQ_5:66 ; :: thesis: verum

end;assume A4: k in dom (Rev (Y_axis f)) ; :: thesis: (Rev (Y_axis f)) . k = ((Rev f) /. k) `2

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 (Y_axis f)) = Y_axis f ;

then A8: ((len f) + 1) -' k in dom (Y_axis f) by A1, A3, A4, A6, FINSEQ_5:59;

thus (Rev (Y_axis f)) . k = (Rev (Y_axis f)) /. k by A4, PARTFUN1:def 6

.= (Y_axis f) /. (((len f) + 1) -' k) by A1, A3, A4, A6, A7, FINSEQ_5:66

.= (Y_axis f) . (((len f) + 1) -' k) by A8, PARTFUN1:def 6

.= (f /. (((len f) + 1) -' k)) `2 by A8, GOBOARD1:def 2

.= ((Rev f) /. k) `2 by A1, A2, A3, A4, A6, A7, FINSEQ_5:59, FINSEQ_5:66 ; :: thesis: verum