let S be non void Signature; :: thesis: for X being ManySortedSet of the carrier of S holds the Sorts of (Free S,X) = S -Terms X,(X \/ (the carrier of S --> {0 }))
let X be ManySortedSet of the carrier of S; :: thesis: the Sorts of (Free S,X) = S -Terms X,(X \/ (the carrier of S --> {0 }))
set Y = X \/ (the carrier of S --> {0 });
consider A being MSSubset of (FreeMSA (X \/ (the carrier of S --> {0 }))) such that
A1: ( Free S,X = GenMSAlg A & A = (Reverse (X \/ (the carrier of S --> {0 }))) "" X ) by Def2;
set B = MSAlgebra(# (S -Terms X,(X \/ (the carrier of S --> {0 }))),(Opers (FreeMSA (X \/ (the carrier of S --> {0 }))),(S -Terms X,(X \/ (the carrier of S --> {0 })))) #);
for Z being MSSubset of (FreeMSA (X \/ (the carrier of S --> {0 }))) st Z = the Sorts of MSAlgebra(# (S -Terms X,(X \/ (the carrier of S --> {0 }))),(Opers (FreeMSA (X \/ (the carrier of S --> {0 }))),(S -Terms X,(X \/ (the carrier of S --> {0 })))) #) holds
( Z is opers_closed & the Charact of MSAlgebra(# (S -Terms X,(X \/ (the carrier of S --> {0 }))),(Opers (FreeMSA (X \/ (the carrier of S --> {0 }))),(S -Terms X,(X \/ (the carrier of S --> {0 })))) #) = Opers (FreeMSA (X \/ (the carrier of S --> {0 }))),Z ) by Th22;
then reconsider B = MSAlgebra(# (S -Terms X,(X \/ (the carrier of S --> {0 }))),(Opers (FreeMSA (X \/ (the carrier of S --> {0 }))),(S -Terms X,(X \/ (the carrier of S --> {0 })))) #) as MSSubAlgebra of FreeMSA (X \/ (the carrier of S --> {0 })) by MSUALG_2:def 10;
(Reverse (X \/ (the carrier of S --> {0 }))) "" X c= S -Terms X,(X \/ (the carrier of S --> {0 })) by Th23;
then (Reverse (X \/ (the carrier of S --> {0 }))) "" X is MSSubset of B by PBOOLE:def 23;
then Free S,X is MSSubAlgebra of B by A1, MSUALG_2:def 18;
then the Sorts of (Free S,X) is MSSubset of B by MSUALG_2:def 10;
hence the Sorts of (Free S,X) c= S -Terms X,(X \/ (the carrier of S --> {0 })) by PBOOLE:def 23; :: according to PBOOLE:def 13 :: thesis: S -Terms X,(X \/ (the carrier of S --> {0 })) c= the Sorts of (Free S,X)
let s be set ; :: according to PBOOLE:def 5 :: thesis: ( not s in the carrier of S or (S -Terms X,(X \/ (the carrier of S --> {0 }))) . s c= the Sorts of (Free S,X) . s )
assume A2: s in the carrier of S ; :: thesis: (S -Terms X,(X \/ (the carrier of S --> {0 }))) . s c= the Sorts of (Free S,X) . s
S -Terms X,(X \/ (the carrier of S --> {0 })) c= the Sorts of (FreeMSA (X \/ (the carrier of S --> {0 }))) by PBOOLE:def 23;
then A3: (S -Terms X,(X \/ (the carrier of S --> {0 }))) . s c= the Sorts of (FreeMSA (X \/ (the carrier of S --> {0 }))) . s by A2, PBOOLE:def 5;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (S -Terms X,(X \/ (the carrier of S --> {0 }))) . s or x in the Sorts of (Free S,X) . s )
assume A4: x in (S -Terms X,(X \/ (the carrier of S --> {0 }))) . s ; :: thesis: x in the Sorts of (Free S,X) . s
FreeMSA (X \/ (the carrier of S --> {0 })) = MSAlgebra(# (FreeSort (X \/ (the carrier of S --> {0 }))),(FreeOper (X \/ (the carrier of S --> {0 }))) #) by MSAFREE:def 16;
then ( x in (FreeSort (X \/ (the carrier of S --> {0 }))) . s & dom (FreeSort (X \/ (the carrier of S --> {0 }))) = the carrier of S ) by A3, A4, PBOOLE:def 3;
then x in Union (FreeSort (X \/ (the carrier of S --> {0 }))) by A2, CARD_5:10;
then x is Term of S,(X \/ (the carrier of S --> {0 })) by MSATERM:13;
hence x in the Sorts of (Free S,X) . s by A2, A4, Th24; :: thesis: verum