theorem
for
G,
F being
AbGroup holds
( ( for
x being
set holds
(
x is
Element of
[: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
[: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. [:G,F:] = [(0. G),(0. F)] & ( for
x being
Element of
[:G,F:] for
x1 being
Element of
G for
x2 being
Element of
F st
x = [x1,x2] holds
- x = [(- x1),(- x2)] ) )