let FT be non empty RelStr ; :: thesis:
let g be FinSequence of FT; :: thesis:
let A be Subset of FT; :: thesis:
let x1, x2 be Element of FT; :: thesis:
let k be Element of NAT ; :: thesis:
assume A1: ( g is_minimum_path_in A,x1,x2 & 1 <= k & k <= len g ) ; :: thesis:
then A2: len (g | k) = k by FINSEQ_1:80;
A3: ( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 ) by A1, Def8;
hence g | k is continuous by A1, Th47; :: thesis:
rng (g | k) c= rng g by FINSEQ_5:21;
hence rng (g | k) c= A by A3, XBOOLE_1:1; :: thesis:
thus (g | k) . 1 = x1 by A1, A3, FINSEQ_3:121; :: thesis:
A4: k in dom g by A1, FINSEQ_3:27;
thus (g | k) . (len (g | k)) = g . k by A2, FINSEQ_3:121
.= g /. k by A4, PARTFUN1:def 8 ; :: thesis: