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