let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
for u, v being VECTOR of V
for a being Real holds
( PProJ w,y,(a * u),v = a * (PProJ w,y,u,v) & PProJ w,y,u,(a * v) = a * (PProJ w,y,u,v) & PProJ w,y,(a * u),v = (PProJ w,y,u,v) * a & PProJ w,y,u,(a * v) = (PProJ w,y,u,v) * a )
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies for u, v being VECTOR of V
for a being Real holds
( PProJ w,y,(a * u),v = a * (PProJ w,y,u,v) & PProJ w,y,u,(a * v) = a * (PProJ w,y,u,v) & PProJ w,y,(a * u),v = (PProJ w,y,u,v) * a & PProJ w,y,u,(a * v) = (PProJ w,y,u,v) * a ) )
assume A1: Gen w,y ; :: thesis: for u, v being VECTOR of V
for a being Real holds
( PProJ w,y,(a * u),v = a * (PProJ w,y,u,v) & PProJ w,y,u,(a * v) = a * (PProJ w,y,u,v) & PProJ w,y,(a * u),v = (PProJ w,y,u,v) * a & PProJ w,y,u,(a * v) = (PProJ w,y,u,v) * a )
let u, v be VECTOR of V; :: thesis: for a being Real holds
( PProJ w,y,(a * u),v = a * (PProJ w,y,u,v) & PProJ w,y,u,(a * v) = a * (PProJ w,y,u,v) & PProJ w,y,(a * u),v = (PProJ w,y,u,v) * a & PProJ w,y,u,(a * v) = (PProJ w,y,u,v) * a )
let a be Real; :: thesis: ( PProJ w,y,(a * u),v = a * (PProJ w,y,u,v) & PProJ w,y,u,(a * v) = a * (PProJ w,y,u,v) & PProJ w,y,(a * u),v = (PProJ w,y,u,v) * a & PProJ w,y,u,(a * v) = (PProJ w,y,u,v) * a )

A2: now

let u, v be VECTOR of V; :: thesis: for a being Real holds PProJ w,y,(a * u),v = a * (PProJ w,y,u,v)
let a be Real; :: thesis: PProJ w,y,(a * u),v = a * (PProJ w,y,u,v)
PProJ w,y,(a * u),v = ((a * (pr1 w,y,u)) * (pr1 w,y,v)) + ((pr2 w,y,(a * u)) * (pr2 w,y,v)) by A1, Lm16
.= ((a * (pr1 w,y,u)) * (pr1 w,y,v)) + ((a * (pr2 w,y,u)) * (pr2 w,y,v)) by A1, Lm16
.= a * (PProJ w,y,u,v) ;
hence PProJ w,y,(a * u),v = a * (PProJ w,y,u,v) ; :: thesis: verum

end;

hence PProJ w,y,(a * u),v = a * (PProJ w,y,u,v) ; :: thesis: ( PProJ w,y,u,(a * v) = a * (PProJ w,y,u,v) & PProJ w,y,(a * u),v = (PProJ w,y,u,v) * a & PProJ w,y,u,(a * v) = (PProJ w,y,u,v) * a )
thus PProJ w,y,u,(a * v) = PProJ w,y,(a * v),u
.= a * (PProJ w,y,v,u) by A2
.= a * (PProJ w,y,u,v) ; :: thesis: ( PProJ w,y,(a * u),v = (PProJ w,y,u,v) * a & PProJ w,y,u,(a * v) = (PProJ w,y,u,v) * a )
thus PProJ w,y,(a * u),v = (PProJ w,y,u,v) * a by A2; :: thesis: PProJ w,y,u,(a * v) = (PProJ w,y,u,v) * a
thus PProJ w,y,u,(a * v) = PProJ w,y,(a * v),u
.= a * (PProJ w,y,v,u) by A2
.= (PProJ w,y,u,v) * a ; :: thesis: verum