set f = <*1,2*>;
for n being Nat st n in dom <*1,2*> holds
<*1,2*> . n > 0
proof
let n be Nat; :: thesis: ( n in dom <*1,2*> implies <*1,2*> . n > 0 )
assume n in dom <*1,2*> ; :: thesis: <*1,2*> . n > 0
then n in Seg (len <*1,2*>) by FINSEQ_1:def 3;
then n in {1,2} by FINSEQ_1:2, FINSEQ_1:44;
then ( n = 1 or n = 2 ) by TARSKI:def 2;
hence <*1,2*> . n > 0 by FINSEQ_1:44; :: thesis: verum
end;
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; :: thesis: verum