let V be RealLinearSpace; :: thesis: for u, v, w, y being VECTOR of V
for a being Real st Gen w,y holds
( pr1 (w,y,(u + v)) = (pr1 (w,y,u)) + (pr1 (w,y,v)) & pr2 (w,y,(u + v)) = (pr2 (w,y,u)) + (pr2 (w,y,v)) & pr1 (w,y,(u - v)) = (pr1 (w,y,u)) - (pr1 (w,y,v)) & pr2 (w,y,(u - v)) = (pr2 (w,y,u)) - (pr2 (w,y,v)) & pr1 (w,y,(a * u)) = a * (pr1 (w,y,u)) & pr2 (w,y,(a * u)) = a * (pr2 (w,y,u)) )
let u, v, w, y be VECTOR of V; :: thesis: for a being Real st Gen w,y holds
( pr1 (w,y,(u + v)) = (pr1 (w,y,u)) + (pr1 (w,y,v)) & pr2 (w,y,(u + v)) = (pr2 (w,y,u)) + (pr2 (w,y,v)) & pr1 (w,y,(u - v)) = (pr1 (w,y,u)) - (pr1 (w,y,v)) & pr2 (w,y,(u - v)) = (pr2 (w,y,u)) - (pr2 (w,y,v)) & pr1 (w,y,(a * u)) = a * (pr1 (w,y,u)) & pr2 (w,y,(a * u)) = a * (pr2 (w,y,u)) )
let a be Real; :: thesis: ( Gen w,y implies ( pr1 (w,y,(u + v)) = (pr1 (w,y,u)) + (pr1 (w,y,v)) & pr2 (w,y,(u + v)) = (pr2 (w,y,u)) + (pr2 (w,y,v)) & pr1 (w,y,(u - v)) = (pr1 (w,y,u)) - (pr1 (w,y,v)) & pr2 (w,y,(u - v)) = (pr2 (w,y,u)) - (pr2 (w,y,v)) & pr1 (w,y,(a * u)) = a * (pr1 (w,y,u)) & pr2 (w,y,(a * u)) = a * (pr2 (w,y,u)) ) )
set p1u = pr1 (w,y,u);
set p2u = pr2 (w,y,u);
set p1v = pr1 (w,y,v);
set p2v = pr2 (w,y,v);
assume A1: Gen w,y ; :: thesis: ( pr1 (w,y,(u + v)) = (pr1 (w,y,u)) + (pr1 (w,y,v)) & pr2 (w,y,(u + v)) = (pr2 (w,y,u)) + (pr2 (w,y,v)) & pr1 (w,y,(u - v)) = (pr1 (w,y,u)) - (pr1 (w,y,v)) & pr2 (w,y,(u - v)) = (pr2 (w,y,u)) - (pr2 (w,y,v)) & pr1 (w,y,(a * u)) = a * (pr1 (w,y,u)) & pr2 (w,y,(a * u)) = a * (pr2 (w,y,u)) )
then A2: u = ((pr1 (w,y,u)) * w) + ((pr2 (w,y,u)) * y) by Lm15;
A3: v = ((pr1 (w,y,v)) * w) + ((pr2 (w,y,v)) * y) by A1, Lm15;
then u + v = ((((pr1 (w,y,u)) * w) + ((pr2 (w,y,u)) * y)) + ((pr1 (w,y,v)) * w)) + ((pr2 (w,y,v)) * y) by A2, RLVECT_1:def 3
.= ((((pr1 (w,y,u)) * w) + ((pr1 (w,y,v)) * w)) + ((pr2 (w,y,u)) * y)) + ((pr2 (w,y,v)) * y) by RLVECT_1:def 3
.= (((pr1 (w,y,u)) * w) + ((pr1 (w,y,v)) * w)) + (((pr2 (w,y,u)) * y) + ((pr2 (w,y,v)) * y)) by RLVECT_1:def 3
.= (((pr1 (w,y,u)) + (pr1 (w,y,v))) * w) + (((pr2 (w,y,u)) * y) + ((pr2 (w,y,v)) * y)) by RLVECT_1:def 6
.= (((pr1 (w,y,u)) + (pr1 (w,y,v))) * w) + (((pr2 (w,y,u)) + (pr2 (w,y,v))) * y) by RLVECT_1:def 6 ;
hence ( pr1 (w,y,(u + v)) = (pr1 (w,y,u)) + (pr1 (w,y,v)) & pr2 (w,y,(u + v)) = (pr2 (w,y,u)) + (pr2 (w,y,v)) ) by A1, Lm16; :: thesis: ( pr1 (w,y,(u - v)) = (pr1 (w,y,u)) - (pr1 (w,y,v)) & pr2 (w,y,(u - v)) = (pr2 (w,y,u)) - (pr2 (w,y,v)) & pr1 (w,y,(a * u)) = a * (pr1 (w,y,u)) & pr2 (w,y,(a * u)) = a * (pr2 (w,y,u)) )
u - v = (((pr1 (w,y,u)) - (pr1 (w,y,v))) * w) + (((pr2 (w,y,u)) - (pr2 (w,y,v))) * y) by A2, A3, Lm12;
hence ( pr1 (w,y,(u - v)) = (pr1 (w,y,u)) - (pr1 (w,y,v)) & pr2 (w,y,(u - v)) = (pr2 (w,y,u)) - (pr2 (w,y,v)) ) by A1, Lm16; :: thesis: ( pr1 (w,y,(a * u)) = a * (pr1 (w,y,u)) & pr2 (w,y,(a * u)) = a * (pr2 (w,y,u)) )
a * u = ((a * (pr1 (w,y,u))) * w) + ((a * (pr2 (w,y,u))) * y) by A2, Lm13;
hence ( pr1 (w,y,(a * u)) = a * (pr1 (w,y,u)) & pr2 (w,y,(a * u)) = a * (pr2 (w,y,u)) ) by A1, Lm16; :: thesis: verum