set f = <*(1. R)*>;
1 in Seg 1 by FINSEQ_1:2, TARSKI:def 1;
then B: 1 in dom <*(1. R)*> by FINSEQ_1:38;
D: <*(1. R)*> . 1 = 1. R ;

now :: thesis: for i being Element of dom <*(1. R)*> holds <*(1. R)*> . i is square

let i be Element of dom <*(1. R)*>; :: thesis: <*(1. R)*> . i is square
dom <*(1. R)*> = Seg 1 by FINSEQ_1:38;
then i = 1 by TARSKI:def 1, FINSEQ_1:2;
hence <*(1. R)*> . i is square ; :: thesis: verum

end;

hence for b₁ being non empty FinSequence of R st b₁ = <*(1. R)*> holds
( b₁ is quadratic & not b₁ is trivial ) by D, B; :: thesis: verum