let L be Sequence; :: thesis: for A being Ordinal holds L | (Rank A) is Sequence
let A be Ordinal; :: thesis: L | (Rank A) is Sequence
A1: dom (L | (Rank A)) = (dom L) /\ (Rank A) by RELAT_1:61;
now :: thesis: for X being set st X in dom (L | (Rank A)) holds
( X is Ordinal & X c= dom (L | (Rank A)) )
let X be set ; :: thesis: ( X in dom (L | (Rank A)) implies ( X is Ordinal & X c= dom (L | (Rank A)) ) )
assume A2: X in dom (L | (Rank A)) ; :: thesis: ( X is Ordinal & X c= dom (L | (Rank A)) )
then A3: X in dom L by A1, XBOOLE_0:def 4;
hence X is Ordinal ; :: thesis: X c= dom (L | (Rank A))
X in Rank A by A1, A2, XBOOLE_0:def 4;
then A4: X c= Rank A by ORDINAL1:def 2;
X c= dom L by A3, ORDINAL1:def 2;
hence X c= dom (L | (Rank A)) by A1, A4, XBOOLE_1:19; :: thesis: verum
end;
then dom (L | (Rank A)) is epsilon-transitive epsilon-connected set by ORDINAL1:19;
hence L | (Rank A) is Sequence by ORDINAL1:31; :: thesis: verum