let B0 be set ; :: thesis: for x0 being real-valued FinSequence st B0 is R-normal & |.x0.| = 1 holds
B0 \/ {x0} is R-normal
let x0 be real-valued FinSequence; :: thesis: ( B0 is R-normal & |.x0.| = 1 implies B0 \/ {x0} is R-normal )
assume that
A1: B0 is R-normal and
A2: |.x0.| = 1 ; :: thesis: B0 \/ {x0} is R-normal
{x0} is R-normal by A2, Th15;
hence B0 \/ {x0} is R-normal by A1; :: thesis: verum