let F1, F2 be Element of REAL * ; :: thesis: ( dom F1 = dom f & ( for k being Element of 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 Element of 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
A24: ( dom F1 = dom f & ( for k being Element of 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
A25: ( dom F2 = dom f & ( for k being Element of 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
let xx be set ; :: thesis: ( xx in dom F1 implies F1 . b1 = F2 . b1 )
assume A26: xx in dom F1 ; :: thesis: F1 . b1 = F2 . b1
then reconsider k = xx as Element of NAT ;
defpred S1[] means f hasBetterPathAt n,k -' n;
defpred S2[] means f hasBetterPathAt n,k -' (2 * n);
per cases ( ( n < k & k <= 2 * n ) or ( 2 * n < k & k <= 3 * n ) or k <= n or k > 3 * n ) ;
suppose A27: ( n < k & k <= 2 * n ) ; :: thesis: F1 . b1 = F2 . b1
hereby :: thesis: verum
per cases ( S1[] or not S1[] ) ;
suppose A28: S1[] ; :: thesis: F1 . xx = F2 . xx
hence F1 . xx = f /. (((n * n) + (3 * n)) + 1) by A24, A26, A27
.= F2 . xx by A24, A25, A26, A27, A28 ;
:: thesis: verum
end;
suppose A29: not S1[] ; :: thesis: F1 . xx = F2 . xx
hence F1 . xx = f . k by A24, A26, A27
.= F2 . xx by A24, A25, A26, A27, A29 ;
:: thesis: verum
end;
end;
end;
end;
suppose A30: ( 2 * n < k & k <= 3 * n ) ; :: thesis: F1 . b1 = F2 . b1
hereby :: thesis: verum
per cases ( S2[] or not S2[] ) ;
suppose A31: S2[] ; :: thesis: F1 . xx = F2 . xx
hence F1 . xx = newpathcost f,n,(k -' (2 * n)) by A24, A26, A30
.= F2 . xx by A24, A25, A26, A30, A31 ;
:: thesis: verum
end;
suppose A32: not S2[] ; :: thesis: F1 . xx = F2 . xx
hence F1 . xx = f . k by A24, A26, A30
.= F2 . xx by A24, A25, A26, A30, A32 ;
:: thesis: verum
end;
end;
end;
end;
suppose A33: ( k <= n or k > 3 * n ) ; :: thesis: F1 . b1 = F2 . b1
hence F1 . xx = f . k by A24, A26
.= F2 . xx by A24, A25, A26, A33 ;
:: thesis: verum
end;
end;
end;
hence F1 = F2 by A24, A25, FUNCT_1:9; :: thesis: verum