let FT be non empty RelStr ; 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 filled & FT is symmetric & x1 <> x2 holds
( ( for i being Nat st 1 < i & i < len g holds
(rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ) & (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} )
let g be 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 filled & FT is symmetric & x1 <> x2 holds
( ( for i being Nat st 1 < i & i < len g holds
(rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ) & (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} )
let A be Subset of FT; for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & x1 <> x2 holds
( ( for i being Nat st 1 < i & i < len g holds
(rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ) & (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} )
let x1, x2 be Element of FT; ( g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & x1 <> x2 implies ( ( for i being Nat st 1 < i & i < len g holds
(rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ) & (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} ) )
assume that
A1:
g is_minimum_path_in A,x1,x2
and
A2:
( FT is filled & FT is symmetric )
and
A3:
x1 <> x2
; ( ( for i being Nat st 1 < i & i < len g holds
(rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ) & (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} )
A4:
dom g = Seg (len g)
by FINSEQ_1:def 3;
A5:
g is continuous
by A1;
then A6:
1 <= len g
;
then A7:
len g in dom g
by A4;
then A8:
g . (len g) = g /. (len g)
by PARTFUN1:def 6;
A9:
g is inv_continuous
by A1, A2, Th55;
then A10:
1 <= len g
;
thus
for i being Nat st 1 < i & i < len g holds
(rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))}
( (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} )proof
let i be
Nat;
( 1 < i & i < len g implies (rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} )
assume that A11:
1
< i
and A12:
i < len g
;
(rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))}
A13:
i in Seg (len g)
by A11, A12;
( 1
< i + 1 &
i + 1
<= len g )
by A11, A12, NAT_1:13;
then A14:
i + 1
in Seg (len g)
;
i -' 1
<= i
by NAT_D:35;
then A15:
i -' 1
< len g
by A12, XXREAL_0:2;
1
+ 1
<= i
by A11, NAT_1:13;
then A16:
1
<= i - 1
by XREAL_1:19;
then
1
<= i -' 1
by A11, XREAL_1:233;
then A17:
i -' 1
in Seg (len g)
by A15;
A18:
(i -' 1) + 1 =
(i - 1) + 1
by A11, XREAL_1:233
.=
i
;
thus
(rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))}
verumproof
thus
(rng g) /\ (U_FT (g /. i)) c= {(g . (i -' 1)),(g . i),(g . (i + 1))}
XBOOLE_0:def 10 {(g . (i -' 1)),(g . i),(g . (i + 1))} c= (rng g) /\ (U_FT (g /. i))proof
let x be
object ;
TARSKI:def 3 ( not x in (rng g) /\ (U_FT (g /. i)) or x in {(g . (i -' 1)),(g . i),(g . (i + 1))} )
assume A19:
x in (rng g) /\ (U_FT (g /. i))
;
x in {(g . (i -' 1)),(g . i),(g . (i + 1))}
then A20:
x in U_FT (g /. i)
by XBOOLE_0:def 4;
x in rng g
by A19, XBOOLE_0:def 4;
then consider nx being
object such that A21:
nx in dom g
and A22:
x = g . nx
by FUNCT_1:def 3;
reconsider j =
nx as
Element of
NAT by A21;
(
i = j + 1 implies
i - 1
= j )
;
then A23:
(
i = j + 1 implies
i -' 1
= j )
by A11, XREAL_1:233;
A24:
g /. i = g . i
by A4, A13, PARTFUN1:def 6;
( 1
<= j &
j <= len g )
by A4, A21, FINSEQ_1:1;
then
(
j = i or
i = j + 1 or
j = i + 1 )
by A9, A11, A12, A20, A22, A24;
hence
x in {(g . (i -' 1)),(g . i),(g . (i + 1))}
by A22, A23, ENUMSET1:def 1;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in {(g . (i -' 1)),(g . i),(g . (i + 1))} or x in (rng g) /\ (U_FT (g /. i)) )
A25:
g . i = g /. i
by A4, A13, PARTFUN1:def 6;
A26:
g . (i -' 1) = g /. (i -' 1)
by A4, A17, PARTFUN1:def 6;
assume A27:
x in {(g . (i -' 1)),(g . i),(g . (i + 1))}
;
x in (rng g) /\ (U_FT (g /. i))
per cases
( x = g . (i -' 1) or x = g . i or x = g . (i + 1) )
by A27, ENUMSET1:def 1;
suppose A28:
x = g . (i -' 1)
;
x in (rng g) /\ (U_FT (g /. i))
g . i in U_FT (g /. (i -' 1))
by A5, A16, A15, A18, A26;
then A29:
x in U_FT (g /. i)
by A2, A25, A26, A28;
x in rng g
by A4, A17, A28, FUNCT_1:def 3;
hence
x in (rng g) /\ (U_FT (g /. i))
by A29, XBOOLE_0:def 4;
verum end;
end;
end;
( g . 1 = x1 & g . (len g) = x2 )
by A1;
then A30:
1 < len g
by A3, A6, XXREAL_0:1;
then A31:
1 + 1 <= len g
by NAT_1:13;
then A32:
(1 + 1) - 1 <= (len g) - 1
by XREAL_1:13;
A33:
1 in dom g
by A10, FINSEQ_3:25;
then A34:
g . 1 = g /. 1
by PARTFUN1:def 6;
thus
(rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)}
(rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))}proof
thus
(rng g) /\ (U_FT (g /. 1)) c= {(g . 1),(g . 2)}
XBOOLE_0:def 10 {(g . 1),(g . 2)} c= (rng g) /\ (U_FT (g /. 1))proof
let x be
object ;
TARSKI:def 3 ( not x in (rng g) /\ (U_FT (g /. 1)) or x in {(g . 1),(g . 2)} )
assume A35:
x in (rng g) /\ (U_FT (g /. 1))
;
x in {(g . 1),(g . 2)}
then A36:
x in U_FT (g /. 1)
by XBOOLE_0:def 4;
x in rng g
by A35, XBOOLE_0:def 4;
then consider y being
object such that A37:
y in dom g
and A38:
x = g . y
by FUNCT_1:def 3;
reconsider j =
y as
Element of
NAT by A37;
A39:
1
<= j
by A4, A37, FINSEQ_1:1;
j <= len g
by A4, A37, FINSEQ_1:1;
then
( 1
+ 1
= j or 1
= j or
j + 1
= 1 )
by A9, A34, A36, A38, A39;
then
( 1
+ 1
= j or 1
= j )
by A39, XREAL_1:7;
hence
x in {(g . 1),(g . 2)}
by A38, TARSKI:def 2;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in {(g . 1),(g . 2)} or x in (rng g) /\ (U_FT (g /. 1)) )
2
in dom g
by A31, A4;
then A40:
(
x = g . 2 implies
x in rng g )
by FUNCT_1:def 3;
assume A41:
x in {(g . 1),(g . 2)}
;
x in (rng g) /\ (U_FT (g /. 1))
(
x = g . 1 implies
x in rng g )
by A33, FUNCT_1:def 3;
hence
x in (rng g) /\ (U_FT (g /. 1))
by A40, A42, XBOOLE_0:def 4;
verum
end;
len g < (len g) + 1
by NAT_1:13;
then A44:
(len g) - 1 < ((len g) + 1) - 1
by XREAL_1:14;
then A45:
(len g) -' 1 < len g
by A10, XREAL_1:233;
A46:
(len g) -' 1 = (len g) - 1
by A10, XREAL_1:233;
then A47:
(len g) -' 1 in dom g
by A32, A44, FINSEQ_3:25;
then A48:
g . ((len g) -' 1) = g /. ((len g) -' 1)
by PARTFUN1:def 6;
A49:
1 <= (len g) -' 1
by A10, A32, XREAL_1:233;
thus
(rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))}
verumproof
thus
(rng g) /\ (U_FT (g /. (len g))) c= {(g . ((len g) -' 1)),(g . (len g))}
XBOOLE_0:def 10 {(g . ((len g) -' 1)),(g . (len g))} c= (rng g) /\ (U_FT (g /. (len g)))proof
let x be
object ;
TARSKI:def 3 ( not x in (rng g) /\ (U_FT (g /. (len g))) or x in {(g . ((len g) -' 1)),(g . (len g))} )
assume A50:
x in (rng g) /\ (U_FT (g /. (len g)))
;
x in {(g . ((len g) -' 1)),(g . (len g))}
then A51:
x in U_FT (g /. (len g))
by XBOOLE_0:def 4;
x in rng g
by A50, XBOOLE_0:def 4;
then consider y being
object such that A52:
y in dom g
and A53:
x = g . y
by FUNCT_1:def 3;
reconsider ny =
y as
Element of
NAT by A52;
A54:
ny <= len g
by A4, A52, FINSEQ_1:1;
1
<= ny
by A4, A52, FINSEQ_1:1;
then
(
ny + 1
= len g or
(len g) + 1
= ny or
len g = ny )
by A9, A8, A51, A53, A54;
then
(
ny = (len g) - 1 or
len g = ny )
by A54, NAT_1:13;
then
(
x = g . ((len g) -' 1) or
x = g . (len g) )
by A6, A53, XREAL_1:233;
hence
x in {(g . ((len g) -' 1)),(g . (len g))}
by TARSKI:def 2;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in {(g . ((len g) -' 1)),(g . (len g))} or x in (rng g) /\ (U_FT (g /. (len g))) )
A55:
g . (len g) in U_FT (g /. (len g))
by A2, A8;
g . (((len g) -' 1) + 1) in U_FT (g /. ((len g) -' 1))
by A5, A49, A45, A48;
then A56:
g . ((len g) -' 1) in U_FT (g /. (len g))
by A2, A8, A46, A48;
assume
x in {(g . ((len g) -' 1)),(g . (len g))}
;
x in (rng g) /\ (U_FT (g /. (len g)))
then A57:
(
x = g . ((len g) -' 1) or
x = g . (len g) )
by TARSKI:def 2;
then
x in rng g
by A7, A47, FUNCT_1:def 3;
hence
x in (rng g) /\ (U_FT (g /. (len g)))
by A57, A55, A56, XBOOLE_0:def 4;
verum
end;