let f be constant standard special_circular_sequence; :: thesis: for g being FinSequence of (TOP-REAL 2)
for i1, i2 being 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 Nat st g is_a_part>_of f,i1,i2 holds
Rev g is_a_part<_of f,i2,i1
let i1, i2 be Nat; :: thesis: ( g is_a_part>_of f,i1,i2 implies Rev g is_a_part<_of f,i2,i1 )
A1: len g = len (Rev g) by FINSEQ_5:def 3;
assume A2: g is_a_part>_of f,i1,i2 ; :: thesis: Rev g is_a_part<_of f,i2,i1
then A3: 1 <= len g ;
A4: len g < len f by A2;
A5: i1 + 1 <= len f by A2;
then (i1 + 1) - 1 <= (len f) - 1 by XREAL_1:9;
then A6: i1 <= (len f) -' 1 by A3, A4, XREAL_1:233, XXREAL_0:2;
A7: i1 < len f by A5, NAT_1:13;
A8: 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 that
A9: 1 <= i and
A10: i <= len (Rev g) ; :: thesis: (Rev g) . i = f . (S_Drop ((((len f) + i2) -' i),f))
len g <= (len g) + (i -' 1) by NAT_1:11;
then len g <= (len g) + (i - 1) by A9, XREAL_1:233;
then (len g) - (i - 1) <= ((len g) + (i - 1)) - (i - 1) by XREAL_1:9;
then ((len g) - i) + 1 <= len g ;
then A11: ((len g) -' i) + 1 <= len g by A1, A10, XREAL_1:233;
A12: 1 <= ((len g) -' i) + 1 by NAT_1:11;
A13: (Rev g) . i = g . (((len g) - i) + 1) by A1, A9, A10, FINSEQ_6:115
.= g . (((len g) -' i) + 1) by A1, A10, XREAL_1:233
.= f . (S_Drop (((i1 + (((len g) -' i) + 1)) -' 1),f)) by A2, A12, A11 ;

now :: thesis: ( ( i1 <= i2 & (Rev g) . i = f . (S_Drop ((((len f) + i2) -' i),f)) ) or ( i1 > i2 & (Rev g) . i = f . (S_Drop ((((len f) + i2) -' i),f)) ) )

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

case A14: 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 A2, Th25;
then ((len f) - 1) + (len g) = (len f) + (i2 -' i1) ;
then ((len f) - 1) + (len g) = (len f) + (i2 - i1) by A14, XREAL_1:233;
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 A4, A1, A10, NAT_D:37, XXREAL_0:2;
then ((len f) + i2) -' i = ((len f) - 1) + (((i1 + ((len g) -' i)) + 1) - 1) by A1, A10, XREAL_1:233;
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, A4, XREAL_1:233, XXREAL_0:2;
hence (Rev g) . i = f . (S_Drop ((((len f) + i2) -' i),f)) by A13, Th23; :: 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 A2, Th26;
then (len g) + i1 = (((len f) + i2) - i1) + i1 by A7, NAT_D:37;
then ((len f) + i2) -' i = (i1 + (len g)) - i by A1, A10, NAT_D:37;
then ((len f) + i2) -' i = i1 + ((len g) - i) ;
then ((len f) + i2) -' i = ((i1 + ((len g) -' i)) + 1) - 1 by A1, A10, XREAL_1:233;
hence (Rev g) . i = f . (S_Drop ((((len f) + i2) -' i),f)) by A13, NAT_D:37; :: thesis: verum

end;

end;

end;

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

end;

A15: i2 + 1 <= len f by A2;
A16: 1 <= i1 by A2;
A17: (Rev g) . (len (Rev g)) = (Rev g) . (len g) by FINSEQ_5:def 3
.= g . (((len g) - (len g)) + 1) by A3, FINSEQ_6:115
.= f . (S_Drop (((i1 + 1) -' 1),f)) by A2
.= f . (S_Drop (i1,f)) by NAT_D:34 ;

A18: now :: thesis: ( ( i1 mod ((len f) -' 1) <> 0 & (Rev g) . (len (Rev g)) = f . i1 ) or ( i1 mod ((len f) -' 1) = 0 & (Rev g) . (len (Rev g)) = f . i1 ) )

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

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

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

end;

case A21: 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 A16, A17, A6, A21, Th4; :: thesis: verum

end;

end;

end;

1 <= i2 by A2;
hence Rev g is_a_part<_of f,i2,i1 by A16, A5, A15, A3, A4, A1, A18, A8; :: thesis: verum