let G, F be AbGroup; :: thesis: ( ( 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)*> ) )
consider I being Homomorphism of [:G,F:],(product <*G,F*>) such that
A1: ( I is bijective & ( for x being Element of G
for y being Element of F holds I . (x,y) = <*x,y*> ) ) by Th2;
thus A2: 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*> ) :: thesis: ( ( 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)*> ) )

proof

let y be set ; :: thesis: ( y is Element of (product <*G,F*>) iff ex x1 being Element of G ex x2 being Element of F st y = <*x1,x2*> )

hereby :: thesis: ( ex x1 being Element of G ex x2 being Element of F st y = <*x1,x2*> implies y is Element of (product <*G,F*>) )

assume y is Element of (product <*G,F*>) ; :: thesis: ex x1 being Element of G ex x2 being Element of F st y = <*x1,x2*>
then y in the carrier of (product <*G,F*>) ;
then y in rng I by A1, FUNCT_2:def 3;
then consider x being Element of the carrier of [:G,F:] such that
A3: y = I . x by FUNCT_2:113;
consider x1 being Element of G, x2 being Element of F such that
A4: x = [x1,x2] by SUBSET_1:43;
take x1 = x1; :: thesis: ex x2 being Element of F st y = <*x1,x2*>
take x2 = x2; :: thesis: y = <*x1,x2*>
I . (x1,x2) = <*x1,x2*> by A1;
hence y = <*x1,x2*> by A3, A4; :: thesis: verum

end;

now :: thesis: ( ex x1 being Element of G ex x2 being Element of F st y = <*x1,x2*> implies y is Element of (product <*G,F*>) )

assume ex x1 being Element of G ex x2 being Element of F st y = <*x1,x2*> ; :: thesis: y is Element of (product <*G,F*>)
then consider x1 being Element of G, x2 being Element of F such that
A5: y = <*x1,x2*> ;
A6: I . [x1,x2] in rng I by FUNCT_2:112;
I . (x1,x2) = <*x1,x2*> by A1;
hence y is Element of (product <*G,F*>) by A5, A6; :: thesis: verum

end;

hence ( ex x1 being Element of G ex x2 being Element of F st y = <*x1,x2*> implies y is Element of (product <*G,F*>) ) ; :: thesis: verum

end;

thus A7: 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)*> :: thesis: ( 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)*> ) )

proof

let x, y be Element of (product <*G,F*>); :: thesis: 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)*>
let x1, y1 be Element of G; :: thesis: for x2, y2 being Element of F st x = <*x1,x2*> & y = <*y1,y2*> holds
x + y = <*(x1 + y1),(x2 + y2)*>
let x2, y2 be Element of F; :: thesis: ( x = <*x1,x2*> & y = <*y1,y2*> implies x + y = <*(x1 + y1),(x2 + y2)*> )
assume A8: ( x = <*x1,x2*> & y = <*y1,y2*> ) ; :: thesis: x + y = <*(x1 + y1),(x2 + y2)*>
reconsider z = [x1,x2], w = [y1,y2] as Element of [:G,F:] ;
A9: z + w = [(x1 + y1),(x2 + y2)] by PRVECT_3:def 1;
( I . ((x1 + y1),(x2 + y2)) = <*(x1 + y1),(x2 + y2)*> & I . (x1,x2) = <*x1,x2*> & I . (y1,y2) = <*y1,y2*> ) by A1;
hence <*(x1 + y1),(x2 + y2)*> = x + y by A9, A8, VECTSP_1:def 20; :: thesis: verum

end;

thus A10: 0. (product <*G,F*>) = <*(0. G),(0. F)*> :: thesis: 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)*>

proof

thus 0. (product <*G,F*>) = I . (0. [:G,F:]) by MOD_4:40
.= I . ((0. G),(0. F))
.= <*(0. G),(0. F)*> by A1 ; :: thesis: verum

end;

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

proof

let x be Element of (product <*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 A11: x = <*x1,x2*> ; :: thesis: - x = <*(- x1),(- x2)*>
reconsider y = <*(- x1),(- x2)*> as Element of (product <*G,F*>) by A2;
x + y = <*(x1 + (- x1)),(x2 + (- x2))*> by A7, A11
.= <*(0. G),(x2 + (- x2))*> by RLVECT_1:def 10
.= 0. (product <*G,F*>) by A10, RLVECT_1:def 10 ;
hence - x = <*(- x1),(- x2)*> by RLVECT_1:def 10; :: thesis: verum

end;