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) )

A1: now

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

now

let x be Element of X; :: thesis: ((FuncAdd X,Y) . f,g) . x = h . x
A3: 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 A3, FUNCOP_1:28
.= h . x by A2 ; :: thesis: verum

end;

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

end;

now

assume A4: 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)
A5: x in dom (the addF of Y .: f,g) by Lm1;
thus h . x = (the addF of Y .: f,g) . x by A4, Def1
.= (f . x) + (g . x) by A5, FUNCOP_1:28 ; :: thesis: verum

end;

hence ( h = (FuncAdd X,Y) . f,g iff for x being Element of X holds h . x = (f . x) + (g . x) ) by A1; :: thesis: verum