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

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, Lm16
.= ((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, Lm16
.= (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, Lm16
.= ((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, Lm16
.= (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