let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for k being Nat st 1 <= k & k + 1 <= len (Cage (C,n)) & (Cage (C,n)) /. k = S-max (L~ (Cage (C,n))) holds
((Cage (C,n)) /. (k + 1)) `2 = S-bound (L~ (Cage (C,n)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for k being Nat st 1 <= k & k + 1 <= len (Cage (C,n)) & (Cage (C,n)) /. k = S-max (L~ (Cage (C,n))) holds
((Cage (C,n)) /. (k + 1)) `2 = S-bound (L~ (Cage (C,n)))
A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;
A2: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32;
then 1 < (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:69;
then 1 < (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A2, SPRECT_2:70, XXREAL_0:2;
then 1 < (E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A2, SPRECT_2:71, XXREAL_0:2;
then A3: (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 by A2, SPRECT_2:72, XXREAL_0:2;
let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len (Cage (C,n)) & (Cage (C,n)) /. k = S-max (L~ (Cage (C,n))) implies ((Cage (C,n)) /. (k + 1)) `2 = S-bound (L~ (Cage (C,n))) )
assume that
A4: 1 <= k and
A5: k + 1 <= len (Cage (C,n)) and
A6: (Cage (C,n)) /. k = S-max (L~ (Cage (C,n))) ; :: thesis: ((Cage (C,n)) /. (k + 1)) `2 = S-bound (L~ (Cage (C,n)))
A7: k < len (Cage (C,n)) by A5, NAT_1:13;
then A8: k in dom (Cage (C,n)) by A4, FINSEQ_3:25;
then reconsider k9 = k - 1 as Nat by FINSEQ_3:26;
(S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) <= k by A6, A8, FINSEQ_5:39;
then A9: k > 1 by A3, XXREAL_0:2;
then consider i1, j1, i2, j2 being Nat such that
A10: [i1,j1] in Indices (Gauge (C,n)) and
A11: (Cage (C,n)) /. k = (Gauge (C,n)) * (i1,j1) and
A12: [i2,j2] in Indices (Gauge (C,n)) and
A13: (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i2,j2) and
A14: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A5, JORDAN8:3;
A15: 1 <= i1 by A10, MATRIX_0:32;
A16: j2 <= width (Gauge (C,n)) by A12, MATRIX_0:32;
A17: 1 <= j2 by A12, MATRIX_0:32;
A18: j1 <= width (Gauge (C,n)) by A10, MATRIX_0:32;
A19: k9 + 1 < len (Cage (C,n)) by A5, NAT_1:13;
A20: i1 <= len (Gauge (C,n)) by A10, MATRIX_0:32;
((Gauge (C,n)) * (i1,j1)) `2 = S-bound (L~ (Cage (C,n))) by A6, A11, EUCLID:52
.= ((Gauge (C,n)) * (i1,1)) `2 by A15, A20, JORDAN1A:72 ;
then A21: j1 <= 1 by A15, A20, A18, GOBOARD5:4;
k >= 1 + 1 by A9, NAT_1:13;
then A22: k9 >= (1 + 1) - 1 by XREAL_1:9;
then consider i3, j3, i4, j4 being Nat such that
A23: [i3,j3] in Indices (Gauge (C,n)) and
A24: (Cage (C,n)) /. k9 = (Gauge (C,n)) * (i3,j3) and
A25: [i4,j4] in Indices (Gauge (C,n)) and
A26: (Cage (C,n)) /. (k9 + 1) = (Gauge (C,n)) * (i4,j4) and
A27: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, A7, JORDAN8:3;
A28: i1 = i4 by A10, A11, A25, A26, GOBOARD1:5;
A29: j1 = j4 by A10, A11, A25, A26, GOBOARD1:5;
A30: 1 <= i3 by A23, MATRIX_0:32;
A31: i3 <= len (Gauge (C,n)) by A23, MATRIX_0:32;
A32: 1 <= j1 by A10, MATRIX_0:32;
then A33: j1 = 1 by A21, XXREAL_0:1;
A34: i3 = i4

proof

assume A35: i3 <> i4 ; :: thesis: contradiction

per cases ( ( j3 = j4 & i3 + 1 = i4 ) or ( j3 = j4 & i3 = i4 + 1 ) ) by A27, A35;

suppose ( j3 = j4 & i3 + 1 = i4 ) ; :: thesis: contradiction

hence contradiction by A7, A21, A22, A23, A24, A25, A26, A29, JORDAN10:3; :: thesis: verum

end;

suppose A36: ( j3 = j4 & i3 = i4 + 1 ) ; :: thesis: contradiction

k9 < len (Cage (C,n)) by A19, NAT_1:13;
then (Gauge (C,n)) * (i3,j3) in S-most (L~ (Cage (C,n))) by A33, A22, A24, A29, A30, A31, A36, JORDAN1A:60;
then A37: ((Gauge (C,n)) * ((i4 + 1),j4)) `1 <= ((Gauge (C,n)) * (i4,j4)) `1 by A6, A26, A36, PSCOMP_1:55;
i4 < i4 + 1 by NAT_1:13;
hence contradiction by A15, A32, A18, A28, A29, A31, A36, A37, GOBOARD5:3; :: thesis: verum

end;

end;

end;

A38: ( 1 <= i2 & i2 <= len (Gauge (C,n)) ) by A12, MATRIX_0:32;
A39: k9 + 1 = k ;
A40: 1 <= j3 by A23, MATRIX_0:32;
j1 = j2

proof

assume A41: j1 <> j2 ; :: thesis: contradiction

per cases ( ( j1 = j2 + 1 & i1 = i2 ) or ( j1 + 1 = j2 & i1 = i2 ) ) by A14, A41;

suppose ( j1 = j2 + 1 & i1 = i2 ) ; :: thesis: contradiction

hence contradiction by A17, A21, NAT_1:13; :: thesis: verum

end;

suppose A42: ( j1 + 1 = j2 & i1 = i2 ) ; :: thesis: contradiction

k9 + (1 + 1) <= len (Cage (C,n)) by A5;
then A43: (LSeg ((Cage (C,n)),k9)) /\ (LSeg ((Cage (C,n)),k)) = {((Cage (C,n)) /. k)} by A22, A39, TOPREAL1:def 6;
( (Cage (C,n)) /. k9 in LSeg ((Cage (C,n)),k9) & (Cage (C,n)) /. (k + 1) in LSeg ((Cage (C,n)),k) ) by A4, A5, A7, A22, A39, TOPREAL1:21;
then (Cage (C,n)) /. (k + 1) in {((Cage (C,n)) /. k)} by A13, A21, A24, A27, A28, A29, A40, A34, A42, A43, NAT_1:13, XBOOLE_0:def 4;
then (Cage (C,n)) /. (k + 1) = (Cage (C,n)) /. k by TARSKI:def 1;
hence contradiction by A10, A11, A12, A13, A41, GOBOARD1:5; :: thesis: verum

end;

end;

end;

then ((Gauge (C,n)) * (i1,j1)) `2 = ((Gauge (C,n)) * (1,j2)) `2 by A15, A20, A32, A18, GOBOARD5:1
.= ((Gauge (C,n)) * (i2,j2)) `2 by A38, A17, A16, GOBOARD5:1 ;
hence ((Cage (C,n)) /. (k + 1)) `2 = S-bound (L~ (Cage (C,n))) by A6, A11, A13, EUCLID:52; :: thesis: verum