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 & 1 <= k & k <= len g holds

( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )

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 & 1 <= k & k <= len g holds

( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )

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 & 1 <= k & k <= len g holds

( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )

let x1, x2 be Element of FT; :: thesis: for k being Element of NAT st g is_minimum_path_in A,x1,x2 & 1 <= k & k <= len g holds

( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )

let k be Element of NAT ; :: thesis: ( g is_minimum_path_in A,x1,x2 & 1 <= k & k <= len g implies ( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k ) )

assume that

A1: g is_minimum_path_in A,x1,x2 and

A2: 1 <= k and

A3: k <= len g ; :: thesis: ( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )

A4: k in dom g by A2, A3, FINSEQ_3:25;

g is continuous by A1;

hence g | k is continuous by A2, Th46; :: thesis: ( rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )

A5: rng (g | k) c= rng g by FINSEQ_5:19;

rng g c= A by A1;

hence rng (g | k) c= A by A5; :: thesis: ( (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )

g . 1 = x1 by A1;

hence (g | k) . 1 = x1 by A2, FINSEQ_3:112; :: thesis: (g | k) . (len (g | k)) = g /. k

len (g | k) = k by A3, FINSEQ_1:59;

hence (g | k) . (len (g | k)) = g . k by FINSEQ_3:112

.= g /. k by A4, PARTFUN1:def 6 ;

:: 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 & 1 <= k & k <= len g holds

( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )

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 & 1 <= k & k <= len g holds

( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )

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 & 1 <= k & k <= len g holds

( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )

let x1, x2 be Element of FT; :: thesis: for k being Element of NAT st g is_minimum_path_in A,x1,x2 & 1 <= k & k <= len g holds

( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )

let k be Element of NAT ; :: thesis: ( g is_minimum_path_in A,x1,x2 & 1 <= k & k <= len g implies ( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k ) )

assume that

A1: g is_minimum_path_in A,x1,x2 and

A2: 1 <= k and

A3: k <= len g ; :: thesis: ( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )

A4: k in dom g by A2, A3, FINSEQ_3:25;

g is continuous by A1;

hence g | k is continuous by A2, Th46; :: thesis: ( rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )

A5: rng (g | k) c= rng g by FINSEQ_5:19;

rng g c= A by A1;

hence rng (g | k) c= A by A5; :: thesis: ( (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )

g . 1 = x1 by A1;

hence (g | k) . 1 = x1 by A2, FINSEQ_3:112; :: thesis: (g | k) . (len (g | k)) = g /. k

len (g | k) = k by A3, FINSEQ_1:59;

hence (g | k) . (len (g | k)) = g . k by FINSEQ_3:112

.= g /. k by A4, PARTFUN1:def 6 ;

:: thesis: verum