let M, N be AbGroup; :: thesis: for f, g, h being Element of Funcs ( the carrier of M, the carrier of N) holds
( h = (ADD (M,N)) . (f,g) iff for x being Element of the carrier of M holds h . x = (f . x) + (g . x) )
let f, g, h be Element of Funcs ( the carrier of M, the carrier of N); :: thesis: ( h = (ADD (M,N)) . (f,g) iff for x being Element of the carrier of M holds h . x = (f . x) + (g . x) )

hereby :: thesis: ( ( for x being Element of the carrier of M holds h . x = (f . x) + (g . x) ) implies h = (ADD (M,N)) . (f,g) )

assume A1: h = (ADD (M,N)) . (f,g) ; :: thesis: for x being Element of the carrier of M holds h . x = (f . x) + (g . x)
let x be Element of the carrier of M; :: thesis: h . x = (f . x) + (g . x)
A2: x in dom ( the addF of N .: (f,g)) by Lm1;
thus h . x = ( the addF of N .: (f,g)) . x by A1, Def1
.= (f . x) + (g . x) by A2, FUNCOP_1:22 ; :: thesis: verum

end;

assume A3: for x being Element of M holds h . x = (f . x) + (g . x) ; :: thesis: h = (ADD (M,N)) . (f,g)

now :: thesis: for x being Element of M holds ((ADD (M,N)) . (f,g)) . x = h . x

let x be Element of M; :: thesis: ((ADD (M,N)) . (f,g)) . x = h . x
A4: x in dom ( the addF of N .: (f,g)) by Lm1;
thus ((ADD (M,N)) . (f,g)) . x = ( the addF of N .: (f,g)) . x by Def1
.= (f . x) + (g . x) by A4, FUNCOP_1:22
.= h . x by A3 ; :: thesis: verum

end;

hence h = (ADD (M,N)) . (f,g) ; :: thesis: verum