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,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,b * v are_Ort_wrt w,y
let a, b be Real; :: thesis: ( u,v are_Ort_wrt w,y implies a * u,b * v are_Ort_wrt w,y )
assume u,v are_Ort_wrt w,y ; :: thesis: a * u,b * v are_Ort_wrt w,y
then consider a1, a2, b1, b2 being Real such that
A1: ( u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) ) and
A2: (a1 * b1) + (a2 * b2) = 0 by Def2;
A3: a * u = (a * (a1 * w)) + (a * (a2 * y)) by A1, RLVECT_1:def 9
.= ((a * a1) * w) + (a * (a2 * y)) by RLVECT_1:def 9
.= ((a * a1) * w) + ((a * a2) * y) by RLVECT_1:def 9 ;
A4: b * v = (b * (b1 * w)) + (b * (b2 * y)) by A1, RLVECT_1:def 9
.= ((b * b1) * w) + (b * (b2 * y)) by RLVECT_1:def 9
.= ((b * b1) * w) + ((b * b2) * y) by RLVECT_1:def 9 ;
((a * a1) * (b * b1)) + ((a * a2) * (b * b2)) = (b * a) * ((a1 * b1) + (a2 * b2))
.= 0 by A2 ;
hence a * u,b * v are_Ort_wrt w,y by A3, A4, Def2; :: thesis: verum