let FT be non empty RelStr ; for g being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds
for k being Nat st 1 <= k & k <= len g holds
g | k is_minimum_path_in A,x1,g /. k
let g be FinSequence of FT; for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds
for k being Nat st 1 <= k & k <= len g holds
g | k is_minimum_path_in A,x1,g /. k
let A be Subset of FT; for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds
for k being Nat st 1 <= k & k <= len g holds
g | k is_minimum_path_in A,x1,g /. k
let x1, x2 be Element of FT; ( g is_minimum_path_in A,x1,x2 implies for k being Nat st 1 <= k & k <= len g holds
g | k is_minimum_path_in A,x1,g /. k )
assume A1:
g is_minimum_path_in A,x1,x2
; for k being Nat st 1 <= k & k <= len g holds
g | k is_minimum_path_in A,x1,g /. k
then A2:
rng g c= A
;
A3:
g is continuous
by A1;
then A4:
1 <= len g
;
A5:
g . (len g) = x2
by A1;
let k be Nat; ( 1 <= k & k <= len g implies g | k is_minimum_path_in A,x1,g /. k )
assume that
A6:
1 <= k
and
A7:
k <= len g
; g | k is_minimum_path_in A,x1,g /. k
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A8:
( (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )
by A1, A6, A7, Th51;
A9:
( g | k is continuous & rng (g | k) c= A )
by A1, A6, A7, Th51;
now g | k is_minimum_path_in A,x1,g /. kper cases
( k < len g or k = len g )
by A7, XXREAL_0:1;
suppose A10:
k < len g
;
g | k is_minimum_path_in A,x1,g /. know g | k is_minimum_path_in A,x1,g /. k
k in dom g
by A6, A7, FINSEQ_3:25;
then A11:
g /. k = g . k
by PARTFUN1:def 6;
k + 1
<= len g
by A10, NAT_1:13;
then A12:
(g /^ k) . 1
= g . (k + 1)
by FINSEQ_6:114;
rng (g /^ k) c= rng g
by FINSEQ_5:33;
then A13:
rng (g /^ k) c= A
by A2;
assume
not
g | k is_minimum_path_in A,
x1,
g /. k
;
contradictionthen consider h being
FinSequence of
FT such that A14:
h is
continuous
and A15:
rng h c= A
and A16:
h . 1
= x1
and A17:
h . (len h) = g /. k
and A18:
len (g | k) > len h
by A9, A8;
reconsider s =
h ^ (g /^ k) as
FinSequence of
FT ;
A19:
len s = (len h) + (len (g /^ k))
by FINSEQ_1:22;
rng s = (rng h) \/ (rng (g /^ k))
by FINSEQ_1:31;
then A20:
rng s c= A
by A15, A13, XBOOLE_1:8;
A21:
g /^ k is
continuous
by A1, A10, Th52;
then
1
<= len (g /^ k)
;
then
len (g /^ k) in dom (g /^ k)
by FINSEQ_3:25;
then A22:
s . (len s) =
(g /^ k) . (len (g /^ k))
by A19, FINSEQ_1:def 7
.=
x2
by A5, A10, JORDAN4:6
;
A23:
1
<= len h
by A14;
then
1
in dom h
by FINSEQ_3:25;
then A24:
s . 1
= x1
by A16, FINSEQ_1:def 7;
len h in dom h
by A23, FINSEQ_3:25;
then
h . (len h) = h /. (len h)
by PARTFUN1:def 6;
then
(g /^ k) . 1
in U_FT (h /. (len h))
by A3, A6, A10, A17, A12, A11;
then A25:
s is
continuous
by A14, A21, Th44;
g = (g | k) ^ (g /^ k)
by RFINSEQ:8;
then
len g = (len (g | k)) + (len (g /^ k))
by FINSEQ_1:22;
then
len s < len g
by A18, A19, XREAL_1:8;
hence
contradiction
by A1, A25, A20, A24, A22;
verum end; hence
g | k is_minimum_path_in A,
x1,
g /. k
;
verum end; end; end;
hence
g | k is_minimum_path_in A,x1,g /. k
; verum