:: deftheorem defines |-> FINSEQ_2:def 2 :
for i being natural Number
for a being object holds i |-> a = (Seg i) --> a;