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

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