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: 2 * (v - (u # v)) = (2 * v) - ((1 + 1) * (u # v)) by RLVECT_1:34
.= (2 * v) - ((1 * (u # v)) + (1 * (u # v))) by RLVECT_1:def 6
.= (2 * v) - ((1 * (u # v)) + (u # v)) by RLVECT_1:def 8
.= (2 * v) - ((u # v) + (u # v)) by RLVECT_1:def 8
.= (2 * v) - (u + v) by Def2
.= ((2 * v) - v) - u by RLVECT_1:27
.= ((2 * v) - (1 * v)) - u by RLVECT_1:def 8
.= (1 * v) - u by A1, RLVECT_1:35
.= v - u by RLVECT_1:def 8 ;
A3: 1 - 2 = - 1 ;
2 * ((u # v) - u) = ((1 + 1) * (u # v)) - (2 * u) by RLVECT_1:34
.= ((1 * (u # v)) + (1 * (u # v))) - (2 * u) by RLVECT_1:def 6
.= ((u # v) + (1 * (u # v))) - (2 * u) by RLVECT_1:def 8
.= ((u # v) + (u # v)) - (2 * u) by RLVECT_1:def 8
.= (u + v) - (2 * u) by Def2
.= v + (u - (2 * u)) by RLVECT_1:def 3
.= v + ((1 * u) - (2 * u)) by RLVECT_1:def 8
.= v + ((- 1) * u) by A3, RLVECT_1:35
.= v - u by RLVECT_1:16 ;
hence ( 2 * ((u # v) - u) = v - u & 2 * (v - (u # v)) = v - u ) by A2; :: thesis: verum