let V be RealLinearSpace; :: thesis: for u, v being VECTOR of V holds
( 2 * ((u # v) - u) = v - u & 2 * (v - (u # v)) = v - u )
let u, v be VECTOR of V; :: thesis: ( 2 * ((u # v) - u) = v - u & 2 * (v - (u # v)) = v - u )
set p = u # v;
A1: 2 - 1 = 1 ;
A2: 1 - 2 = - 1 ;
A3: 2 * ((u # v) - u) = ((1 + 1) * (u # v)) - (2 * u) by RLVECT_1:48
.= ((1 * (u # v)) + (1 * (u # v))) - (2 * u) by RLVECT_1:def 9
.= ((u # v) + (1 * (u # v))) - (2 * u) by RLVECT_1:def 9
.= ((u # v) + (u # v)) - (2 * u) by RLVECT_1:def 9
.= (u + v) - (2 * u) by Def2
.= v + (u - (2 * u)) by RLVECT_1:def 6
.= v + ((1 * u) - (2 * u)) by RLVECT_1:def 9
.= v + ((- 1) * u) by A2, RLVECT_1:49
.= v - u by RLVECT_1:29 ;
2 * (v - (u # v)) = (2 * v) - ((1 + 1) * (u # v)) by RLVECT_1:48
.= (2 * v) - ((1 * (u # v)) + (1 * (u # v))) by RLVECT_1:def 9
.= (2 * v) - ((1 * (u # v)) + (u # v)) by RLVECT_1:def 9
.= (2 * v) - ((u # v) + (u # v)) by RLVECT_1:def 9
.= (2 * v) - (u + v) by Def2
.= ((2 * v) - v) - u by RLVECT_1:41
.= ((2 * v) - (1 * v)) - u by RLVECT_1:def 9
.= (1 * v) - u by A1, RLVECT_1:49
.= v - u by RLVECT_1:def 9 ;
hence ( 2 * ((u # v) - u) = v - u & 2 * (v - (u # v)) = v - u ) by A3; :: thesis: verum