let V be RealLinearSpace; :: thesis: for x, y, u, v being VECTOR of V
for a being Real st Gen x,y holds
( pr1 x,y,(u + v) = (pr1 x,y,u) + (pr1 x,y,v) & pr2 x,y,(u + v) = (pr2 x,y,u) + (pr2 x,y,v) & pr1 x,y,(u - v) = (pr1 x,y,u) - (pr1 x,y,v) & pr2 x,y,(u - v) = (pr2 x,y,u) - (pr2 x,y,v) & pr1 x,y,(a * u) = a * (pr1 x,y,u) & pr2 x,y,(a * u) = a * (pr2 x,y,u) )
let x, y, u, v be VECTOR of V; :: thesis: for a being Real st Gen x,y holds
( pr1 x,y,(u + v) = (pr1 x,y,u) + (pr1 x,y,v) & pr2 x,y,(u + v) = (pr2 x,y,u) + (pr2 x,y,v) & pr1 x,y,(u - v) = (pr1 x,y,u) - (pr1 x,y,v) & pr2 x,y,(u - v) = (pr2 x,y,u) - (pr2 x,y,v) & pr1 x,y,(a * u) = a * (pr1 x,y,u) & pr2 x,y,(a * u) = a * (pr2 x,y,u) )
let a be Real; :: thesis: ( Gen x,y implies ( pr1 x,y,(u + v) = (pr1 x,y,u) + (pr1 x,y,v) & pr2 x,y,(u + v) = (pr2 x,y,u) + (pr2 x,y,v) & pr1 x,y,(u - v) = (pr1 x,y,u) - (pr1 x,y,v) & pr2 x,y,(u - v) = (pr2 x,y,u) - (pr2 x,y,v) & pr1 x,y,(a * u) = a * (pr1 x,y,u) & pr2 x,y,(a * u) = a * (pr2 x,y,u) ) )
assume A1: Gen x,y ; :: thesis: ( pr1 x,y,(u + v) = (pr1 x,y,u) + (pr1 x,y,v) & pr2 x,y,(u + v) = (pr2 x,y,u) + (pr2 x,y,v) & pr1 x,y,(u - v) = (pr1 x,y,u) - (pr1 x,y,v) & pr2 x,y,(u - v) = (pr2 x,y,u) - (pr2 x,y,v) & pr1 x,y,(a * u) = a * (pr1 x,y,u) & pr2 x,y,(a * u) = a * (pr2 x,y,u) )
set p1u = pr1 x,y,u;
set p2u = pr2 x,y,u;
set p1v = pr1 x,y,v;
set p2v = pr2 x,y,v;
A2: ( u = ((pr1 x,y,u) * x) + ((pr2 x,y,u) * y) & v = ((pr1 x,y,v) * x) + ((pr2 x,y,v) * y) ) by A1, Lm5;
then u + v = ((((pr1 x,y,u) * x) + ((pr2 x,y,u) * y)) + ((pr1 x,y,v) * x)) + ((pr2 x,y,v) * y) by RLVECT_1:def 6
.= ((((pr1 x,y,u) * x) + ((pr1 x,y,v) * x)) + ((pr2 x,y,u) * y)) + ((pr2 x,y,v) * y) by RLVECT_1:def 6
.= (((pr1 x,y,u) * x) + ((pr1 x,y,v) * x)) + (((pr2 x,y,u) * y) + ((pr2 x,y,v) * y)) by RLVECT_1:def 6
.= (((pr1 x,y,u) + (pr1 x,y,v)) * x) + (((pr2 x,y,u) * y) + ((pr2 x,y,v) * y)) by RLVECT_1:def 9
.= (((pr1 x,y,u) + (pr1 x,y,v)) * x) + (((pr2 x,y,u) + (pr2 x,y,v)) * y) by RLVECT_1:def 9 ;
hence ( pr1 x,y,(u + v) = (pr1 x,y,u) + (pr1 x,y,v) & pr2 x,y,(u + v) = (pr2 x,y,u) + (pr2 x,y,v) ) by A1, Lm6; :: thesis: ( pr1 x,y,(u - v) = (pr1 x,y,u) - (pr1 x,y,v) & pr2 x,y,(u - v) = (pr2 x,y,u) - (pr2 x,y,v) & pr1 x,y,(a * u) = a * (pr1 x,y,u) & pr2 x,y,(a * u) = a * (pr2 x,y,u) )
u - v = (((pr1 x,y,u) - (pr1 x,y,v)) * x) + (((pr2 x,y,u) - (pr2 x,y,v)) * y) by A2, Lm1;
hence ( pr1 x,y,(u - v) = (pr1 x,y,u) - (pr1 x,y,v) & pr2 x,y,(u - v) = (pr2 x,y,u) - (pr2 x,y,v) ) by A1, Lm6; :: thesis: ( pr1 x,y,(a * u) = a * (pr1 x,y,u) & pr2 x,y,(a * u) = a * (pr2 x,y,u) )
a * u = ((a * (pr1 x,y,u)) * x) + ((a * (pr2 x,y,u)) * y) by A2, Lm2;
hence ( pr1 x,y,(a * u) = a * (pr1 x,y,u) & pr2 x,y,(a * u) = a * (pr2 x,y,u) ) by A1, Lm6; :: thesis: verum