let X be non empty set ; :: thesis: for Y being non empty addLoopStr
for f, g, h being Element of Funcs (X, the carrier of Y) holds
( h = (FuncAdd (X,Y)) . (f,g) iff for x being Element of X holds h . x = (f . x) + (g . x) )
let Y be non empty addLoopStr ; :: thesis: for f, g, h being Element of Funcs (X, the carrier of Y) holds
( h = (FuncAdd (X,Y)) . (f,g) iff for x being Element of X holds h . x = (f . x) + (g . x) )
let f, g, h be Element of Funcs (X, the carrier of Y); :: thesis: ( h = (FuncAdd (X,Y)) . (f,g) iff for x being Element of X holds h . x = (f . x) + (g . x) )

hereby :: thesis: ( ( for x being Element of X holds h . x = (f . x) + (g . x) ) implies h = (FuncAdd (X,Y)) . (f,g) )

assume A1: h = (FuncAdd (X,Y)) . (f,g) ; :: thesis: for x being Element of X holds h . x = (f . x) + (g . x)
let x be Element of X; :: thesis: h . x = (f . x) + (g . x)
A2: x in dom ( the addF of Y .: (f,g)) by Lm1;
thus h . x = ( the addF of Y .: (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 X holds h . x = (f . x) + (g . x) ; :: thesis: h = (FuncAdd (X,Y)) . (f,g)

now :: thesis: for x being Element of X holds ((FuncAdd (X,Y)) . (f,g)) . x = h . x

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

end;

hence h = (FuncAdd (X,Y)) . (f,g) by FUNCT_2:63; :: thesis: verum