let C be initialized ConstructorSignature; :: thesis: for s1, s2 being SortSymbol of C st s1 <> s2 holds
for t1 being expression of C,s1
for t2 being expression of C,s2 holds t1 <> t2
set X = MSVars C;
set Y = (MSVars C) \/ (the carrier of C --> {0 });
consider A being MSSubset of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) such that
A1: ( Free C,(MSVars C) = GenMSAlg A & A = (Reverse ((MSVars C) \/ (the carrier of C --> {0 }))) "" (MSVars C) ) by MSAFREE3:def 2;
let s1, s2 be SortSymbol of C; :: thesis: ( s1 <> s2 implies for t1 being expression of C,s1
for t2 being expression of C,s2 holds t1 <> t2 )
the Sorts of (Free C,(MSVars C)) is MSSubset of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) by A1, MSUALG_2:def 10;
then the Sorts of (Free C,(MSVars C)) c= the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) by PBOOLE:def 23;
then A2: ( the Sorts of (Free C,(MSVars C)) . s1 c= the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) . s1 & the Sorts of (Free C,(MSVars C)) . s2 c= the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) . s2 ) by PBOOLE:def 5;
assume s1 <> s2 ; :: thesis: for t1 being expression of C,s1
for t2 being expression of C,s2 holds t1 <> t2
then A3: the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) . s1 misses the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) . s2 by PROB_2:def 3;
let t1 be expression of C,s1; :: thesis: for t2 being expression of C,s2 holds t1 <> t2
let t2 be expression of C,s2; :: thesis: t1 <> t2
( t1 in the Sorts of (Free C,(MSVars C)) . s1 & t2 in the Sorts of (Free C,(MSVars C)) . s2 ) by ELEMENT;
hence t1 <> t2 by A2, A3, XBOOLE_0:3; :: thesis: verum