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