let S be non void Signature; :: thesis: for X being V5() ManySortedSet of
for t being Term of S,X holds not t is pair
let X be V5() ManySortedSet of ; :: 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 set such that A1: t = [x,y] ; :: according to FACIRC_1: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 set 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:9;
then A4: [{} ,(t . {} )] <> {x} by ZFMISC_1:9;
{} in dom t by TREES_1:47;
then [{} ,(t . {} )] in t by FUNCT_1:def 4;
then ( [{} ,(t . {} )] = {x,y} & x = y ) by A1, A4, Th89, TARSKI:def 2;
hence contradiction by A4, ENUMSET1:69; :: thesis: verum