let f be non constant standard special_circular_sequence; :: thesis: for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part>_of f,i1,i2 holds
Rev g is_a_part<_of f,i2,i1
let g be FinSequence of (TOP-REAL 2); :: thesis: for i1, i2 being Element of NAT st g is_a_part>_of f,i1,i2 holds
Rev g is_a_part<_of f,i2,i1
let i1, i2 be Element of NAT ; :: thesis: ( g is_a_part>_of f,i1,i2 implies Rev g is_a_part<_of f,i2,i1 )
assume A1: g is_a_part>_of f,i1,i2 ; :: thesis: Rev g is_a_part<_of f,i2,i1
then A2: ( 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f & g . (len g) = f . i2 & 1 <= len g & len g < len f & ( for i being Element of NAT st 1 <= i & i <= len g holds
g . i = f . (S_Drop ((i1 + i) -' 1),f) ) ) by Def2;
then A3: 1 < len f by XXREAL_0:2;
A4: i1 < len f by A2, NAT_1:13;
A5: len g = len (Rev g) by FINSEQ_5:def 3;
A6: (Rev g) . (len (Rev g)) = (Rev g) . (len g) by FINSEQ_5:def 3
.= g . (((len g) - (len g)) + 1) by A2, JORDAN3:24
.= f . (S_Drop ((i1 + 1) -' 1),f) by A2
.= f . (S_Drop i1,f) by NAT_D:34 ;
(i1 + 1) - 1 <= (len f) - 1 by A2, XREAL_1:11;
then A7: i1 <= (len f) -' 1 by A3, XREAL_1:235;

A8: now

per cases ( i1 mod ((len f) -' 1) <> 0 or i1 mod ((len f) -' 1) = 0 ) ;

case A9: i1 mod ((len f) -' 1) <> 0 ; :: thesis: (Rev g) . (len (Rev g)) = f . i1

then A10: S_Drop i1,f = i1 mod ((len f) -' 1) by Def1;
i1 <> (len f) -' 1 by A9, NAT_D:25;
then i1 < (len f) -' 1 by A7, XXREAL_0:1;
hence (Rev g) . (len (Rev g)) = f . i1 by A6, A10, NAT_D:24; :: thesis: verum

end;

case A11: i1 mod ((len f) -' 1) = 0 ; :: thesis: (Rev g) . (len (Rev g)) = f . i1

then S_Drop i1,f = (len f) -' 1 by Def1;
hence (Rev g) . (len (Rev g)) = f . i1 by A2, A6, A7, A11, Th9; :: thesis: verum

end;

end;

end;

for i being Nat st 1 <= i & i <= len (Rev g) holds
(Rev g) . i = f . (S_Drop (((len f) + i2) -' i),f)

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (Rev g) implies (Rev g) . i = f . (S_Drop (((len f) + i2) -' i),f) )
assume A12: ( 1 <= i & i <= len (Rev g) ) ; :: thesis: (Rev g) . i = f . (S_Drop (((len f) + i2) -' i),f)
A13: i in NAT by ORDINAL1:def 13;
len g <= (len g) + (i -' 1) by NAT_1:11;
then len g <= (len g) + (i - 1) by A12, XREAL_1:235;
then (len g) - (i - 1) <= ((len g) + (i - 1)) - (i - 1) by XREAL_1:11;
then ((len g) - i) + 1 <= len g ;
then A14: ( 1 <= ((len g) -' i) + 1 & ((len g) -' i) + 1 <= len g ) by A5, A12, NAT_1:11, XREAL_1:235;
A15: (Rev g) . i = g . (((len g) - i) + 1) by A5, A12, A13, JORDAN3:24
.= g . (((len g) -' i) + 1) by A5, A12, XREAL_1:235
.= f . (S_Drop ((i1 + (((len g) -' i) + 1)) -' 1),f) by A1, A14, Def2 ;
A16: i < len f by A2, A5, A12, XXREAL_0:2;

now

per cases ( i1 <= i2 or i1 > i2 ) ;

case A17: i1 <= i2 ; :: thesis: (Rev g) . i = f . (S_Drop (((len f) + i2) -' i),f)

then ((len f) - 1) + (len g) = ((len f) - 1) + ((i2 -' i1) + 1) by A1, Th37;
then ((len f) - 1) + (len g) = (len f) + (i2 -' i1) ;
then ((len f) - 1) + (len g) = (len f) + (i2 - i1) by A17, XREAL_1:235;
then ((len f) + i2) - i = (((len f) - 1) + (i1 + (len g))) - i ;
then ((len f) + i2) -' i = ((len f) - 1) + (i1 + ((len g) - i)) by A16, NAT_D:37;
then ((len f) + i2) -' i = ((len f) - 1) + (((i1 + ((len g) -' i)) + 1) - 1) by A5, A12, XREAL_1:235;
then ((len f) + i2) -' i = ((len f) - 1) + ((i1 + (((len g) -' i) + 1)) -' 1) by NAT_D:37;
then ((len f) + i2) -' i = ((i1 + (((len g) -' i) + 1)) -' 1) + ((len f) -' 1) by A3, XREAL_1:235;
hence (Rev g) . i = f . (S_Drop (((len f) + i2) -' i),f) by A15, Th35; :: thesis: verum

end;

case i1 > i2 ; :: thesis: (Rev g) . i = f . (S_Drop (((len f) + i2) -' i),f)

then len g = ((len f) + i2) -' i1 by A1, Th38;
then (len g) + i1 = (((len f) + i2) - i1) + i1 by A4, NAT_D:37;
then ((len f) + i2) -' i = (i1 + (len g)) - i by A5, A12, NAT_D:37;
then ((len f) + i2) -' i = i1 + ((len g) - i) ;
then ((len f) + i2) -' i = ((i1 + ((len g) -' i)) + 1) - 1 by A5, A12, XREAL_1:235;
hence (Rev g) . i = f . (S_Drop (((len f) + i2) -' i),f) by A15, NAT_D:37; :: thesis: verum

end;

end;

end;

hence (Rev g) . i = f . (S_Drop (((len f) + i2) -' i),f) ; :: thesis: verum

end;

hence Rev g is_a_part<_of f,i2,i1 by A2, A5, A8, Def3; :: thesis: verum