let FT be non empty RelStr ; :: thesis: for g being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds
g is inv_continuous

let g be FinSequence of FT; :: thesis: for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds
g is inv_continuous

let A be Subset of FT; :: thesis: for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds
g is inv_continuous

let x1, x2 be Element of FT; :: thesis: ( g is_minimum_path_in A,x1,x2 & FT is symmetric implies g is inv_continuous )
assume that
A1: g is_minimum_path_in A,x1,x2 and
A2: FT is symmetric ; :: thesis:
A3: g . 1 = x1 by A1;
A4: g . (len g) = x2 by A1;
A5: g is continuous by A1;
hence 1 <= len g ; :: according to FINTOPO6:def 9 :: thesis: for i, j being Nat
for y being Element of FT st 1 <= i & i <= len g & 1 <= j & j <= len g & y = g . i & i <> j & g . j in U_FT y & not i = j + 1 holds
j = i + 1

let i2, j2 be Nat; :: thesis: for y being Element of FT st 1 <= i2 & i2 <= len g & 1 <= j2 & j2 <= len g & y = g . i2 & i2 <> j2 & g . j2 in U_FT y & not i2 = j2 + 1 holds
j2 = i2 + 1

let y be Element of FT; :: thesis: ( 1 <= i2 & i2 <= len g & 1 <= j2 & j2 <= len g & y = g . i2 & i2 <> j2 & g . j2 in U_FT y & not i2 = j2 + 1 implies j2 = i2 + 1 )
assume that
A6: 1 <= i2 and
A7: i2 <= len g and
A8: 1 <= j2 and
A9: j2 <= len g and
A10: y = g . i2 and
A11: i2 <> j2 and
A12: g . j2 in U_FT y ; :: thesis: ( i2 = j2 + 1 or j2 = i2 + 1 )
A13: rng g c= A by A1;
hereby :: thesis: verum
assume that
A14: i2 <> j2 + 1 and
A15: j2 <> i2 + 1 ; :: thesis: contradiction
per cases ( i2 < j2 or j2 < i2 ) by ;
suppose A16: i2 < j2 ; :: thesis: contradiction
set n1 = j2 -' 1;
set n2 = i2;
reconsider n1 = j2 -' 1, n2 = i2 as Element of NAT by ORDINAL1:def 12;
i2 + 1 <= j2 by ;
then i2 + 1 < j2 by ;
then i2 < j2 - 1 by XREAL_1:20;
then A17: n1 > n2 by ;
1 < j2 by ;
then 1 + 1 <= j2 by NAT_1:13;
then 1 <= j2 - 1 by XREAL_1:19;
then A18: 1 <= n1 by ;
set k = (len g) -' n1;
reconsider g2 = (g | n2) ^ (g /^ n1) as FinSequence of FT ;
A19: len (g | n2) = n2 by ;
A20: j2 -' 1 <= j2 by NAT_D:35;
then A21: n1 <= len g by ;
then A22: len (g /^ n1) = (len g) - n1 by RFINSEQ:def 1;
A23: (len g) - n1 >= 0 by ;
then A24: (len g) -' n1 = (len g) - n1 by XREAL_0:def 2;
A25: len g2 = (len (g | n2)) + (len (g /^ n1)) by FINSEQ_1:22
.= n2 + ((len g) - n1) by ;
A26: g2 . 1 = (g | n2) . 1 by
.= x1 by ;
now :: thesis: contradiction
per cases ( n1 < len g or n1 = len g ) by ;
suppose n1 < len g ; :: thesis: contradiction
then n1 + 1 <= len g by NAT_1:13;
then A27: (n1 + 1) - n1 <= (len g) - n1 by XREAL_1:13;
then A28: 0 + 1 <= n2 + ((len g) - n1) by XREAL_1:7;
A29: g2 is continuous
proof
thus len g2 >= 1 by ; :: according to FINTOPO6:def 6 :: thesis: for i being Nat
for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds
g2 . (i + 1) in U_FT x1

let i be Nat; :: thesis: for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds
g2 . (i + 1) in U_FT x1

