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 )
assume A1: 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
A2: x in B0 and
A3: y in B0 and
A4: x <> y ; :: thesis: |(x,y)| = 0
x,y are_orthogonal by A1, A2, A3, A4;
hence |(x,y)| = 0 ; :: thesis: verum