theorem :: GROUP_14:4

for G, F being AbGroup holds
( ( for x being set holds
( x is Element of (product <*G,F*>) iff ex x1 being Element of G ex x2 being Element of F st x = <*x1,x2*> ) ) & ( for x, y being Element of (product <*G,F*>)
for x1, y1 being Element of G
for x2, y2 being Element of F st x = <*x1,x2*> & y = <*y1,y2*> holds
x + y = <*(x1 + y1),(x2 + y2)*> ) & 0. (product <*G,F*>) = <*(0. G),(0. F)*> & ( for x being Element of (product <*G,F*>)
for x1 being Element of G
for x2 being Element of F st x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*> ) )