set V = [:X,Y:];

set W = graph T;

_{1} being Element of the carrier of [:X,Y:] holds

( not b_{1} in graph T or a * b_{1} 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 A9, ZFMISC_1:87;

reconsider y = y as VECTOR of Y by A9, ZFMISC_1:87;

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 FUNCT_1:1, A9, A8

.= T . (a * x) by LOPBAN_1:def 5 ;

[(a * x),(a * y)] = a * v by PRVECT_3:18, A9;

hence a * v in graph T by A11, A10, FUNCT_1:1; :: thesis: verum

set W = graph T;

hereby :: according to RLSUB_1:def 1 :: thesis: for b_{1} being object

for b_{2} being Element of the carrier of [:X,Y:] holds

( not b_{2} in graph T or b_{1} * b_{2} in graph T )

let a be Real; :: thesis: for bfor b

( not b

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 FUNCT_1:1, A3, A1;

reconsider x1 = x1 as VECTOR of X by A3, ZFMISC_1:87;

reconsider y1 = y1 as VECTOR of Y by A3, ZFMISC_1:87;

consider x2, y2 being object such that

A5: u = [x2,y2] by RELAT_1:def 1;

reconsider x2 = x2 as VECTOR of X by A5, ZFMISC_1:87;

reconsider y2 = y2 as VECTOR of Y by A5, ZFMISC_1:87;

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 A4, FUNCT_1:1, A5, A2

.= T . (x1 + x2) by VECTSP_1:def 20 ;

[(x1 + x2),(y1 + y2)] = v + u by PRVECT_3:18, A3, A5;

hence v + u in graph T by A7, A6, FUNCT_1:1; :: thesis: verum

end;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 FUNCT_1:1, A3, A1;

reconsider x1 = x1 as VECTOR of X by A3, ZFMISC_1:87;

reconsider y1 = y1 as VECTOR of Y by A3, ZFMISC_1:87;

consider x2, y2 being object such that

A5: u = [x2,y2] by RELAT_1:def 1;

reconsider x2 = x2 as VECTOR of X by A5, ZFMISC_1:87;

reconsider y2 = y2 as VECTOR of Y by A5, ZFMISC_1:87;

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 A4, FUNCT_1:1, A5, A2

.= T . (x1 + x2) by VECTSP_1:def 20 ;

[(x1 + x2),(y1 + y2)] = v + u by PRVECT_3:18, A3, A5;

hence v + u in graph T by A7, A6, FUNCT_1:1; :: thesis: verum

( not b

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 A9, ZFMISC_1:87;

reconsider y = y as VECTOR of Y by A9, ZFMISC_1:87;

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 FUNCT_1:1, A9, A8

.= T . (a * x) by LOPBAN_1:def 5 ;

[(a * x),(a * y)] = a * v by PRVECT_3:18, A9;

hence a * v in graph T by A11, A10, FUNCT_1:1; :: thesis: verum