for W being Universe
for A1 being Ordinal of W
for phi being Ordinal-Sequence of W holds A1 in dom phi