let m, n be Nat; :: thesis: for f, g, h being Element of REAL * st f,g equal_at m,n & g,h equal_at m,n holds
f,h equal_at m,n
let f, g, h be Element of REAL * ; :: thesis: ( f,g equal_at m,n & g,h equal_at m,n implies f,h equal_at m,n )
assume that
A1: f,g equal_at m,n and
A2: g,h equal_at m,n ; :: thesis: f,h equal_at m,n
A3: dom f = dom g by A1;

A4: now :: thesis: for k being Nat st k in dom f & m <= k & k <= n holds
f . k = h . k

let k be Nat; :: thesis: ( k in dom f & m <= k & k <= n implies f . k = h . k )
assume A5: ( k in dom f & m <= k & k <= n ) ; :: thesis: f . k = h . k
hence f . k = g . k by A1
.= h . k by A2, A3, A5 ;
:: thesis: verum

end;

dom g = dom h by A2;
hence f,h equal_at m,n by A3, A4; :: thesis: verum