defpred S_{1}[ Nat] means f hasBetterPathAt n,$1 -' (2 * n);

defpred S_{2}[ Nat] means f hasBetterPathAt n,$1 -' n;

set X = dom f;

defpred S_{3}[ object , object ] means for k being Nat st $1 = k & k in dom f holds

( ( n < k & k <= 2 * n implies ( ( S_{2}[k] implies $2 = f /. (((n * n) + (3 * n)) + 1) ) & ( not S_{2}[k] implies $2 = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( S_{1}[k] implies $2 = newpathcost (f,n,(k -' (2 * n))) ) & ( not S_{1}[k] implies $2 = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies $2 = f . k ) );

A9: ( dom F = dom f & ( for x being object st x in dom f holds

S_{3}[x,F . x] ) )
from CLASSES1:sch 1(A1);

A10: rng F c= REAL

then F is FinSequence by A9, FINSEQ_1:def 2;

then F is FinSequence of REAL by A10, FINSEQ_1:def 4;

then reconsider F = F as Element of REAL * by FINSEQ_1:def 11;

take F ; :: thesis: ( dom F = dom f & ( for k being Nat st k in dom f holds

( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies F . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies F . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies F . k = newpathcost (f,n,(k -' (2 * n))) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies F . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies F . k = f . k ) ) ) )

thus dom F = dom f by A9; :: thesis: for k being Nat st k in dom f holds

( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies F . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies F . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies F . k = newpathcost (f,n,(k -' (2 * n))) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies F . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies F . k = f . k ) )

let k be Nat; :: thesis: ( k in dom f implies ( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies F . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies F . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies F . k = newpathcost (f,n,(k -' (2 * n))) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies F . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies F . k = f . k ) ) )

assume k in dom f ; :: thesis: ( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies F . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies F . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies F . k = newpathcost (f,n,(k -' (2 * n))) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies F . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies F . k = f . k ) )

hence ( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies F . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies F . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies F . k = newpathcost (f,n,(k -' (2 * n))) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies F . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies F . k = f . k ) ) by A9; :: thesis: verum

defpred S

set X = dom f;

defpred S

( ( n < k & k <= 2 * n implies ( ( S

A1: now :: thesis: for xx being object st xx in dom f holds

ex y1 being object st S_{3}[xx,y1]

consider F being Function such that ex y1 being object st S

let xx be object ; :: thesis: ( xx in dom f implies ex y1 being object st S_{3}[y1,b_{2}] )

assume xx in dom f ; :: thesis: ex y1 being object st S_{3}[y1,b_{2}]

then reconsider k = xx as Element of NAT ;

end;assume xx in dom f ; :: thesis: ex y1 being object st S

then reconsider k = xx as Element of NAT ;

per cases
( ( n < k & k <= 2 * n ) or ( 2 * n < k & k <= 3 * n ) or k <= n or k > 3 * n )
;

end;

suppose A2:
( n < k & k <= 2 * n )
; :: thesis: ex y1 being object st S_{3}[y1,b_{2}]

thus
ex y1 being object st S_{3}[xx,y1]
:: thesis: verum

end;proof
end;

per cases
( S_{2}[k] or not S_{2}[k] )
;

end;

suppose A3:
S_{2}[k]
; :: thesis: ex y1 being object st S_{3}[xx,y1]

take y1 = f /. (((n * n) + (3 * n)) + 1); :: thesis: S_{3}[xx,y1]

thus S_{3}[xx,y1]
by A2, A3, Lm8; :: thesis: verum

end;thus S

suppose A5:
( 2 * n < k & k <= 3 * n )
; :: thesis: ex y1 being object st S_{3}[y1,b_{2}]

thus
ex y1 being object st S_{3}[xx,y1]
:: thesis: verum

end;proof
end;

per cases
( S_{1}[k] or not S_{1}[k] )
;

end;

suppose A6:
S_{1}[k]
; :: thesis: ex y1 being object st S_{3}[xx,y1]

take y1 = newpathcost (f,n,(k -' (2 * n))); :: thesis: S_{3}[xx,y1]

thus S_{3}[xx,y1]
by A5, A6, Lm8; :: thesis: verum

end;thus S

suppose A8:
( k <= n or k > 3 * n )
; :: thesis: ex y1 being object st S_{3}[y1,b_{2}]

end;

end;

A9: ( dom F = dom f & ( for x being object st x in dom f holds

S

A10: rng F c= REAL

proof

dom f = Seg (len f)
by FINSEQ_1:def 3;
let y1 be object ; :: according to TARSKI:def 3 :: thesis: ( not y1 in rng F or y1 in REAL )

assume y1 in rng F ; :: thesis: y1 in REAL

then consider xx being object such that

A11: xx in dom F and

A12: y1 = F . xx by FUNCT_1:def 3;

reconsider k = xx as Element of NAT by A9, A11;

end;assume y1 in rng F ; :: thesis: y1 in REAL

then consider xx being object such that

A11: xx in dom F and

A12: y1 = F . xx by FUNCT_1:def 3;

reconsider k = xx as Element of NAT by A9, A11;

per cases
( ( n < k & k <= 2 * n ) or ( 2 * n < k & k <= 3 * n ) or k <= n or k > 3 * n )
;

end;

suppose A13:
( n < k & k <= 2 * n )
; :: thesis: y1 in REAL

end;

hereby :: thesis: verum
end;

per cases
( S_{2}[k] or not S_{2}[k] )
;

end;

suppose
not S_{2}[k]
; :: thesis: y1 in REAL

then y1 =
f . k
by A9, A11, A12, A13

.= f /. k by A9, A11, PARTFUN1:def 6 ;

hence y1 in REAL ; :: thesis: verum

end;.= f /. k by A9, A11, PARTFUN1:def 6 ;

hence y1 in REAL ; :: thesis: verum

suppose A14:
( 2 * n < k & k <= 3 * n )
; :: thesis: y1 in REAL

end;

hereby :: thesis: verum
end;

per cases
( S_{1}[k] or not S_{1}[k] )
;

end;

suppose
not S_{1}[k]
; :: thesis: y1 in REAL

then y1 =
f . k
by A9, A11, A12, A14

.= f /. k by A9, A11, PARTFUN1:def 6 ;

hence y1 in REAL ; :: thesis: verum

end;.= f /. k by A9, A11, PARTFUN1:def 6 ;

hence y1 in REAL ; :: thesis: verum

then F is FinSequence by A9, FINSEQ_1:def 2;

then F is FinSequence of REAL by A10, FINSEQ_1:def 4;

then reconsider F = F as Element of REAL * by FINSEQ_1:def 11;

take F ; :: thesis: ( dom F = dom f & ( for k being Nat st k in dom f holds

( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies F . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies F . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies F . k = newpathcost (f,n,(k -' (2 * n))) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies F . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies F . k = f . k ) ) ) )

thus dom F = dom f by A9; :: thesis: for k being Nat st k in dom f holds

( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies F . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies F . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies F . k = newpathcost (f,n,(k -' (2 * n))) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies F . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies F . k = f . k ) )

let k be Nat; :: thesis: ( k in dom f implies ( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies F . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies F . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies F . k = newpathcost (f,n,(k -' (2 * n))) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies F . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies F . k = f . k ) ) )

assume k in dom f ; :: thesis: ( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies F . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies F . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies F . k = newpathcost (f,n,(k -' (2 * n))) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies F . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies F . k = f . k ) )

hence ( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies F . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies F . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies F . k = newpathcost (f,n,(k -' (2 * n))) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies F . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies F . k = f . k ) ) by A9; :: thesis: verum