set V = [:X,Y:];
set W = graph T;
hereby RLSUB_1:def 1 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:];
( 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
;
v + u in graph Tconsider 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;
verum
end;
let a be Real; 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:]; ( not v in graph T or a * v in graph T )
assume A8:
v in graph T
; 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; verum