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
for k being Element of NAT st g is_minimum_path_in A,x1,x2 & k < len g holds
( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 )

let g be FinSequence of FT; :: thesis: for A being Subset of FT
for x1, x2 being Element of FT
for k being Element of NAT st g is_minimum_path_in A,x1,x2 & k < len g holds
( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 )

let A be Subset of FT; :: thesis: for x1, x2 being Element of FT
for k being Element of NAT st g is_minimum_path_in A,x1,x2 & k < len g holds
( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 )

let x1, x2 be Element of FT; :: thesis: for k being Element of NAT st g is_minimum_path_in A,x1,x2 & k < len g holds
( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 )

let k be Element of NAT ; :: thesis: ( g is_minimum_path_in A,x1,x2 & k < len g implies ( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 ) )
assume that
A1: g is_minimum_path_in A,x1,x2 and
A2: k < len g ; :: thesis: ( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 )
A3: len (g /^ k) = (len g) - k by ;
g is continuous by A1;
hence g /^ k is continuous by ; :: thesis: ( rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 )
A4: rng (g /^ k) c= rng g by FINSEQ_5:33;
rng g c= A by A1;
hence rng (g /^ k) c= A by A4; :: thesis: ( (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 )
A5: len (g /^ k) = (len g) - k by ;
( 1 <= 1 + k & k + 1 <= len g ) by ;
then A6: 1 + k in dom g by FINSEQ_3:25;
A7: (len g) - k > 0 by ;
then (len g) -' k = (len g) - k by XREAL_0:def 2;
then (len g) - k >= 0 + 1 by ;
then 1 in dom (g /^ k) by ;
hence (g /^ k) . 1 = g . (1 + k) by
.= g /. (1 + k) by ;
:: thesis: (g /^ k) . (len (g /^ k)) = x2
A8: (len g) - k > 0 by ;
then A9: (len g) - k = (len g) -' k by XREAL_0:def 2;
then (len g) -' k >= 0 + 1 by ;
then (len g) -' k in dom (g /^ k) by ;
hence (g /^ k) . (len (g /^ k)) = g . (((len g) -' k) + k) by
.= x2 by A1, A9 ;
:: thesis: verum