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;