let f be V26() 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: 1 <= i2 by A2;
A5: len g < len f by A2;
A6: i2 + 1 <= len f by A2;
then A7: i2 < len f by NAT_1:13;
A8: 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 that
A9: 1 <= i and
A10: i <= len (Rev g) ; :: thesis: (Rev g) . i = f . (S_Drop (((i2 + i) -' 1),f))
A11: 1 <= ((len g) -' i) + 1 by NAT_1:11;
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 A12: ((len g) -' i) + 1 <= len g by A1, A10, XREAL_1:233;
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 ((((len f) + i1) -' (((len g) -' i) + 1)),f)) by A2, A11, A12 ;
(len g) + 1 <= ((len g) + 1) + i by NAT_1:11;
then ((len g) + 1) - i <= (((len g) + 1) + i) - i by XREAL_1:9;
then ((len g) - i) + 1 <= (len g) + 1 ;
then A14: ((len g) -' i) + 1 <= (len g) + 1 by A1, A10, XREAL_1:233;
A15: (len g) + 1 <= len f by A5, NAT_1:13;
now :: thesis: ( ( i1 < i2 & (Rev g) . i = f . (S_Drop (((i2 + i) -' 1),f)) ) or ( i1 >= i2 & (Rev g) . i = f . (S_Drop (((i2 + i) -' 1),f)) ) )
per cases ( i1 < i2 or i1 >= i2 ) ;
case A16: i1 < i2 ; :: thesis: (Rev g) . i = f . (S_Drop (((i2 + i) -' 1),f))
len f = ((len f) -' 1) + 1 by A3, A5, XREAL_1:235, XXREAL_0:2;
then A17: ((- (len f)) + i2) + i = ((i2 + i) - 1) - ((len f) -' 1) ;
len g = ((len f) + i1) -' i2 by A2, A16, Th28;
then len g = ((len f) + i1) - i2 by A7, NAT_D:37;
then i1 - ((len g) - i) = ((i2 + i) -' 1) - ((len f) -' 1) by A4, A17, NAT_D:37;
then i1 - ((len g) -' i) = ((i2 + i) -' 1) - ((len f) -' 1) by A1, A10, XREAL_1:233;
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, A5, XREAL_1:235, XXREAL_0:2;
hence (Rev g) . i = f . (S_Drop (((i2 + i) -' 1),f)) by A13, A15, A14, NAT_D:37, XXREAL_0:2; :: thesis: verum
end;
case A18: i1 >= i2 ; :: thesis: (Rev g) . i = f . (S_Drop (((i2 + i) -' 1),f))
then len g = (i1 -' i2) + 1 by A2, Th27;
then len g = (i1 - i2) + 1 by A18, XREAL_1:233;
then i1 - ((len g) - i) = (i2 + i) - 1 ;
then i1 - ((len g) - i) = (i2 + i) -' 1 by A9, NAT_D:37;
then i1 - ((len g) -' i) = (i2 + i) -' 1 by A1, A10, XREAL_1:233;
then ((len f) - 1) + (i1 - ((len g) -' i)) = ((i2 + i) -' 1) + ((len f) -' 1) by A3, A5, XREAL_1:233, XXREAL_0:2;
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 A13, A15, A14, NAT_D:37, XXREAL_0:2
.= f . (S_Drop (((i2 + i) -' 1),f)) by Th23 ;
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;
A19: S_Drop ((((len f) -' 1) + i1),f) = S_Drop (i1,f) by Th23;
A20: i1 + 1 <= len f by A2;
then (i1 + 1) - 1 <= (len f) - 1 by XREAL_1:9;
then A21: i1 <= (len f) -' 1 by A3, A5, XREAL_1:233, XXREAL_0:2;
A22: 1 <= i1 by A2;
A23: (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 ((((len f) + i1) -' 1),f)) by A2
.= f . (S_Drop ((((len f) -' 1) + i1),f)) by A3, A5, NAT_D:38, XXREAL_0:2 ;
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 A24: i1 mod ((len f) -' 1) <> 0 ; :: thesis: (Rev g) . (len (Rev g)) = f . i1
then i1 <> (len f) -' 1 by NAT_D:25;
then A25: i1 < (len f) -' 1 by A21, XXREAL_0:1;
S_Drop (i1,f) = i1 mod ((len f) -' 1) by A24, Def1;
hence (Rev g) . (len (Rev g)) = f . i1 by A23, A19, A25, NAT_D:24; :: thesis: verum
end;
case A26: 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 A22, A23, A21, A19, A26, Th4; :: thesis: verum
end;
end;
end;
hence Rev g is_a_part>_of f,i2,i1 by A22, A20, A4, A6, A3, A5, A1, A8; :: thesis: verum