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});
A1: ex A being MSSubset of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) st
( Free (C,(MSVars C)) = GenMSAlg A & A = (Reverse ((MSVars C) (\/) ( the carrier of C --> {0}))) "" (MSVars C) ) by MSAFREE3:def 1;
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 9;
then A2: the Sorts of (Free (C,(MSVars C))) c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) by PBOOLE:def 18;
then A3: the Sorts of (Free (C,(MSVars C))) . s1 c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . s1 ;
A4: the Sorts of (Free (C,(MSVars C))) . s2 c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . s2 by A2;
assume s1 <> s2 ; :: thesis: for t1 being expression of C,s1
for t2 being expression of C,s2 holds t1 <> t2
then A5: 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 2;
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
A6: t1 in the Sorts of (Free (C,(MSVars C))) . s1 by Def28;
t2 in the Sorts of (Free (C,(MSVars C))) . s2 by Def28;
hence t1 <> t2 by A3, A4, A5, A6, XBOOLE_0:3; :: thesis: verum