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 that
A2: x in B0 and
A3: y in B0 and
A4: x <> y ; :: thesis: x,y are_orthogonal
thus |(x,y)| = 0 by A1, A2, A3, A4, Def3; :: according to RVSUM_1:def 17 :: thesis: verum

end;

assume A5: 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 that
A6: x in B0 and
A7: y in B0 and
A8: x <> y ; :: thesis: |(x,y)| = 0
x,y are_orthogonal by A5, A6, A7, A8;
hence |(x,y)| = 0 by RVSUM_1:def 17; :: thesis: verum