let X be set ; :: thesis: for psi being Ordinal-Sequence holds Union (X | psi) is Ordinal
let psi be Ordinal-Sequence; :: thesis: Union (X | psi) is Ordinal
consider A being Ordinal such that
A1: rng psi c= A by ORDINAL2:def 8;
A2: rng (X | psi) c= rng psi by RELAT_1:118;

A3: now

let x be set ; :: thesis: ( x in rng (X | psi) implies x is Ordinal )
assume x in rng (X | psi) ; :: thesis: x is Ordinal
then x in A by A1, A2, TARSKI:def 3;
hence x is Ordinal ; :: thesis: verum

end;

Union (X | psi) = union (rng (X | psi)) by CARD_3:def 4;
hence Union (X | psi) is Ordinal by A3, ORDINAL1:35; :: thesis: verum