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

now

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

case A9: i1 <= i2 ; :: thesis: g1 . 2 <> g2 . 2

now

per cases ( i1 = i2 or i1 < i2 ) by A9, XXREAL_0:1;

case i1 = i2 ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;

case A10: i1 < i2 ; :: thesis: g1 . 2 <> g2 . 2

then A11: g2 = (mid f,i1,1) ^ (mid f,((len f) -' 1),i2) by A1, Th40;
(i1 + 1) - 1 <= (len f) - 1 by A2, XREAL_1:11;
then A12: 1 <= (len f) -' 1 by A2, A5, XXREAL_0:2;
A13: len (mid f,i1,1) = (i1 -' 1) + 1 by A2, A8, Th21;

now

per cases ( 1 < i1 or 1 = i1 ) by A2, XXREAL_0:1;

case A14: 1 < i1 ; :: thesis: g1 . 2 <> g2 . 2

then A15: 1 + 1 <= i1 by NAT_1:13;
1 + 1 <= (i1 - 1) + 1 by A14, NAT_1:13;
then A16: 2 <= len (mid f,i1,1) by A2, A13, XREAL_1:235;
A17: g2 . 2 = ((mid f,i1,1) ^ (mid f,((len f) -' 1),i2)) . 2 by A1, A10, Th40
.= (mid f,i1,1) . 2 by A16, FINSEQ_1:85
.= f . ((i1 -' 2) + 1) by A4, A8, A14, A16, JORDAN3:27
.= f . ((i1 - (1 + 1)) + 1) by A15, XREAL_1:235
.= f . (i1 - 1)
.= f . (i1 -' 1) by A2, XREAL_1:235 ;
i1 + 1 <= i2 by A10, NAT_1:13;
then (1 + i1) - i1 <= i2 - i1 by XREAL_1:11;
then 1 <= i2 -' i1 by NAT_D:39;
then 1 + 1 <= (i2 -' i1) + 1 by XREAL_1:8;
then A18: 2 <= len (mid f,i1,i2) by A2, A7, A8, A10, JORDAN3:27;
A19: g1 . 2 = (mid f,i1,i2) . 2 by A1, A10, Th37
.= f . ((2 + i1) -' 1) by A2, A7, A8, A10, A18, JORDAN3:27
.= f . (((1 + 1) + i1) - 1) by NAT_D:37
.= f . (i1 + 1) ;
1 + 1 <= i1 by A14, NAT_1:13;
then A20: (1 + 1) - 1 <= i1 - 1 by XREAL_1:11;
then A21: 1 <= i1 -' 1 by NAT_D:39;

A22: now

assume A23: ( 1 = i1 -' 1 & i1 + 1 = len f ) ; :: thesis: contradiction
then 1 = i1 - 1 by NAT_D:39;
hence contradiction by A23, GOBOARD7:36; :: thesis: verum

end;

now

per cases ( 1 <> i1 -' 1 or i1 + 1 <> len f ) by A22;

case A24: 1 <> i1 -' 1 ; :: thesis: g1 . 2 <> g2 . 2

i1 -' 1 < (i1 -' 1) + 1 by NAT_1:13;
then i1 -' 1 < i1 by A2, XREAL_1:237;
then A25: ( 1 < i1 -' 1 & i1 -' 1 < i1 + 1 & i1 + 1 <= len f ) by A1, A21, A24, Def2, NAT_1:13, XXREAL_0:1;
then A26: f /. (i1 -' 1) <> f /. (i1 + 1) by GOBOARD7:39;
i1 -' 1 < len f by A25, XXREAL_0:2;
then A27: f . (i1 -' 1) = f /. (i1 -' 1) by A21, FINSEQ_4:24;
1 < i1 + 1 by A2, NAT_1:13;
hence g1 . 2 <> g2 . 2 by A2, A17, A19, A26, A27, FINSEQ_4:24; :: thesis: verum

end;

case A28: i1 + 1 <> len f ; :: thesis: g1 . 2 <> g2 . 2

i1 -' 1 < (i1 -' 1) + 1 by NAT_1:13;
then i1 -' 1 < i1 by A2, XREAL_1:237;
then A29: ( 1 <= i1 -' 1 & i1 -' 1 < i1 + 1 & i1 + 1 < len f ) by A2, A20, A28, NAT_1:13, NAT_D:39, XXREAL_0:1;
then A30: f /. (i1 -' 1) <> f /. (i1 + 1) by GOBOARD7:38;
i1 -' 1 < len f by A29, XXREAL_0:2;
then A31: f . (i1 -' 1) = f /. (i1 -' 1) by A29, FINSEQ_4:24;
1 < i1 + 1 by A2, NAT_1:13;
hence g1 . 2 <> g2 . 2 by A2, A17, A19, A30, A31, FINSEQ_4:24; :: thesis: verum

end;

end;

end;

hence g1 . 2 <> g2 . 2 ; :: thesis: verum

end;

case A32: 1 = i1 ; :: thesis: g1 . 2 <> g2 . 2

A33: len (mid f,i1,1) = (i1 -' 1) + 1 by A2, A8, Th21
.= 0 + 1 by A32, XREAL_1:234
.= 1 ;
A34: len g2 = ((len f) + i1) -' i2 by A1, A10, Th40
.= ((len f) + 1) - i2 by A7, A32, NAT_D:37 ;
(i2 + 1) + 1 <= (len f) + 1 by A2, XREAL_1:8;
then A35: ((1 + i2) + 1) - i2 <= ((len f) + 1) - i2 by XREAL_1:11;
A36: len (mid f,i1,1) = (i1 -' 1) + 1 by A2, A8, Th21
.= 0 + 1 by A32, XREAL_1:234
.= 1 ;
A37: g2 . 2 = (mid f,((len f) -' 1),i2) . (2 - (len (mid f,i1,1))) by A11, A33, A34, A35, JORDAN3:15
.= f . ((len f) -' 1) by A2, A5, A6, A7, A12, A36, JORDAN3:27 ;
i1 + 1 <= i2 by A10, NAT_1:13;
then (1 + i1) - i1 <= i2 - i1 by XREAL_1:11;
then 1 <= i2 -' i1 by NAT_D:39;
then 1 + 1 <= (i2 -' i1) + 1 by XREAL_1:8;
then A38: 2 <= len (mid f,i1,i2) by A2, A7, A8, A10, JORDAN3:27;
A39: g1 . 2 = (mid f,i1,i2) . 2 by A1, A10, Th37
.= f . ((2 + i1) -' 1) by A2, A7, A8, A10, A38, JORDAN3:27
.= f . (((1 + 1) + i1) - 1) by NAT_D:37
.= f . (i1 + 1) ;
len f > 4 by GOBOARD7:36;
then (len f) - 1 > (3 + 1) - 1 by XREAL_1:11;
then i1 + 1 < (len f) -' 1 by A5, A32, XXREAL_0:2;
then A40: f /. (i1 + 1) <> f /. ((len f) -' 1) by A5, A6, A32, GOBOARD7:39;
A41: f . ((len f) -' 1) = f /. ((len f) -' 1) by A5, A6, A12, FINSEQ_4:24;
1 < i1 + 1 by A2, NAT_1:13;
hence g1 . 2 <> g2 . 2 by A2, A37, A39, A40, A41, FINSEQ_4:24; :: thesis: verum

end;

end;

end;

hence g1 . 2 <> g2 . 2 ; :: thesis: verum

end;

end;

end;

hence g1 . 2 <> g2 . 2 ; :: thesis: verum

end;

case A42: i1 > i2 ; :: thesis: g1 . 2 <> g2 . 2

then A43: g1 = (mid f,i1,((len f) -' 1)) ^ (mid f,1,i2) by A1, Th38;
1 < i1 by A2, A42, XXREAL_0:2;
then A44: 1 + 1 <= i1 by NAT_1:13;
A45: (i1 + 1) - 1 <= (len f) - 1 by A2, XREAL_1:11;
then 1 <= (len f) -' 1 by A2, A5, XXREAL_0:2;
then A46: len (mid f,i1,((len f) -' 1)) = (((len f) -' 1) -' i1) + 1 by A2, A5, A6, A8, A45, JORDAN3:27;
A47: (i1 + 1) - 1 <= (len f) - 1 by A2, XREAL_1:11;

A48: now

per cases ( i1 < (len f) - 1 or i1 = (len f) - 1 ) by A45, XXREAL_0:1;

case i1 < (len f) - 1 ; :: thesis: g1 . 2 = f . (i1 + 1)

then i1 + 1 <= (len f) -' 1 by A5, NAT_1:13;
then A49: 1 + (i1 + 1) <= 1 + ((len f) -' 1) by XREAL_1:8;
then A50: (1 + (i1 + 1)) - i1 <= (1 + ((len f) -' 1)) - i1 by XREAL_1:11;
((1 + 1) + i1) - i1 <= (1 + ((len f) -' 1)) - i1 by A49, XREAL_1:11;
then 1 + 1 <= 1 + (((len f) -' 1) - i1) ;
then A51: 2 <= len (mid f,i1,((len f) -' 1)) by A5, A46, A47, XREAL_1:235;
thus g1 . 2 = ((mid f,i1,((len f) -' 1)) ^ (mid f,1,i2)) . 2 by A1, A42, Th38
.= (mid f,i1,((len f) -' 1)) . 2 by A51, FINSEQ_1:85
.= f . (((1 + 1) + i1) - 1) by A2, A5, A6, A47, A50, JORDAN3:31
.= f . (i1 + 1) ; :: thesis: verum

end;

case A52: i1 = (len f) - 1 ; :: thesis: g1 . 2 = f . (i1 + 1)

then A53: len (mid f,i1,((len f) -' 1)) = (((len f) -' 1) -' ((len f) -' 1)) + 1 by A2, A5, A6, JORDAN3:27
.= 0 + 1 by XREAL_1:234
.= 1 ;
A54: len g1 = ((((len f) -' 1) + 1) + i2) -' ((len f) -' 1) by A1, A5, A42, A52, Th38
.= (((len f) -' 1) + (1 + i2)) -' ((len f) -' 1)
.= 1 + i2 by NAT_D:34 ;
A55: 1 + 1 <= i2 + 1 by A2, XREAL_1:8;
A56: len (mid f,i1,((len f) -' 1)) = (((len f) -' 1) -' ((len f) -' 1)) + 1 by A2, A5, A6, A52, JORDAN3:27
.= 0 + 1 by XREAL_1:234
.= 1 ;
thus g1 . 2 = (mid f,1,i2) . (2 - (len (mid f,i1,((len f) -' 1)))) by A43, A53, A54, A55, JORDAN3:15
.= f . 1 by A2, A4, A7, A56, JORDAN3:27
.= f . (i1 + 1) by A52, Th14, NAT_1:11 ; :: thesis: verum

end;

end;

end;

i2 + 1 <= i1 by A42, NAT_1:13;
then (1 + i2) - i2 <= i1 - i2 by XREAL_1:11;
then 1 <= i1 -' i2 by NAT_D:39;
then 1 + 1 <= (i1 -' i2) + 1 by XREAL_1:8;
then A57: 2 <= len (mid f,i1,i2) by A2, A7, A8, A42, JORDAN3:27;
A58: g2 . 2 = (mid f,i1,i2) . 2 by A1, A42, Th39
.= f . ((i1 -' 2) + 1) by A2, A7, A8, A42, A57, JORDAN3:27
.= f . ((i1 - (1 + 1)) + 1) by A44, XREAL_1:235
.= f . (i1 - 1)
.= f . (i1 -' 1) by A2, XREAL_1:235 ;
1 < i1 by A2, A42, XXREAL_0:2;
then 1 + 1 <= i1 by NAT_1:13;
then A59: (1 + 1) - 1 <= i1 - 1 by XREAL_1:11;
then A60: 1 <= i1 -' 1 by NAT_D:39;

A61: now

assume A62: ( 1 = i1 -' 1 & i1 + 1 = len f ) ; :: thesis: contradiction
then 1 = i1 - 1 by NAT_D:39;
hence contradiction by A62, GOBOARD7:36; :: thesis: verum

end;

now

per cases ( 1 <> i1 -' 1 or i1 + 1 <> len f ) by A61;

case A63: 1 <> i1 -' 1 ; :: thesis: g1 . 2 <> g2 . 2

i1 -' 1 < (i1 -' 1) + 1 by NAT_1:13;
then i1 -' 1 < i1 by A2, XREAL_1:237;
then A64: ( 1 < i1 -' 1 & i1 -' 1 < i1 + 1 & i1 + 1 <= len f ) by A1, A60, A63, Def2, NAT_1:13, XXREAL_0:1;
then A65: f /. (i1 -' 1) <> f /. (i1 + 1) by GOBOARD7:39;
i1 -' 1 < len f by A64, XXREAL_0:2;
then A66: f . (i1 -' 1) = f /. (i1 -' 1) by A60, FINSEQ_4:24;
1 < i1 + 1 by A2, NAT_1:13;
hence g1 . 2 <> g2 . 2 by A2, A48, A58, A65, A66, FINSEQ_4:24; :: thesis: verum

end;

case A67: i1 + 1 <> len f ; :: thesis: g1 . 2 <> g2 . 2

i1 -' 1 < (i1 -' 1) + 1 by NAT_1:13;
then i1 -' 1 < i1 by A2, XREAL_1:237;
then A68: ( 1 <= i1 -' 1 & i1 -' 1 < i1 + 1 & i1 + 1 < len f ) by A2, A59, A67, NAT_1:13, NAT_D:39, XXREAL_0:1;
then A69: f /. (i1 -' 1) <> f /. (i1 + 1) by GOBOARD7:38;
i1 -' 1 < len f by A68, XXREAL_0:2;
then A70: f . (i1 -' 1) = f /. (i1 -' 1) by A68, FINSEQ_4:24;
1 < i1 + 1 by A2, NAT_1:13;
hence g1 . 2 <> g2 . 2 by A2, A48, A58, A69, A70, FINSEQ_4:24; :: thesis: verum

end;

end;

end;

hence g1 . 2 <> g2 . 2 ; :: thesis: verum

end;

end;

end;

hence g1 . 2 <> g2 . 2 ; :: thesis: verum