let K be Ring; :: thesis: 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)*> ) )

let G, F be VectSp of K; :: thesis: ( ( 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)*> ) )

consider I being Function of [:G,F:],(product <*G,F*>) such that

A1: ( I is one-to-one & I is onto & ( for x being Vector of G

for y being Vector of F holds I . (x,y) = <*x,y*> ) & ( for v, w being Vector of [:G,F:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of [:G,F:]

for r being Element of K holds I . (r * v) = r * (I . v) ) & 0. (product <*G,F*>) = I . (0. [:G,F:]) ) by Th12;

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

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

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)*> ) )

for x1 being Vector of G

for x2 being Vector of F st x = <*x1,x2*> holds

- x = <*(- x1),(- x2)*> :: thesis: 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)*>

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

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

let G, F be VectSp of K; :: thesis: ( ( 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)*> ) )

consider I being Function of [:G,F:],(product <*G,F*>) such that

A1: ( I is one-to-one & I is onto & ( for x being Vector of G

for y being Vector of F holds I . (x,y) = <*x,y*> ) & ( for v, w being Vector of [:G,F:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Vector of [:G,F:]

for r being Element of K holds I . (r * v) = r * (I . v) ) & 0. (product <*G,F*>) = I . (0. [:G,F:]) ) by Th12;

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

proof

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

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

assume
y is Vector of (product <*G,F*>)
; :: thesis: ex x1 being Vector of G ex x2 being Vector of F st y = <*x1,x2*>

then consider x being Element of the carrier of [:G,F:] such that

A3: y = I . x by A1, FUNCT_2:113;

consider x1 being Vector of G, x2 being Vector of F such that

A4: x = [x1,x2] by SUBSET_1:43;

take x1 = x1; :: thesis: ex x2 being Vector 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;then consider x being Element of the carrier of [:G,F:] such that

A3: y = I . x by A1, FUNCT_2:113;

consider x1 being Vector of G, x2 being Vector of F such that

A4: x = [x1,x2] by SUBSET_1:43;

take x1 = x1; :: thesis: ex x2 being Vector 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

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

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

then consider x1 being Vector of G, x2 being Vector 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 Vector of (product <*G,F*>) by A5, A6; :: thesis: verum

end;then consider x1 being Vector of G, x2 being Vector 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 Vector of (product <*G,F*>) by A5, A6; :: thesis: verum

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

proof

thus A10:
0. (product <*G,F*>) = <*(0. G),(0. F)*>
:: thesis: ( ( for x being Vector of (product <*G,F*>)
let x, y be Vector of (product <*G,F*>); :: thesis: 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)*>

let x1, y1 be Vector of G; :: thesis: for x2, y2 being Vector of F st x = <*x1,x2*> & y = <*y1,y2*> holds

x + y = <*(x1 + y1),(x2 + y2)*>

let x2, y2 be Vector 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 Vector 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 A1, A9, A8; :: thesis: verum

end;for x2, y2 being Vector of F st x = <*x1,x2*> & y = <*y1,y2*> holds

x + y = <*(x1 + y1),(x2 + y2)*>

let x1, y1 be Vector of G; :: thesis: for x2, y2 being Vector of F st x = <*x1,x2*> & y = <*y1,y2*> holds

x + y = <*(x1 + y1),(x2 + y2)*>

let x2, y2 be Vector 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 Vector 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 A1, A9, A8; :: thesis: verum

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)*> ) )

proof

thus
for x being Vector of (product <*G,F*>)
I . ((0. G),(0. F)) = <*(0. G),(0. F)*>
by A1;

hence 0. (product <*G,F*>) = <*(0. G),(0. F)*> by A1; :: thesis: verum

end;hence 0. (product <*G,F*>) = <*(0. G),(0. F)*> by A1; :: thesis: verum

for x1 being Vector of G

for x2 being Vector of F st x = <*x1,x2*> holds

- x = <*(- x1),(- x2)*> :: thesis: 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)*>

proof

thus
for x being Vector of (product <*G,F*>)
let x be Vector of (product <*G,F*>); :: thesis: for x1 being Vector of G

for x2 being Vector of F st x = <*x1,x2*> holds

- x = <*(- x1),(- x2)*>

let x1 be Vector of G; :: thesis: for x2 being Vector of F st x = <*x1,x2*> holds

- x = <*(- x1),(- x2)*>

let x2 be Vector of F; :: thesis: ( x = <*x1,x2*> implies - x = <*(- x1),(- x2)*> )

assume A11: x = <*x1,x2*> ; :: thesis: - x = <*(- x1),(- x2)*>

reconsider y = <*(- x1),(- x2)*> as Vector 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;for x2 being Vector of F st x = <*x1,x2*> holds

- x = <*(- x1),(- x2)*>

let x1 be Vector of G; :: thesis: for x2 being Vector of F st x = <*x1,x2*> holds

- x = <*(- x1),(- x2)*>

let x2 be Vector of F; :: thesis: ( x = <*x1,x2*> implies - x = <*(- x1),(- x2)*> )

assume A11: x = <*x1,x2*> ; :: thesis: - x = <*(- x1),(- x2)*>

reconsider y = <*(- x1),(- x2)*> as Vector 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

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

proof

let x be Vector of (product <*G,F*>); :: thesis: 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)*>

let x1 be Vector of G; :: thesis: for x2 being Vector of F

for a being Element of K st x = <*x1,x2*> holds

a * x = <*(a * x1),(a * x2)*>

let x2 be Vector of F; :: thesis: for a being Element of K st x = <*x1,x2*> holds

a * x = <*(a * x1),(a * x2)*>

let a be Element of K; :: thesis: ( x = <*x1,x2*> implies a * x = <*(a * x1),(a * x2)*> )

assume A12: x = <*x1,x2*> ; :: thesis: a * x = <*(a * x1),(a * x2)*>

reconsider y = [x1,x2] as Vector of [:G,F:] ;

A13: <*x1,x2*> = I . (x1,x2) by A1;

I . (a * y) = I . ((a * x1),(a * x2)) by YDef2

.= <*(a * x1),(a * x2)*> by A1 ;

hence a * x = <*(a * x1),(a * x2)*> by A1, A12, A13; :: thesis: verum

end;for x2 being Vector of F

for a being Element of K st x = <*x1,x2*> holds

a * x = <*(a * x1),(a * x2)*>

let x1 be Vector of G; :: thesis: for x2 being Vector of F

for a being Element of K st x = <*x1,x2*> holds

a * x = <*(a * x1),(a * x2)*>

let x2 be Vector of F; :: thesis: for a being Element of K st x = <*x1,x2*> holds

a * x = <*(a * x1),(a * x2)*>

let a be Element of K; :: thesis: ( x = <*x1,x2*> implies a * x = <*(a * x1),(a * x2)*> )

assume A12: x = <*x1,x2*> ; :: thesis: a * x = <*(a * x1),(a * x2)*>

reconsider y = [x1,x2] as Vector of [:G,F:] ;

A13: <*x1,x2*> = I . (x1,x2) by A1;

I . (a * y) = I . ((a * x1),(a * x2)) by YDef2

.= <*(a * x1),(a * x2)*> by A1 ;

hence a * x = <*(a * x1),(a * x2)*> by A1, A12, A13; :: thesis: verum