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

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