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;

hence f,h equal_at m,n by A3, A4; :: thesis: verum

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

dom g = dom h
by A2;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;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

hence f,h equal_at m,n by A3, A4; :: thesis: verum