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