let F1, F2 be Element of REAL * ; ( dom F1 = dom f & ( for k being Nat st k in dom f holds
( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies F1 . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies F1 . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies F1 . k = newpathcost (f,n,(k -' (2 * n))) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies F1 . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies F1 . k = f . k ) ) ) & dom F2 = dom f & ( for k being Nat st k in dom f holds
( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies F2 . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies F2 . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies F2 . k = newpathcost (f,n,(k -' (2 * n))) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies F2 . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies F2 . k = f . k ) ) ) implies F1 = F2 )
assume that
A15:
dom F1 = dom f
and
A16:
for k being Nat st k in dom f holds
( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies F1 . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies F1 . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies F1 . k = newpathcost (f,n,(k -' (2 * n))) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies F1 . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies F1 . k = f . k ) )
and
A17:
dom F2 = dom f
and
A18:
for k being Nat st k in dom f holds
( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies F2 . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies F2 . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies F2 . k = newpathcost (f,n,(k -' (2 * n))) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies F2 . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies F2 . k = f . k ) )
; F1 = F2
hence
F1 = F2
by A15, A17, FUNCT_1:2; verum