let x be real-valued FinSequence; :: according to EUCLID_7:def 4 :: thesis: ( x in B0 \/ B1 implies |.x.| = 1 )
assume x in B0 \/ B1 ; :: thesis: |.x.| = 1
then ( x in B0 or x in B1 ) by XBOOLE_0:def 3;
hence |.x.| = 1 by Def4; :: thesis: verum