set p = 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 q = a, r = b as FinSequence by A1, A2;
A5:
( the Element of S ^ q in S ^ T & the Element of S ^ r in S ^ T )
by A1, A2, Def2;
the Element of S ^ q <> the Element of S ^ r
by A3, FINSEQ_1:33;
hence
not S ^ T is trivial
by A5, ZFMISC_1:def 10; verum