consider k1 being Nat such that
A1: A c= Seg k1 by DI;
consider k2 being Nat such that
A2: B c= Seg k2 by DI;
take k1 + k2 ; :: according to FINSEQ_1:def 13 :: thesis: A \/ B c= Seg (k1 + k2)
A3: A \/ B c= (Seg k1) \/ (Seg k2) by A1, A2, XBOOLE_1:13;
( k1 <= k1 + k2 & k2 <= k1 + k2 ) by NAT_1:11;
then ( Seg k1 c= Seg (k1 + k2) & Seg k2 c= Seg (k1 + k2) ) by Th5;
then (Seg k1) \/ (Seg k2) c= Seg (k1 + k2) by XBOOLE_1:8;
hence A \/ B c= Seg (k1 + k2) by A3; :: thesis: verum