set f = <*0*>;
for n being object holds <*0*> . n is triangular

proof

let n be object ; :: thesis: <*0*> . n is triangular

per cases ( n in dom <*0*> or not n in dom <*0*> ) ;

suppose n in dom <*0*> ; :: thesis: <*0*> . n is triangular

then n in Seg 1 by FINSEQ_1:def 8;
then n = 1 by TARSKI:def 1, FINSEQ_1:2;
hence <*0*> . n is triangular by FINSEQ_1:def 8; :: thesis: verum

end;

suppose not n in dom <*0*> ; :: thesis: <*0*> . n is triangular

hence <*0*> . n is triangular by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

hence for b₁ being FinSequence st b₁ = <*0*> holds
b₁ is triangular-valued ; :: thesis: verum