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
( PProJ (w,y,u,(v + v1)) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) & PProJ (w,y,u,(v - v1)) = (PProJ (w,y,u,v)) - (PProJ (w,y,u,v1)) & PProJ (w,y,(v - v1),u) = (PProJ (w,y,v,u)) - (PProJ (w,y,v1,u)) & PProJ (w,y,(v + v1),u) = (PProJ (w,y,v,u)) + (PProJ (w,y,v1,u)) )
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies for u, v, v1 being VECTOR of V holds
( PProJ (w,y,u,(v + v1)) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) & PProJ (w,y,u,(v - v1)) = (PProJ (w,y,u,v)) - (PProJ (w,y,u,v1)) & PProJ (w,y,(v - v1),u) = (PProJ (w,y,v,u)) - (PProJ (w,y,v1,u)) & PProJ (w,y,(v + v1),u) = (PProJ (w,y,v,u)) + (PProJ (w,y,v1,u)) ) )
assume A1: Gen w,y ; :: thesis: for u, v, v1 being VECTOR of V holds
( PProJ (w,y,u,(v + v1)) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) & PProJ (w,y,u,(v - v1)) = (PProJ (w,y,u,v)) - (PProJ (w,y,u,v1)) & PProJ (w,y,(v - v1),u) = (PProJ (w,y,v,u)) - (PProJ (w,y,v1,u)) & PProJ (w,y,(v + v1),u) = (PProJ (w,y,v,u)) + (PProJ (w,y,v1,u)) )
let u, v, v1 be VECTOR of V; :: thesis: ( PProJ (w,y,u,(v + v1)) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) & PProJ (w,y,u,(v - v1)) = (PProJ (w,y,u,v)) - (PProJ (w,y,u,v1)) & PProJ (w,y,(v - v1),u) = (PProJ (w,y,v,u)) - (PProJ (w,y,v1,u)) & PProJ (w,y,(v + v1),u) = (PProJ (w,y,v,u)) + (PProJ (w,y,v1,u)) )

A2: now :: thesis: for u, v, v1 being VECTOR of V holds
( PProJ (w,y,u,(v + v1)) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) & 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: ( PProJ (w,y,u,(v + v1)) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) & PProJ (w,y,u,(v - v1)) = (PProJ (w,y,u,v)) - (PProJ (w,y,u,v1)) )
A3: PProJ (w,y,u,(v - v1)) = ((pr1 (w,y,u)) * ((pr1 (w,y,v)) - (pr1 (w,y,v1)))) + ((pr2 (w,y,u)) * (pr2 (w,y,(v - v1)))) by A1, Lm17
.= ((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, Lm17
.= (PProJ (w,y,u,v)) - (PProJ (w,y,u,v1)) ;
PProJ (w,y,u,(v + v1)) = ((pr1 (w,y,u)) * ((pr1 (w,y,v)) + (pr1 (w,y,v1)))) + ((pr2 (w,y,u)) * (pr2 (w,y,(v + v1)))) by A1, Lm17
.= ((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, Lm17
.= (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) ;
hence ( PProJ (w,y,u,(v + v1)) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) & PProJ (w,y,u,(v - v1)) = (PProJ (w,y,u,v)) - (PProJ (w,y,u,v1)) ) by A3; :: thesis: verum

end;

hence ( PProJ (w,y,u,(v + v1)) = (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) & PProJ (w,y,u,(v - v1)) = (PProJ (w,y,u,v)) - (PProJ (w,y,u,v1)) ) ; :: thesis: ( PProJ (w,y,(v - v1),u) = (PProJ (w,y,v,u)) - (PProJ (w,y,v1,u)) & PProJ (w,y,(v + v1),u) = (PProJ (w,y,v,u)) + (PProJ (w,y,v1,u)) )
thus PProJ (w,y,(v - v1),u) = PProJ (w,y,u,(v - v1))
.= (PProJ (w,y,u,v)) - (PProJ (w,y,u,v1)) by A2
.= (PProJ (w,y,v,u)) - (PProJ (w,y,v1,u)) ; :: thesis: PProJ (w,y,(v + v1),u) = (PProJ (w,y,v,u)) + (PProJ (w,y,v1,u))
thus PProJ (w,y,(v + v1),u) = PProJ (w,y,u,(v + v1))
.= (PProJ (w,y,u,v)) + (PProJ (w,y,u,v1)) by A2
.= (PProJ (w,y,v,u)) + (PProJ (w,y,v1,u)) ; :: thesis: verum