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 by FINSEQ_1:40;
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 by FINSEQ_1:40; :: thesis: verum
end;
hence for b1 being non empty FinSequence of R st b1 = <*(1. R)*> holds
( b1 is quadratic & not b1 is trivial ) by D, B; :: thesis: verum