let F1, F2 be Element of REAL * ; :: thesis: ( 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 ) ) ; :: thesis: F1 = F2
now :: thesis: for xx being object st xx in dom F1 holds
F1 . xx = F2 . xx
let xx be object ; :: thesis: ( xx in dom F1 implies F1 . b1 = F2 . b1 )
assume A19: xx in dom F1 ; :: thesis: F1 . b1 = F2 . b1
then reconsider k = xx as Element of NAT ;
defpred S1[] means f hasBetterPathAt n,k -' (2 * n);
defpred S2[] means f hasBetterPathAt n,k -' n;
per cases ( ( n < k & k <= 2 * n ) or ( 2 * n < k & k <= 3 * n ) or k <= n or k > 3 * n ) ;
suppose A20: ( n < k & k <= 2 * n ) ; :: thesis: F1 . b1 = F2 . b1
hereby :: thesis: verum
per cases ( S2[] or not S2[] ) ;
suppose A21: S2[] ; :: thesis: F1 . xx = F2 . xx
hence F1 . xx = f /. (((n * n) + (3 * n)) + 1) by A15, A16, A19, A20
.= F2 . xx by A15, A18, A19, A20, A21 ;
:: thesis: verum
end;
suppose A22: not S2[] ; :: thesis: F1 . xx = F2 . xx
hence F1 . xx = f . k by A15, A16, A19, A20
.= F2 . xx by A15, A18, A19, A20, A22 ;
:: thesis: verum
end;
end;
end;
end;
suppose A23: ( 2 * n < k & k <= 3 * n ) ; :: thesis: F1 . b1 = F2 . b1
hereby :: thesis: verum
per cases ( S1[] or not S1[] ) ;
suppose A24: S1[] ; :: thesis: F1 . xx = F2 . xx
hence F1 . xx = newpathcost (f,n,(k -' (2 * n))) by A15, A16, A19, A23
.= F2 . xx by A15, A18, A19, A23, A24 ;
:: thesis: verum
end;
suppose A25: not S1[] ; :: thesis: F1 . xx = F2 . xx
hence F1 . xx = f . k by A15, A16, A19, A23
.= F2 . xx by A15, A18, A19, A23, A25 ;
:: thesis: verum
end;
end;
end;
end;
suppose A26: ( k <= n or k > 3 * n ) ; :: thesis: F1 . b1 = F2 . b1
hence F1 . xx = f . k by A15, A16, A19
.= F2 . xx by A15, A18, A19, A26 ;
:: thesis: verum
end;
end;
end;
hence F1 = F2 by A15, A17, FUNCT_1:2; :: thesis: verum