let S be non empty non void ManySortedSign ; :: thesis: for X being V5() 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 V5() 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 )
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