:: deftheorem Def3 defines -leading_coeff ORDINAL7:def 3 :
for A being Ordinal-Sequence
for b being Ordinal
for b₃ being Ordinal-Sequence holds
( b₃ = b -leading_coeff A iff ( dom b₃ = dom A & ( for a being object st a in dom A holds
b₃ . a = b -leading_coeff (A . a) ) ) );