let z1 be Element of FT; :: thesis: ( 1 <= i & i < len g2 & z1 = g2 . i implies g2 . (i + 1) in U_FT z1 )
assume that
A30: 1 <= i and
A31: i < len g2 and
A32: z1 = g2 . i ; :: thesis: g2 . (i + 1) in U_FT z1
A33: i + 1 <= len g2 by ;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
1 < i + 1 by ;
then i + 1 in dom g2 by ;
then g2 . (i + 1) = g2 /. (i + 1) by PARTFUN1:def 6;
then reconsider z2 = g2 . (i + 1) as Element of FT ;
per cases ( i < n2 or i >= n2 ) ;
suppose A34: i < n2 ; :: thesis: g2 . (i + 1) in U_FT z1
then A35: i + 1 <= n2 by NAT_1:13;
i + 1 <= len (g | n2) by ;
then A36: z2 = (g | n2) . (i + 1) by
.= g . (i + 1) by ;
A37: i < len g by ;
z1 = (g | n2) . i by
.= g . i by ;
hence g2 . (i + 1) in U_FT z1 by A5, A30, A37, A36; :: thesis: verum
end;
suppose A38: i >= n2 ; :: thesis: g2 . (i + 1) in U_FT z1
i - n2 < (n2 + ((len g) - n1)) - n2 by ;
then A39: i -' n2 < (len g) - n1 by ;
then i -' n2 < (len g) -' n1 by ;
then (i -' n2) + 1 <= (len g) -' n1 by NAT_1:13;
then A40: (i -' n2) + 1 <= len (g /^ n1) by ;
A41: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by
.= i ;
A42: (len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by
.= i + 1 ;
1 <= (i -' n2) + 1 by NAT_1:12;
then A43: (i -' n2) + 1 in dom (g /^ n1) by ;
per cases ( i > n2 or i = n2 ) by ;
suppose i > n2 ; :: thesis: g2 . (i + 1) in U_FT z1
then A44: i - n2 > 0 by XREAL_1:50;
then i -' n2 = i - n2 by XREAL_0:def 2;
then A45: 0 + 1 <= i -' n2 by ;
then A46: i -' n2 in dom (g /^ n1) by ;
A47: z2 = (g /^ n1) . ((i -' n2) + 1) by
.= g . (((i -' n2) + 1) + n1) by
.= g . (((i -' n2) + n1) + 1) ;
A48: ( 1 <= (i -' n2) + n1 & (i -' n2) + n1 < ((len g) - n1) + n1 ) by ;
z1 = (g /^ n1) . (i -' n2) by
.= g . ((i -' n2) + n1) by ;
hence g2 . (i + 1) in U_FT z1 by A5, A47, A48; :: thesis: verum
end;
suppose A49: i = n2 ; :: thesis: g2 . (i + 1) in U_FT z1
then A50: z1 = (g | n2) . n2 by
.= y by ;
z2 = (g /^ n1) . ((i -' n2) + 1) by
.= g . (((i -' n2) + 1) + n1) by
.= g . (((i -' n2) + n1) + 1)
.= g . ((0 + (j2 -' 1)) + 1) by
.= g . ((j2 - 1) + 1) by ;
hence g2 . (i + 1) in U_FT z1 by ; :: thesis: verum
end;
end;
end;
end;
end;
A51: rng (g /^ n1) c= rng g by FINSEQ_5:33;
( rng g2 = (rng (g | n2)) \/ (rng (g /^ n1)) & rng (g | n2) c= rng g ) by ;
then rng g2 c= rng g by ;
then A52: rng g2 c= A by A13;
A53: ((len g) -' n1) + n1 = len g by A24;
A54: (len g) -' n1 in dom (g /^ n1) by ;
then g2 . ((len (g | n2)) + ((len g) -' n1)) = (g /^ n1) . ((len g) -' n1) by FINSEQ_1:def 7
.= x2 by ;
then g2 . (len g2) = x2 by ;
then len g <= len g2 by A1, A26, A52, A29;
then (len g) - n2 <= (n2 + ((len g) - n1)) - n2 by ;
hence contradiction by A17, XREAL_1:10; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
suppose A55: j2 < i2 ; :: thesis: contradiction
reconsider n1 = i2 -' 1, n2 = j2 as Element of NAT by ORDINAL1:def 12;
j2 + 1 <= i2 by ;
then j2 + 1 < i2 by ;
then j2 < i2 - 1 by XREAL_1:20;
then A56: n1 > n2 by ;
1 < i2 by ;
then 1 + 1 <= i2 by NAT_1:13;
then 1 <= i2 - 1 by XREAL_1:19;
then A57: 1 <= n1 by ;
set k = (len g) -' n1;
reconsider g2 = (g | n2) ^ (g /^ n1) as FinSequence of FT ;
A58: len (g | n2) = n2 by ;
A59: i2 -' 1 <= i2 by NAT_D:35;
then A60: n1 <= len g by ;
then A61: len (g /^ n1) = (len g) - n1 by RFINSEQ:def 1;
A62: (len g) - n1 >= 0 by ;
then A63: (len g) -' n1 = (len g) - n1 by XREAL_0:def 2;
A64: len g2 = (len (g | n2)) + (len (g /^ n1)) by FINSEQ_1:22
.= n2 + ((len g) - n1) by ;
A65: g2 . 1 = (g | n2) . 1 by
.= x1 by ;
now :: thesis: contradiction
per cases ( n1 < len g or n1 = len g ) by ;
suppose n1 < len g ; :: thesis: contradiction
then n1 + 1 <= len g by NAT_1:13;
then A66: (n1 + 1) - n1 <= (len g) - n1 by XREAL_1:13;
then A67: 0 + 1 <= n2 + ((len g) - n1) by XREAL_1:7;
A68: g2 is continuous
proof
thus len g2 >= 1 by ; :: according to FINTOPO6:def 6 :: thesis: for i being Nat
for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds
g2 . (i + 1) in U_FT x1

let i be Nat; :: thesis: for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds
g2 . (i + 1) in U_FT x1

let z1 be Element of FT; :: thesis: ( 1 <= i & i < len g2 & z1 = g2 . i implies g2 . (i + 1) in U_FT z1 )
assume that
A69: 1 <= i and
A70: i < len g2 and
A71: z1 = g2 . i ; :: thesis: g2 . (i + 1) in U_FT z1
A72: i + 1 <= len g2 by ;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
1 < i + 1 by ;
then i + 1 in dom g2 by ;
then g2 . (i + 1) = g2 /. (i + 1) by PARTFUN1:def 6;
then reconsider z2 = g2 . (i + 1) as Element of FT ;
per cases ( i < n2 or i >= n2 ) ;
suppose A73: i < n2 ; :: thesis: g2 . (i + 1) in U_FT z1
then A74: i + 1 <= n2 by NAT_1:13;
i + 1 <= len (g | n2) by ;
then A75: z2 = (g | n2) . (i + 1) by
.= g . (i + 1) by ;
A76: i < len g by ;
z1 = (g | n2) . i by
.= g . i by ;
hence g2 . (i + 1) in U_FT z1 by A5, A69, A76, A75; :: thesis: verum
end;
suppose A77: i >= n2 ; :: thesis: g2 . (i + 1) in U_FT z1
i - n2 < (n2 + ((len g) - n1)) - n2 by ;
then A78: i -' n2 < (len g) - n1 by ;
then i -' n2 < (len g) -' n1 by ;
then (i -' n2) + 1 <= (len g) -' n1 by NAT_1:13;
then A79: (i -' n2) + 1 <= len (g /^ n1) by ;
A80: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by
.= i ;
A81: (len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by
.= i + 1 ;
1 <= (i -' n2) + 1 by NAT_1:12;
then A82: (i -' n2) + 1 in dom (g /^ n1) by ;
per cases ( i > n2 or i = n2 ) by ;
suppose i > n2 ; :: thesis: g2 . (i + 1) in U_FT z1
then A83: i - n2 > 0 by XREAL_1:50;
then i -' n2 = i - n2 by XREAL_0:def 2;
then A84: 0 + 1 <= i -' n2 by ;
then A85: i -' n2 in dom (g /^ n1) by ;
A86: z2 = (g /^ n1) . ((i -' n2) + 1) by
.= g . (((i -' n2) + 1) + n1) by
.= g . (((i -' n2) + n1) + 1) ;
A87: ( 1 <= (i -' n2) + n1 & (i -' n2) + n1 < ((len g) - n1) + n1 ) by ;
z1 = (g /^ n1) . (i -' n2) by
.= g . ((i -' n2) + n1) by ;
hence g2 . (i + 1) in U_FT z1 by A5, A86, A87; :: thesis: verum
end;
suppose A88: i = n2 ; :: thesis: g2 . (i + 1) in U_FT z1
then A89: z1 = (g | n2) . n2 by
.= g . j2 by FINSEQ_3:112 ;
z2 = (g /^ n1) . ((i -' n2) + 1) by
.= g . (((i -' n2) + 1) + n1) by
.= g . (((i -' n2) + n1) + 1)
.= g . ((0 + (i2 -' 1)) + 1) by
.= g . ((i2 - 1) + 1) by
.= y by A10 ;
hence g2 . (i + 1) in U_FT z1 by A2, A12, A89; :: thesis: verum
end;
end;
end;
end;
end;
A90: rng (g /^ n1) c= rng g by FINSEQ_5:33;
( rng g2 = (rng (g | n2)) \/ (rng (g /^ n1)) & rng (g | n2) c= rng g ) by ;
then rng g2 c= rng g by ;
then A91: rng g2 c= A by A13;
A92: ((len g) -' n1) + n1 = len g by A63;
A93: (len g) -' n1 in dom (g /^ n1) by ;
then g2 . ((len (g | n2)) + ((len g) -' n1)) = (g /^ n1) . ((len g) -' n1) by FINSEQ_1:def 7
.= x2 by ;
then g2 . (len g2) = x2 by ;
then len g <= len g2 by A1, A65, A91, A68;
then (len g) - n2 <= (n2 + ((len g) - n1)) - n2 by ;
hence contradiction by A56, XREAL_1:10; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;