s1 ^ s2 is FinSequence of A ;
hence s1 ^ s2 is Element of A * by FINSEQ_1:def 11; :: thesis: verum