let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for s1, s2 being SortSymbol of S
for x1 being Element of X . s1
for x2 being Element of X . s2 holds
( ( s1 <> s2 or x1 <> x2 ) iff x1 -term is x2 -omitting )
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for s1, s2 being SortSymbol of S
for x1 being Element of X . s1
for x2 being Element of X . s2 holds
( ( s1 <> s2 or x1 <> x2 ) iff x1 -term is x2 -omitting )
let s1, s2 be SortSymbol of S; :: thesis: for x1 being Element of X . s1
for x2 being Element of X . s2 holds
( ( s1 <> s2 or x1 <> x2 ) iff x1 -term is x2 -omitting )
let x1 be Element of X . s1; :: thesis: for x2 being Element of X . s2 holds
( ( s1 <> s2 or x1 <> x2 ) iff x1 -term is x2 -omitting )
let x2 be Element of X . s2; :: thesis: ( ( s1 <> s2 or x1 <> x2 ) iff x1 -term is x2 -omitting )

hereby :: thesis: ( not x1 -term is x2 -omitting or s1 <> s2 or x1 <> x2 )

assume ( s1 <> s2 or x1 <> x2 ) ; :: thesis: x1 -term is x2 -omitting
then [x1,s1] <> [x2,s2] by XTUPLE_0:1;
then [x1,s1] nin {[x2,s2]} by TARSKI:def 1;
hence x1 -term is x2 -omitting by FUNCOP_1:16; :: thesis: verum

end;

assume Coim ((x1 -term),[x2,s2]) = {} ; :: according to MSAFREE5:def 21 :: thesis: ( s1 <> s2 or x1 <> x2 )
then [x1,s1] nin {[x2,s2]} by FUNCOP_1:14;
hence ( s1 <> s2 or x1 <> x2 ) by TARSKI:def 1; :: thesis: verum