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 holds

for k being Nat st 1 <= k & k <= len g holds

g | k is_minimum_path_in A,x1,g /. k

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 holds

for k being Nat st 1 <= k & k <= len g holds

g | k is_minimum_path_in A,x1,g /. k

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

for k being Nat st 1 <= k & k <= len g holds

g | k is_minimum_path_in A,x1,g /. k

let x1, x2 be Element of FT; :: thesis: ( g is_minimum_path_in A,x1,x2 implies for k being Nat st 1 <= k & k <= len g holds

g | k is_minimum_path_in A,x1,g /. k )

assume A1: g is_minimum_path_in A,x1,x2 ; :: thesis: for k being Nat st 1 <= k & k <= len g holds

g | k is_minimum_path_in A,x1,g /. k

then A2: rng g c= A ;

A3: g is continuous by A1;

then A4: 1 <= len g ;

A5: g . (len g) = x2 by A1;

let k be Nat; :: thesis: ( 1 <= k & k <= len g implies g | k is_minimum_path_in A,x1,g /. k )

assume that

A6: 1 <= k and

A7: k <= len g ; :: thesis: g | k is_minimum_path_in A,x1,g /. k

reconsider k = k as Element of NAT by ORDINAL1:def 12;

A8: ( (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k ) by A1, A6, A7, Th51;

A9: ( g | k is continuous & rng (g | k) c= A ) by A1, A6, A7, Th51;

for A being Subset of FT

for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds

for k being Nat st 1 <= k & k <= len g holds

g | k is_minimum_path_in A,x1,g /. k

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 holds

for k being Nat st 1 <= k & k <= len g holds

g | k is_minimum_path_in A,x1,g /. k

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

for k being Nat st 1 <= k & k <= len g holds

g | k is_minimum_path_in A,x1,g /. k

let x1, x2 be Element of FT; :: thesis: ( g is_minimum_path_in A,x1,x2 implies for k being Nat st 1 <= k & k <= len g holds

g | k is_minimum_path_in A,x1,g /. k )

assume A1: g is_minimum_path_in A,x1,x2 ; :: thesis: for k being Nat st 1 <= k & k <= len g holds

g | k is_minimum_path_in A,x1,g /. k

then A2: rng g c= A ;

A3: g is continuous by A1;

then A4: 1 <= len g ;

A5: g . (len g) = x2 by A1;

let k be Nat; :: thesis: ( 1 <= k & k <= len g implies g | k is_minimum_path_in A,x1,g /. k )

assume that

A6: 1 <= k and

A7: k <= len g ; :: thesis: g | k is_minimum_path_in A,x1,g /. k

reconsider k = k as Element of NAT by ORDINAL1:def 12;

A8: ( (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k ) by A1, A6, A7, Th51;

A9: ( g | k is continuous & rng (g | k) c= A ) by A1, A6, A7, Th51;

now :: thesis: g | k is_minimum_path_in A,x1,g /. kend;

hence
g | k is_minimum_path_in A,x1,g /. k
; :: thesis: verumper cases
( k < len g or k = len g )
by A7, XXREAL_0:1;

end;

suppose A10:
k < len g
; :: thesis: g | k is_minimum_path_in A,x1,g /. k

end;

now :: thesis: g | k is_minimum_path_in A,x1,g /. k

hence
g | k is_minimum_path_in A,x1,g /. k
; :: thesis: verum
k in dom g
by A6, A7, FINSEQ_3:25;

then A11: g /. k = g . k by PARTFUN1:def 6;

k + 1 <= len g by A10, NAT_1:13;

then A12: (g /^ k) . 1 = g . (k + 1) by FINSEQ_6:114;

rng (g /^ k) c= rng g by FINSEQ_5:33;

then A13: rng (g /^ k) c= A by A2;

assume not g | k is_minimum_path_in A,x1,g /. k ; :: thesis: contradiction

then consider h being FinSequence of FT such that

A14: h is continuous and

A15: rng h c= A and

A16: h . 1 = x1 and

A17: h . (len h) = g /. k and

A18: len (g | k) > len h by A9, A8;

reconsider s = h ^ (g /^ k) as FinSequence of FT ;

A19: len s = (len h) + (len (g /^ k)) by FINSEQ_1:22;

rng s = (rng h) \/ (rng (g /^ k)) by FINSEQ_1:31;

then A20: rng s c= A by A15, A13, XBOOLE_1:8;

A21: g /^ k is continuous by A1, A10, Th52;

then 1 <= len (g /^ k) ;

then len (g /^ k) in dom (g /^ k) by FINSEQ_3:25;

then A22: s . (len s) = (g /^ k) . (len (g /^ k)) by A19, FINSEQ_1:def 7

.= x2 by A5, A10, JORDAN4:6 ;

A23: 1 <= len h by A14;

then 1 in dom h by FINSEQ_3:25;

then A24: s . 1 = x1 by A16, FINSEQ_1:def 7;

len h in dom h by A23, FINSEQ_3:25;

then h . (len h) = h /. (len h) by PARTFUN1:def 6;

then (g /^ k) . 1 in U_FT (h /. (len h)) by A3, A6, A10, A17, A12, A11;

then A25: s is continuous by A14, A21, Th44;

g = (g | k) ^ (g /^ k) by RFINSEQ:8;

then len g = (len (g | k)) + (len (g /^ k)) by FINSEQ_1:22;

then len s < len g by A18, A19, XREAL_1:8;

hence contradiction by A1, A25, A20, A24, A22; :: thesis: verum

end;then A11: g /. k = g . k by PARTFUN1:def 6;

k + 1 <= len g by A10, NAT_1:13;

then A12: (g /^ k) . 1 = g . (k + 1) by FINSEQ_6:114;

rng (g /^ k) c= rng g by FINSEQ_5:33;

then A13: rng (g /^ k) c= A by A2;

assume not g | k is_minimum_path_in A,x1,g /. k ; :: thesis: contradiction

then consider h being FinSequence of FT such that

A14: h is continuous and

A15: rng h c= A and

A16: h . 1 = x1 and

A17: h . (len h) = g /. k and

A18: len (g | k) > len h by A9, A8;

reconsider s = h ^ (g /^ k) as FinSequence of FT ;

A19: len s = (len h) + (len (g /^ k)) by FINSEQ_1:22;

rng s = (rng h) \/ (rng (g /^ k)) by FINSEQ_1:31;

then A20: rng s c= A by A15, A13, XBOOLE_1:8;

A21: g /^ k is continuous by A1, A10, Th52;

then 1 <= len (g /^ k) ;

then len (g /^ k) in dom (g /^ k) by FINSEQ_3:25;

then A22: s . (len s) = (g /^ k) . (len (g /^ k)) by A19, FINSEQ_1:def 7

.= x2 by A5, A10, JORDAN4:6 ;

A23: 1 <= len h by A14;

then 1 in dom h by FINSEQ_3:25;

then A24: s . 1 = x1 by A16, FINSEQ_1:def 7;

len h in dom h by A23, FINSEQ_3:25;

then h . (len h) = h /. (len h) by PARTFUN1:def 6;

then (g /^ k) . 1 in U_FT (h /. (len h)) by A3, A6, A10, A17, A12, A11;

then A25: s is continuous by A14, A21, Th44;

g = (g | k) ^ (g /^ k) by RFINSEQ:8;

then len g = (len (g | k)) + (len (g /^ k)) by FINSEQ_1:22;

then len s < len g by A18, A19, XREAL_1:8;

hence contradiction by A1, A25, A20, A24, A22; :: thesis: verum

suppose A26:
k = len g
; :: thesis: g | k is_minimum_path_in A,x1,g /. k

A27:
len g in dom g
by A4, FINSEQ_3:25;

g | k = g by A26, FINSEQ_1:58;

hence g | k is_minimum_path_in A,x1,g /. k by A1, A26, A27, PARTFUN1:def 6; :: thesis: verum

end;g | k = g by A26, FINSEQ_1:58;

hence g | k is_minimum_path_in A,x1,g /. k by A1, A26, A27, PARTFUN1:def 6; :: thesis: verum