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 ;
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 ;
then A11: g /. k = g . k by PARTFUN1:def 6;
k + 1 <= len g by ;
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 ;
A21: g /^ k is continuous by ;
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
.= x2 by ;
A23: 1 <= len h by A14;
then 1 in dom h by FINSEQ_3:25;
then A24: s . 1 = x1 by ;
len h in dom h by ;
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 ;
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 ;
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 ;
g | k = g by ;
hence g | k is_minimum_path_in A,x1,g /. k by ; :: thesis: verum
end;
end;
end;
hence g | k is_minimum_path_in A,x1,g /. k ; :: thesis: verum