consider a being object such that
A1: a in S by XBOOLE_0:def 1;
reconsider a = a as FinSequence by A1;
consider b being object such that
A2: b in T by XBOOLE_0:def 1;
reconsider b = b as FinSequence by A2;
a ^ b in S ^ T by A1, A2, Def2;
hence not S ^ T is empty ; :: thesis: verum