let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
for u, v being VECTOR of V holds
( u, 0. V are_Ort_wrt w,y & 0. V,v are_Ort_wrt w,y )
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies for u, v being VECTOR of V holds
( u, 0. V are_Ort_wrt w,y & 0. V,v are_Ort_wrt w,y ) )
assume A1: Gen w,y ; :: thesis: for u, v being VECTOR of V holds
( u, 0. V are_Ort_wrt w,y & 0. V,v are_Ort_wrt w,y )
let u, v be VECTOR of V; :: thesis: ( u, 0. V are_Ort_wrt w,y & 0. V,v are_Ort_wrt w,y )
consider a1, a2 being Real such that
A2: u = (a1 * w) + (a2 * y) by A1;
consider b1, b2 being Real such that
A3: v = (b1 * w) + (b2 * y) by A1;
A4: 0. V = (0. V) + (0. V) by RLVECT_1:4
.= (0 * w) + (0. V) by RLVECT_1:10
.= (0 * w) + (0 * y) by RLVECT_1:10 ;
(a1 * 0) + (a2 * 0) = 0 ;
hence u, 0. V are_Ort_wrt w,y by A2, A4; :: thesis: 0. V,v are_Ort_wrt w,y
(0 * b1) + (0 * b2) = 0 ;
hence 0. V,v are_Ort_wrt w,y by A3, A4; :: thesis: verum