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