let V be RealLinearSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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; :: thesis: verum