:: deftheorem Def3 defines ^ AFINSQ_1:def 3 :
for p, q being XFinSequence
for b₃ being set holds
( b₃ = p ^ q iff ( dom b₃ = (len p) + (len q) & ( for k being Nat st k in dom p holds
b₃ . k = p . k ) & ( for k being Nat st k in dom q holds
b₃ . ((len p) + k) = q . k ) ) );