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