:: deftheorem Def12 defines lims ORDINAL6:def 12 :
for g being Ordinal-Sequence-valued Sequence
for b₂ being Ordinal-Sequence holds
( b₂ = lims g iff ( dom b₂ = dom (g . 0) & ( for a being Ordinal st a in dom b₂ holds
b₂ . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) ) );