set r = the Element of S;
consider a, b being object such that
A1:
a in T
and
A2:
b in T
and
A3:
a <> b
by ZFMISC_1:def 10;
reconsider p = a, q = b as FinSequence by A1, A2;
A5:
( p ^ the Element of S in T ^ S & q ^ the Element of S in T ^ S )
by A1, A2, Def2;
p ^ the Element of S <> q ^ the Element of S
by A3, FINSEQ_1:33;
hence
not T ^ S is trivial
by A5, ZFMISC_1:def 10; verum