let V be RealLinearSpace; for w, y being VECTOR of V st Gen w,y holds
for a, b, c being Real holds
( PProJ (w,y,((a * w) + (b * y)),(((c * b) * w) + ((- (c * a)) * y))) = 0 & (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y )
let w, y be VECTOR of V; ( Gen w,y implies for a, b, c being Real holds
( PProJ (w,y,((a * w) + (b * y)),(((c * b) * w) + ((- (c * a)) * y))) = 0 & (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y ) )
assume A1:
Gen w,y
; for a, b, c being Real holds
( PProJ (w,y,((a * w) + (b * y)),(((c * b) * w) + ((- (c * a)) * y))) = 0 & (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y )
let a, b, c be Real; ( PProJ (w,y,((a * w) + (b * y)),(((c * b) * w) + ((- (c * a)) * y))) = 0 & (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y )
reconsider a = a, b = b, c = c as Real ;
A2:
( pr2 (w,y,((a * w) + (b * y))) = b & pr2 (w,y,(((c * b) * w) + ((- (c * a)) * y))) = - (c * a) )
by A1, GEOMTRAP:def 5;
( pr1 (w,y,((a * w) + (b * y))) = a & pr1 (w,y,(((c * b) * w) + ((- (c * a)) * y))) = c * b )
by A1, GEOMTRAP:def 4;
then PProJ (w,y,((a * w) + (b * y)),(((c * b) * w) + ((- (c * a)) * y))) =
(a * (b * c)) + (b * (- (c * a)))
by A2, GEOMTRAP:def 6
.=
0
;
hence
( PProJ (w,y,((a * w) + (b * y)),(((c * b) * w) + ((- (c * a)) * y))) = 0 & (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y )
by A1, GEOMTRAP:32; verum