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 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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
; :: thesis: for k being Nat st 1 <= k & k <= len g holds
g | k is_minimum_path_in A,x1,g /. k
then A2:
( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds
len g <= len h ) )
by Def8;
then A3:
( 1 <= len g & ( for i being Nat
for x11 being Element of FT st 1 <= i & i < len g & x11 = g . i holds
g . (i + 1) in U_FT x11 ) )
by Def6;
let k be Nat; :: thesis: ( 1 <= k & k <= len g implies g | k is_minimum_path_in A,x1,g /. k )
assume A4:
( 1 <= k & k <= len g )
; :: thesis: g | k is_minimum_path_in A,x1,g /. k
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A5:
( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )
by A1, A4, Th52;
now per cases
( k < len g or k = len g )
by A4, XXREAL_0:1;
suppose A6:
k < len g
;
:: thesis: g | k is_minimum_path_in A,x1,g /. know assume
not
g | k is_minimum_path_in A,
x1,
g /. k
;
:: thesis: contradictionthen consider h being
FinSequence of
FT such that A7:
(
h is
continuous &
rng h c= A &
h . 1
= x1 &
h . (len h) = g /. k &
len (g | k) > len h )
by A5, Def8;
reconsider s =
h ^ (g /^ k) as
FinSequence of
FT ;
A8:
len s = (len h) + (len (g /^ k))
by FINSEQ_1:35;
g = (g | k) ^ (g /^ k)
by RFINSEQ:21;
then
len g = (len (g | k)) + (len (g /^ k))
by FINSEQ_1:35;
then A9:
len s < len g
by A7, A8, XREAL_1:10;
k + 1
<= len g
by A6, NAT_1:13;
then A10:
(g /^ k) . 1
= g . (k + 1)
by JORDAN3:23;
A11:
1
<= len h
by A7, Def6;
then
len h in dom h
by FINSEQ_3:27;
then A12:
h . (len h) = h /. (len h)
by PARTFUN1:def 8;
k in dom g
by A4, FINSEQ_3:27;
then
( 1
<= k &
k < len g &
g /. k = g . k )
by A4, A6, PARTFUN1:def 8;
then A13:
(g /^ k) . 1
in U_FT (h /. (len h))
by A2, A7, A10, A12, Def6;
A14:
g /^ k is
continuous
by A1, A6, Th53;
then A15:
s is
continuous
by A7, A13, Th45;
A16:
1
<= len (g /^ k)
by A14, Def6;
rng (g /^ k) c= rng g
by FINSEQ_5:36;
then A17:
rng (g /^ k) c= A
by A2, XBOOLE_1:1;
rng s = (rng h) \/ (rng (g /^ k))
by FINSEQ_1:44;
then A18:
rng s c= A
by A7, A17, XBOOLE_1:8;
1
in dom h
by A11, FINSEQ_3:27;
then A19:
s . 1
= x1
by A7, FINSEQ_1:def 7;
len (g /^ k) in dom (g /^ k)
by A16, FINSEQ_3:27;
then s . (len s) =
(g /^ k) . (len (g /^ k))
by A8, FINSEQ_1:def 7
.=
x2
by A2, A6, JORDAN4:18
;
hence
contradiction
by A1, A9, A15, A18, A19, Def8;
:: thesis: verum end; hence
g | k is_minimum_path_in A,
x1,
g /. k
;
:: thesis: verum
hence
g | k is_minimum_path_in A,x1,g /. k
; :: thesis: verum