let P be FinSequence-membered set ; :: thesis: for p, q being FinSequence st p in P * & q in P * holds
p ^ q in P *
let p, q be FinSequence; :: thesis: ( p in P * & q in P * implies p ^ q in P * )
assume that
A1: p in P * and
A2: q in P * ; :: thesis: p ^ q in P *
consider m being Nat such that
A3: p in P ^^ m by A1, Th5;
consider n being Nat such that
A4: q in P ^^ n by A2, Th5;
p ^ q in P ^^ (m + n) by Th11, A3, A4;
hence p ^ q in P * by Th5; :: thesis: verum