set V = [:X,Y:];
set W = graph T;
hereby :: according to RLSUB_1:def 1 :: thesis: for b1 being object
for b2 being Element of the carrier of [:X,Y:] holds
( not b2 in graph T or b1 * b2 in graph T )
let v, u be VECTOR of [:X,Y:]; :: thesis: ( v in graph T & u in graph T implies v + u in graph T )
assume that
A1: v in graph T and
A2: u in graph T ; :: thesis: v + u in graph T
consider x1, y1 being object such that
A3: v = [x1,y1] by RELAT_1:def 1;
A4: ( x1 in dom T & y1 = T . x1 ) by ;
reconsider x1 = x1 as VECTOR of X by ;
reconsider y1 = y1 as VECTOR of Y by ;
consider x2, y2 being object such that
A5: u = [x2,y2] by RELAT_1:def 1;
reconsider x2 = x2 as VECTOR of X by ;
reconsider y2 = y2 as VECTOR of Y by ;
x1 + x2 in the carrier of X ;
then A6: x1 + x2 in dom T by FUNCT_2:def 1;
A7: y1 + y2 = (T . x1) + (T . x2) by
.= T . (x1 + x2) by VECTSP_1:def 20 ;
[(x1 + x2),(y1 + y2)] = v + u by ;
hence v + u in graph T by ; :: thesis: verum
end;
let a be Real; :: thesis: for b1 being Element of the carrier of [:X,Y:] holds
( not b1 in graph T or a * b1 in graph T )

let v be VECTOR of [:X,Y:]; :: thesis: ( not v in graph T or a * v in graph T )
assume A8: v in graph T ; :: thesis: a * v in graph T
consider x, y being object such that
A9: v = [x,y] by RELAT_1:def 1;
reconsider x = x as VECTOR of X by ;
reconsider y = y as VECTOR of Y by ;
a * x in the carrier of X ;
then A10: a * x in dom T by FUNCT_2:def 1;
A11: a * y = a * (T . x) by
.= T . (a * x) by LOPBAN_1:def 5 ;
[(a * x),(a * y)] = a * v by ;
hence a * v in graph T by ; :: thesis: verum