defpred S₁[ Nat] means f hasBetterPathAt n,$1 -' (2 * n);
defpred S₂[ Nat] means f hasBetterPathAt n,$1 -' n;
set X = dom f;
defpred S₃[ object , object ] means for k being Nat st $1 = k & k in dom f holds
( ( n < k & k <= 2 * n implies ( ( S₂[k] implies $2 = f /. (((n * n) + (3 * n)) + 1) ) & ( not S₂[k] implies $2 = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( S₁[k] implies $2 = newpathcost (f,n,(k -' (2 * n))) ) & ( not S₁[k] implies $2 = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies $2 = f . k ) );

let xx be object ; :: thesis:
assume xx in dom f ; :: thesis:
then reconsider k = xx as Element of NAT ;

suppose A2: ( n < k & k <= 2 * n ) ; :: thesis:

thus ex y1 being object st S₃[xx,y1] :: thesis:

proof

per cases ;

suppose A3: S₂[k] ; :: thesis:

take y1 = f /. (((n * n) + (3 * n)) + 1); :: thesis:
thus S₃[xx,y1] by A2, A3, Lm8; :: thesis:

end;

suppose A4: not S₂[k] ; :: thesis:

take y1 = f . k; :: thesis:
thus S₃[xx,y1] by A2, A4; :: thesis:

end;

suppose A5: ( 2 * n < k & k <= 3 * n ) ; :: thesis:

thus ex y1 being object st S₃[xx,y1] :: thesis:

proof

per cases ;

suppose A6: S₁[k] ; :: thesis:

take y1 = newpathcost (f,n,(k -' (2 * n))); :: thesis:
thus S₃[xx,y1] by A5, A6, Lm8; :: thesis:

end;

suppose A7: not S₁[k] ; :: thesis:

take y1 = f . k; :: thesis:
thus S₃[xx,y1] by A5, A7; :: thesis:

end;

suppose A8: ( k <= n or k > 3 * n ) ; :: thesis:

thus ex y1 being object st S₃[xx,y1] :: thesis:

proof

take y1 = f . k; :: thesis:
thus S₃[xx,y1] by A8, Lm8; :: thesis:

end;

consider F being Function such that
A9: ( dom F = dom f & ( for x being object st x in dom f holds
S₃[x,F . x] ) ) from CLASSES1:sch 1(A1);
A10: rng F c= REAL

proof

let y1 be object ; :: according to TARSKI:def 3 :: thesis:
assume y1 in rng F ; :: thesis:
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 ;

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

hereby :: thesis:

per cases ;

suppose S₂[k] ; :: thesis:

then y1 = f /. (((n * n) + (3 * n)) + 1) by A9, A11, A12, A13;
hence y1 in REAL ; :: thesis:

end;

suppose not S₂[k] ; :: thesis:

then y1 = f . k by A9, A11, A12, A13
.= f /. k by A9, A11, PARTFUN1:def 6 ;
hence y1 in REAL ; :: thesis:

end;

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

hereby :: thesis:

per cases ;

suppose S₁[k] ; :: thesis:

then y1 = newpathcost (f,n,(k -' (2 * n))) by A9, A11, A12, A14;
hence y1 in REAL ; :: thesis:

end;

suppose not S₁[k] ; :: thesis:

then y1 = f . k by A9, A11, A12, A14
.= f /. k by A9, A11, PARTFUN1:def 6 ;
hence y1 in REAL ; :: thesis:

end;

suppose ( k <= n or k > 3 * n ) ; :: thesis:

then y1 = f . k by A9, A11, A12
.= f /. k by A9, A11, PARTFUN1:def 6 ;
hence y1 in REAL ; :: thesis:

end;

dom f = Seg (len f) by FINSEQ_1:def 3;
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:
thus dom F = dom f by A9; :: thesis:
let k be Nat; :: thesis:
assume k in dom f ; :: thesis:
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: