let V be RealLinearSpace; :: thesis: for u, v, w, y being VECTOR of V st Gen w,y holds
( 2 * (pr1 (w,y,(u # v))) = (pr1 (w,y,u)) + (pr1 (w,y,v)) & 2 * (pr2 (w,y,(u # v))) = (pr2 (w,y,u)) + (pr2 (w,y,v)) )
let u, v, w, y be VECTOR of V; :: thesis: ( Gen w,y implies ( 2 * (pr1 (w,y,(u # v))) = (pr1 (w,y,u)) + (pr1 (w,y,v)) & 2 * (pr2 (w,y,(u # v))) = (pr2 (w,y,u)) + (pr2 (w,y,v)) ) )
assume A1: Gen w,y ; :: thesis: ( 2 * (pr1 (w,y,(u # v))) = (pr1 (w,y,u)) + (pr1 (w,y,v)) & 2 * (pr2 (w,y,(u # v))) = (pr2 (w,y,u)) + (pr2 (w,y,v)) )
set p = u # v;
2 * (u # v) = (1 + 1) * (u # v)
.= (1 * (u # v)) + (1 * (u # v)) by RLVECT_1:def 6
.= (u # v) + (1 * (u # v)) by RLVECT_1:def 8
.= (u # v) + (u # v) by RLVECT_1:def 8
.= u + v by Def2 ;
then ( 2 * (pr1 (w,y,(u # v))) = pr1 (w,y,(u + v)) & 2 * (pr2 (w,y,(u # v))) = pr2 (w,y,(u + v)) ) by A1, Lm17;
hence ( 2 * (pr1 (w,y,(u # v))) = (pr1 (w,y,u)) + (pr1 (w,y,v)) & 2 * (pr2 (w,y,(u # v))) = (pr2 (w,y,u)) + (pr2 (w,y,v)) ) by A1, Lm17; :: thesis: verum