let W be Universe; :: thesis: for A1 being Ordinal of W
for phi being Ordinal-Sequence of W holds A1 in dom phi
let A1 be Ordinal of W; :: thesis: for phi being Ordinal-Sequence of W holds A1 in dom phi
let phi be Ordinal-Sequence of W; :: thesis: A1 in dom phi
dom phi = On W by FUNCT_2:def 1;
hence A1 in dom phi by ORDINAL1:def 9; :: thesis: verum