set f = <*1,2*>;
for n being Nat st n in dom <*1,2*> holds
<*1,2*> . n > 0
then A1:
( not <*1,2*> is empty & <*1,2*> is positive )
;
dom <*1,2*> = {1,2}
by FINSEQ_1:92;
then A2:
( 1 in dom <*1,2*> & 2 in dom <*1,2*> )
by TARSKI:def 2;
( <*1,2*> . 1 = 1 & <*1,2*> . 2 = 2 )
by FINSEQ_1:44;
then
not <*1,2*> is constant
by A2;
hence
ex b1 being real-valued FinSequence st
( not b1 is empty & not b1 is constant & b1 is positive )
by A1; verum