let X be set ; :: thesis: ( X is empty implies X is R-orthogonal )
assume A1: X is empty ; :: thesis: X is R-orthogonal
let f be real-valued FinSequence; :: according to EUCLID_7:def 3 :: thesis: for y being real-valued FinSequence st f in X & y in X & f <> y holds
|(f,y)| = 0
thus for y being real-valued FinSequence st f in X & y in X & f <> y holds
|(f,y)| = 0 by A1; :: thesis: verum