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