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;

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

per cases ( k < len g or k = len g ) by A7, XXREAL_0:1;

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

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

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, FINSEQ_6:185 ;
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;

hence g | k is_minimum_path_in A,x1,g /. k ; :: thesis: verum

end;

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;

end;

end;

hence g | k is_minimum_path_in A,x1,g /. k ; :: thesis: verum