let V be RealLinearSpace; :: thesis: for w, y, u, v 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 w, y, u, v 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 9
.= (u # v) + (1 * (u # v)) by RLVECT_1:def 9
.= (u # v) + (u # v) by RLVECT_1:def 9
.= 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