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 A2, RFINSEQ:def 1;
g is continuous by A1;
hence g /^ k is continuous by A2, Th47; :: 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 A2, RFINSEQ:def 1;
( 1 <= 1 + k & k + 1 <= len g ) by A2, NAT_1:11, NAT_1:13;
then A6: 1 + k in dom g by FINSEQ_3:25;
A7: (len g) - k > 0 by A2, XREAL_1:50;
then (len g) -' k = (len g) - k by XREAL_0:def 2;
then (len g) - k >= 0 + 1 by A7, NAT_1:13;
then 1 in dom (g /^ k) by A5, FINSEQ_3:25;
hence (g /^ k) . 1 = g . (1 + k) by A2, RFINSEQ:def 1
.= g /. (1 + k) by A6, PARTFUN1:def 6 ;
:: thesis: (g /^ k) . (len (g /^ k)) = x2
A8: (len g) - k > 0 by A2, XREAL_1:50;
then A9: (len g) - k = (len g) -' k by XREAL_0:def 2;
then (len g) -' k >= 0 + 1 by A8, NAT_1:13;
then (len g) -' k in dom (g /^ k) by A5, A9, FINSEQ_3:25;
hence (g /^ k) . (len (g /^ k)) = g . (((len g) -' k) + k) by A2, A9, A3, RFINSEQ:def 1
.= x2 by A1, A9 ;
:: thesis: verum