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 A1: ( B0 is R-normal & |.x0.| = 1 ) ; :: thesis: B0 \/ {x0} is R-normal
then {x0} is R-normal by Th19;
hence B0 \/ {x0} is R-normal by A1; :: thesis: verum