let V be RealLinearSpace; :: thesis: for u, v, w, y being VECTOR of V
for a, b being Real st u,v are_Ort_wrt w,y holds
( a * u,v are_Ort_wrt w,y & u,b * v are_Ort_wrt w,y )
let u, v, w, y be VECTOR of V; :: thesis: for a, b being Real st u,v are_Ort_wrt w,y holds
( a * u,v are_Ort_wrt w,y & u,b * v are_Ort_wrt w,y )
let a, b be Real; :: thesis: ( u,v are_Ort_wrt w,y implies ( a * u,v are_Ort_wrt w,y & u,b * v are_Ort_wrt w,y ) )
A1: ( v = 1 * v & u = 1 * u ) by RLVECT_1:def 8;
assume u,v are_Ort_wrt w,y ; :: thesis: ( a * u,v are_Ort_wrt w,y & u,b * v are_Ort_wrt w,y )
hence ( a * u,v are_Ort_wrt w,y & u,b * v are_Ort_wrt w,y ) by A1, Th6; :: thesis: verum