let B0 be set ; :: thesis: ( B0 is R-orthogonal iff for x, y being real-valued FinSequence st x in B0 & y in B0 & x <> y holds
x,y are_orthogonal )
thus ( B0 is R-orthogonal implies for x, y being real-valued FinSequence st x in B0 & y in B0 & x <> y holds
x,y are_orthogonal ) :: thesis: ( ( for x, y being real-valued FinSequence st x in B0 & y in B0 & x <> y holds
x,y are_orthogonal ) implies B0 is R-orthogonal )

proof

assume A1: B0 is R-orthogonal ; :: thesis: for x, y being real-valued FinSequence st x in B0 & y in B0 & x <> y holds
x,y are_orthogonal
let x, y be real-valued FinSequence; :: thesis: ( x in B0 & y in B0 & x <> y implies x,y are_orthogonal )
assume ( x in B0 & y in B0 & x <> y ) ; :: thesis: x,y are_orthogonal
hence |(x,y)| = 0 by Def4, A1; :: according to EUCLID_2:def 3 :: thesis: verum

end;

assume A2: for x, y being real-valued FinSequence st x in B0 & y in B0 & x <> y holds
x,y are_orthogonal ; :: thesis: B0 is R-orthogonal
let x, y be real-valued FinSequence; :: according to EUCLID_7:def 3 :: thesis: ( x in B0 & y in B0 & x <> y implies |(x,y)| = 0 )
assume ( x in B0 & y in B0 & x <> y ) ; :: thesis: |(x,y)| = 0
then x,y are_orthogonal by A2;
hence |(x,y)| = 0 by EUCLID_2:def 3; :: thesis: verum