let S be non void Signature; :: thesis: for X being V8() ManySortedSet of the carrier of S
for t being Term of S,X holds not t is pair
let X be V8() ManySortedSet of the carrier of S; :: thesis: for t being Term of S,X holds not t is pair
let t be Term of S,X; :: thesis: not t is pair
given x, y being object such that A1: t = [x,y] ; :: according to XTUPLE_0:def 1 :: thesis: contradiction
( ex s being SortSymbol of S ex v being Element of X . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] ) by MSATERM:2;
then ( ex s being SortSymbol of S ex v being Element of X . s st t . {} = [v,s] or ex a, b being object st
( a in the carrier' of S & b in { the carrier of S} & t . {} = [a,b] ) ) by ZFMISC_1:def 2;
then {{}} <> {{},(t . {})} by ZFMISC_1:5;
then A2: [{},(t . {})] <> {x} by ZFMISC_1:5;
{} in dom t by TREES_1:22;
then [{},(t . {})] in t by FUNCT_1:def 2;
then A3: [{},(t . {})] = {x,y} by A1, A2, TARSKI:def 2;
x = y by A1, Th3;
hence contradiction by A2, A3, ENUMSET1:29; :: thesis: verum