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 (((len f) + i1) -' i),f) ) ) by Def3;
then A3: 1 < len f by XXREAL_0:2;
A4: i2 < 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 (((len f) + i1) -' 1),f) by A2
.= f . (S_Drop (((len f) -' 1) + i1),f) by A3, NAT_D:38 ;
(i1 + 1) - 1 <= (len f) - 1 by A2, XREAL_1:11;
then A7: i1 <= (len f) -' 1 by A3, XREAL_1:235;
A8: S_Drop (((len f) -' 1) + i1),f = S_Drop i1,f by Th35;

A9: now

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

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

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

end;

case A12: 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, A8, A12, Th9; :: thesis: verum

end;

end;

end;

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

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (Rev g) implies (Rev g) . i = f . (S_Drop ((i2 + i) -' 1),f) )
assume A13: ( 1 <= i & i <= len (Rev g) ) ; :: thesis: (Rev g) . i = f . (S_Drop ((i2 + i) -' 1),f)
A14: 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 A13, 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 A15: ( 1 <= ((len g) -' i) + 1 & ((len g) -' i) + 1 <= len g ) by A5, A13, NAT_1:11, XREAL_1:235;
A16: (Rev g) . i = g . (((len g) - i) + 1) by A5, A13, A14, JORDAN3:24
.= g . (((len g) -' i) + 1) by A5, A13, XREAL_1:235
.= f . (S_Drop (((len f) + i1) -' (((len g) -' i) + 1)),f) by A1, A15, Def3 ;
A17: (len g) + 1 <= len f by A2, NAT_1:13;
(len g) + 1 <= ((len g) + 1) + i by NAT_1:11;
then ((len g) + 1) - i <= (((len g) + 1) + i) - i by XREAL_1:11;
then ((len g) - i) + 1 <= (len g) + 1 ;
then A18: ((len g) -' i) + 1 <= (len g) + 1 by A5, A13, XREAL_1:235;

now

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

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

then len g = ((len f) + i1) -' i2 by A1, Th40;
then A19: len g = ((len f) + i1) - i2 by A4, NAT_D:37;
len f = ((len f) -' 1) + 1 by A3, XREAL_1:237;
then ((- (len f)) + i2) + i = ((i2 + i) - 1) - ((len f) -' 1) ;
then i1 - ((len g) - i) = ((i2 + i) -' 1) - ((len f) -' 1) by A2, A19, NAT_D:37;
then i1 - ((len g) -' i) = ((i2 + i) -' 1) - ((len f) -' 1) by A5, A13, XREAL_1:235;
then ((((len f) -' 1) + 1) + i1) - (((len g) -' i) + 1) = (((len f) -' 1) + ((i2 + i) -' 1)) - ((len f) -' 1) ;
then ((len f) + i1) - (((len g) -' i) + 1) = (((len f) -' 1) + ((i2 + i) -' 1)) - ((len f) -' 1) by A3, XREAL_1:237;
hence (Rev g) . i = f . (S_Drop ((i2 + i) -' 1),f) by A16, A17, A18, NAT_D:37, XXREAL_0:2; :: thesis: verum

end;

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

then len g = (i1 -' i2) + 1 by A1, Th39;
then len g = (i1 - i2) + 1 by A20, XREAL_1:235;
then i1 - ((len g) - i) = (i2 + i) - 1 ;
then i1 - ((len g) - i) = (i2 + i) -' 1 by A13, NAT_D:37;
then i1 - ((len g) -' i) = (i2 + i) -' 1 by A5, A13, XREAL_1:235;
then ((len f) - 1) + (i1 - ((len g) -' i)) = ((i2 + i) -' 1) + ((len f) -' 1) by A3, XREAL_1:235;
then ((len f) + i1) - (((len g) -' i) + 1) = ((i2 + i) -' 1) + ((len f) -' 1) ;
then (Rev g) . i = f . (S_Drop (((i2 + i) -' 1) + ((len f) -' 1)),f) by A16, A17, A18, NAT_D:37, XXREAL_0:2
.= f . (S_Drop ((i2 + i) -' 1),f) by Th35 ;
hence (Rev g) . i = f . (S_Drop ((i2 + i) -' 1),f) ; :: thesis: verum

end;

end;

end;

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

end;

hence Rev g is_a_part>_of f,i2,i1 by A2, A5, A9, Def2; :: thesis: verum