let m, n be Element of 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, Def16;

A4: now

let k be Element of 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, Def16
.= h . k by A2, A3, A5, Def16 ;
:: thesis: verum

end;

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