let p, q be FinSequence; :: thesis: dom p c= dom (p ^ q)
len p <= (len p) + (len q) by NAT_1:11;
then Seg (len p) c= Seg ((len p) + (len q)) by Th7;
then Seg (len p) c= dom (p ^ q) by Def7;
hence dom p c= dom (p ^ q) by Def3; :: thesis: verum