theorem :: FINSEQ_2:58

for a being object holds 0 |-> a = {} ;