:: deftheorem Def4 defines *^ ORDINAL3:def 4 :
for C being Ordinal
for fi, b₃ being Ordinal-Sequence holds
( b₃ = fi *^ C iff ( dom b₃ = dom fi & ( for A being Ordinal st A in dom fi holds
b₃ . A = (fi . A) *^ C ) ) );