let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
for u, v, v1 being VECTOR of V holds 2 * (PProJ (w,y,u,(v # v1))) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1))
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies for u, v, v1 being VECTOR of V holds 2 * (PProJ (w,y,u,(v # v1))) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) )
assume A1: Gen w,y ; :: thesis: for u, v, v1 being VECTOR of V holds 2 * (PProJ (w,y,u,(v # v1))) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1))
let u, v, v1 be VECTOR of V; :: thesis: 2 * (PProJ (w,y,u,(v # v1))) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1))
set a1 = pr1 (w,y,u);
set a2 = pr2 (w,y,u);
set b1 = pr1 (w,y,v);
set b2 = pr2 (w,y,v);
set c1 = pr1 (w,y,v1);
set c2 = pr2 (w,y,v1);
thus 2 * (PProJ (w,y,u,(v # v1))) = ((pr1 (w,y,u)) * (2 * (pr1 (w,y,(v # v1))))) + (2 * ((pr2 (w,y,u)) * (pr2 (w,y,(v # v1)))))
.= ((pr1 (w,y,u)) * ((pr1 (w,y,v)) + (pr1 (w,y,v1)))) + ((pr2 (w,y,u)) * (2 * (pr2 (w,y,(v # v1))))) by A1, Lm18
.= ((pr1 (w,y,u)) * ((pr1 (w,y,v)) + (pr1 (w,y,v1)))) + ((pr2 (w,y,u)) * ((pr2 (w,y,v)) + (pr2 (w,y,v1)))) by A1, Lm18
.= (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) ; :: thesis: verum