let G, F be AbGroup; :: thesis: ( ( 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)] ) )

thus 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] ) by SUBSET_1:43; :: thesis: ( ( 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)] ) )

thus 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)] by PRVECT_3:def 1; :: thesis: ( 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)] ) )

thus 0. [:G,F:] = [(0. G),(0. F)] ; :: thesis: 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)]

thus 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)] :: thesis: verum

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

thus 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] ) by SUBSET_1:43; :: thesis: ( ( 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)] ) )

thus 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)] by PRVECT_3:def 1; :: thesis: ( 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)] ) )

thus 0. [:G,F:] = [(0. G),(0. F)] ; :: thesis: 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)]

thus 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)] :: thesis: verum

proof

let x be Element of [:G,F:]; :: thesis: for x1 being Element of G

for x2 being Element of F st x = [x1,x2] holds

- x = [(- x1),(- x2)]

let x1 be Element of G; :: thesis: for x2 being Element of F st x = [x1,x2] holds

- x = [(- x1),(- x2)]

let x2 be Element of F; :: thesis: ( x = [x1,x2] implies - x = [(- x1),(- x2)] )

assume A1: x = [x1,x2] ; :: thesis: - x = [(- x1),(- x2)]

reconsider y = [(- x1),(- x2)] as Element of [:G,F:] ;

x + y = [(x1 + (- x1)),(x2 + (- x2))] by A1, PRVECT_3:def 1

.= [(0. G),(x2 + (- x2))] by RLVECT_1:def 10

.= 0. [:G,F:] by RLVECT_1:def 10 ;

hence - x = [(- x1),(- x2)] by RLVECT_1:def 10; :: thesis: verum

end;for x2 being Element of F st x = [x1,x2] holds

- x = [(- x1),(- x2)]

let x1 be Element of G; :: thesis: for x2 being Element of F st x = [x1,x2] holds

- x = [(- x1),(- x2)]

let x2 be Element of F; :: thesis: ( x = [x1,x2] implies - x = [(- x1),(- x2)] )

assume A1: x = [x1,x2] ; :: thesis: - x = [(- x1),(- x2)]

reconsider y = [(- x1),(- x2)] as Element of [:G,F:] ;

x + y = [(x1 + (- x1)),(x2 + (- x2))] by A1, PRVECT_3:def 1

.= [(0. G),(x2 + (- x2))] by RLVECT_1:def 10

.= 0. [:G,F:] by RLVECT_1:def 10 ;

hence - x = [(- x1),(- x2)] by RLVECT_1:def 10; :: thesis: verum