let V be RealLinearSpace; :: thesis: for u, v, w, y being VECTOR of V st Gen w,y holds
( u,v are_Ort_wrt w,y iff for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds
(a1 * b1) + (a2 * b2) = 0 )
let u, v, w, y be VECTOR of V; :: thesis: ( Gen w,y implies ( u,v are_Ort_wrt w,y iff for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds
(a1 * b1) + (a2 * b2) = 0 ) )
assume A1: Gen w,y ; :: thesis: ( u,v are_Ort_wrt w,y iff for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds
(a1 * b1) + (a2 * b2) = 0 )

hereby :: thesis: ( ( for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds
(a1 * b1) + (a2 * b2) = 0 ) implies u,v are_Ort_wrt w,y )

assume u,v are_Ort_wrt w,y ; :: thesis: for a1', a2', b1', b2' being Real st u = (a1' * w) + (a2' * y) & v = (b1' * w) + (b2' * y) holds
0 = (a1' * b1') + (a2' * b2')
then consider a1, a2, b1, b2 being Real such that
A2: u = (a1 * w) + (a2 * y) and
A3: v = (b1 * w) + (b2 * y) and
A4: (a1 * b1) + (a2 * b2) = 0 by Def2;
let a1', a2', b1', b2' be Real; :: thesis: ( u = (a1' * w) + (a2' * y) & v = (b1' * w) + (b2' * y) implies 0 = (a1' * b1') + (a2' * b2') )
assume that
A5: u = (a1' * w) + (a2' * y) and
A6: v = (b1' * w) + (b2' * y) ; :: thesis: 0 = (a1' * b1') + (a2' * b2')
A7: b1 = b1' by A1, A3, A6, Lm4;
( a1 = a1' & a2 = a2' ) by A1, A2, A5, Lm4;
hence 0 = (a1' * b1') + (a2' * b2') by A1, A3, A4, A6, A7, Lm4; :: thesis: verum

end;

consider a1, a2 being Real such that
A8: u = (a1 * w) + (a2 * y) by A1, Def1;
consider b1, b2 being Real such that
A9: v = (b1 * w) + (b2 * y) by A1, Def1;
assume for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds
(a1 * b1) + (a2 * b2) = 0 ; :: thesis: u,v are_Ort_wrt w,y
then (a1 * b1) + (a2 * b2) = 0 by A8, A9;
hence u,v are_Ort_wrt w,y by A8, A9, Def2; :: thesis: verum