let D be set ; :: thesis: for p, q being D -valued FinSequence holds p ^ q is FinSequence of D
let p, q be D -valued FinSequence; :: thesis: p ^ q is FinSequence of D
reconsider p = p, q = q as FinSequence of D by LL;
p ^ q is FinSequence of D ;
hence p ^ q is FinSequence of D ; :: thesis: verum