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 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; :: 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 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( ( 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))} :: thesis: ( (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} )

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)} :: thesis: (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))}

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))} :: thesis: verum

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; :: 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 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( ( 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))} :: thesis: ( (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

( g . 1 = x1 & g . (len g) = x2 )
by A1;
let i be Nat; :: thesis: ( 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 ; :: thesis: (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))} :: thesis: verum

end;assume that

A11: 1 < i and

A12: i < len g ; :: thesis: (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))} :: thesis: verum

proof

thus
(rng g) /\ (U_FT (g /. i)) c= {(g . (i -' 1)),(g . i),(g . (i + 1))}
:: according to XBOOLE_0:def 10 :: thesis: {(g . (i -' 1)),(g . i),(g . (i + 1))} c= (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))} ; :: thesis: x in (rng g) /\ (U_FT (g /. i))

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(g . (i -' 1)),(g . i),(g . (i + 1))} or x in (rng g) /\ (U_FT (g /. i)) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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)) ; :: thesis: 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; :: thesis: verum

end;assume A19: x in (rng g) /\ (U_FT (g /. i)) ; :: thesis: 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; :: thesis: verum

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))} ; :: thesis: 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;

end;

suppose A28:
x = g . (i -' 1)
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

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)} :: thesis: (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))}

proof

len g < (len g) + 1
by NAT_1:13;
thus
(rng g) /\ (U_FT (g /. 1)) c= {(g . 1),(g . 2)}
:: according to XBOOLE_0:def 10 :: thesis: {(g . 1),(g . 2)} c= (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)} ; :: thesis: x in (rng g) /\ (U_FT (g /. 1))

hence x in (rng g) /\ (U_FT (g /. 1)) by A40, A42, XBOOLE_0:def 4; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(g . 1),(g . 2)} or x in (rng g) /\ (U_FT (g /. 1)) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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)) ; :: thesis: 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; :: thesis: verum

end;assume A35: x in (rng g) /\ (U_FT (g /. 1)) ; :: thesis: 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; :: thesis: verum

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)} ; :: thesis: x in (rng g) /\ (U_FT (g /. 1))

A42: now :: thesis: ( ( x = g . 1 & x in U_FT (g /. 1) ) or ( x = g . 2 & x in U_FT (g /. 1) ) )

( x = g . 1 implies x in rng g )
by A33, FUNCT_1:def 3;end;

hence x in (rng g) /\ (U_FT (g /. 1)) by A40, A42, XBOOLE_0:def 4; :: thesis: verum

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))} :: thesis: verum

proof

thus
(rng g) /\ (U_FT (g /. (len g))) c= {(g . ((len g) -' 1)),(g . (len g))}
:: according to XBOOLE_0:def 10 :: thesis: {(g . ((len g) -' 1)),(g . (len g))} c= (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))} ; :: thesis: 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; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(g . ((len g) -' 1)),(g . (len g))} or x in (rng g) /\ (U_FT (g /. (len g))) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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))) ; :: thesis: 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; :: thesis: verum

end;assume A50: x in (rng g) /\ (U_FT (g /. (len g))) ; :: thesis: 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; :: thesis: verum

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))} ; :: thesis: 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; :: thesis: verum