theorem :: VECTSP12:18

for K being Ring
for G, F being VectSp of K holds
( ( for x being set holds
( x is Vector of (product <*G,F*>) iff ex x1 being Vector of G ex x2 being Vector of F st x = <*x1,x2*> ) ) & ( for x, y being Vector of (product <*G,F*>)
for x1, y1 being Vector of G
for x2, y2 being Vector 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 Vector of (product <*G,F*>)
for x1 being Vector of G
for x2 being Vector of F st x = <*x1,x2*> holds
- x = <*(- x1),(- x2)*> ) & ( for x being Vector of (product <*G,F*>)
for x1 being Vector of G
for x2 being Vector of F
for a being Element of K st x = <*x1,x2*> holds
a * x = <*(a * x1),(a * x2)*> ) )