let P be FinSequence-membered set ; :: thesis: for p, q being FinSequence
for m, n being Nat st p in P ^^ m & q in P ^^ n holds
p ^ q in P ^^ (m + n)
let p, q be FinSequence; :: thesis: for m, n being Nat st p in P ^^ m & q in P ^^ n holds
p ^ q in P ^^ (m + n)
let m, n be Nat; :: thesis: ( p in P ^^ m & q in P ^^ n implies p ^ q in P ^^ (m + n) )
assume ( p in P ^^ m & q in P ^^ n ) ; :: thesis: p ^ q in P ^^ (m + n)
then p ^ q in (P ^^ m) ^ (P ^^ n) by Def2;
hence p ^ q in P ^^ (m + n) by Th10; :: thesis: verum