let x be object ; :: according to FINSEQ_1:def 19 :: thesis: ( x in X \/ Y implies x is FinSequence )
assume x in X \/ Y ; :: thesis: x is FinSequence
then ( x in X or x in Y ) by XBOOLE_0:def 3;
hence x is FinSequence by Def18; :: thesis: verum