theorem
for
K being
Ring for
G,
F being non
empty ModuleStr over
K holds
( ( for
x being
set holds
(
x is
Vector of
[: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
[: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. [:G,F:] = [(0. G),(0. F)] & ( for
x being
Vector of
[: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)] ) )
by YDef2, PRVECT_3:def 1, SUBSET_1:43;