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 )
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;
hence 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 ;
:: thesis: (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y
hence (a * w) + (b * y),((c * b) * w) + ((- (c * a)) * y) are_Ort_wrt w,y by A1, GEOMTRAP:34; :: thesis: verum