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});

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 Th21;

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 9;

A1: ( FreeMSA (X (\/) ( the carrier of S --> {0})) = MSAlgebra(# (FreeSort (X (\/) ( the carrier of S --> {0}))),(FreeOper (X (\/) ( the carrier of S --> {0}))) #) & dom (FreeSort (X (\/) ( the carrier of S --> {0}))) = the carrier of S ) by MSAFREE:def 14, PARTFUN1:def 2;

(Reverse (X (\/) ( the carrier of S --> {0}))) "" X c= S -Terms (X,(X (\/) ( the carrier of S --> {0}))) by Th22;

then A2: (Reverse (X (\/) ( the carrier of S --> {0}))) "" X is MSSubset of B by PBOOLE:def 18;

let s be Element of S; :: according to PBOOLE:def 21 :: thesis: the Sorts of (Free (S,X)) . s = (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s

ex A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) st

( Free (S,X) = GenMSAlg A & A = (Reverse (X (\/) ( the carrier of S --> {0}))) "" X ) by Def1;

then Free (S,X) is MSSubAlgebra of B by A2, MSUALG_2:def 17;

then the Sorts of (Free (S,X)) is MSSubset of B by MSUALG_2:def 9;

then the Sorts of (Free (S,X)) c= S -Terms (X,(X (\/) ( the carrier of S --> {0}))) by PBOOLE:def 18;

hence the Sorts of (Free (S,X)) . s c= (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s ; :: according to XBOOLE_0:def 10 :: thesis: (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s c= the Sorts of (Free (S,X)) . s

let x be object ; :: 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 A3: x in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s ; :: thesis: x in 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 18;

then (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s c= the Sorts of (FreeMSA (X (\/) ( the carrier of S --> {0}))) . s ;

then x in Union (FreeSort (X (\/) ( the carrier of S --> {0}))) by A3, A1, CARD_5:2;

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 A3, Th23; :: thesis: verum

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});

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 Th21;

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 9;

A1: ( FreeMSA (X (\/) ( the carrier of S --> {0})) = MSAlgebra(# (FreeSort (X (\/) ( the carrier of S --> {0}))),(FreeOper (X (\/) ( the carrier of S --> {0}))) #) & dom (FreeSort (X (\/) ( the carrier of S --> {0}))) = the carrier of S ) by MSAFREE:def 14, PARTFUN1:def 2;

(Reverse (X (\/) ( the carrier of S --> {0}))) "" X c= S -Terms (X,(X (\/) ( the carrier of S --> {0}))) by Th22;

then A2: (Reverse (X (\/) ( the carrier of S --> {0}))) "" X is MSSubset of B by PBOOLE:def 18;

let s be Element of S; :: according to PBOOLE:def 21 :: thesis: the Sorts of (Free (S,X)) . s = (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s

ex A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) st

( Free (S,X) = GenMSAlg A & A = (Reverse (X (\/) ( the carrier of S --> {0}))) "" X ) by Def1;

then Free (S,X) is MSSubAlgebra of B by A2, MSUALG_2:def 17;

then the Sorts of (Free (S,X)) is MSSubset of B by MSUALG_2:def 9;

then the Sorts of (Free (S,X)) c= S -Terms (X,(X (\/) ( the carrier of S --> {0}))) by PBOOLE:def 18;

hence the Sorts of (Free (S,X)) . s c= (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s ; :: according to XBOOLE_0:def 10 :: thesis: (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s c= the Sorts of (Free (S,X)) . s

let x be object ; :: 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 A3: x in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s ; :: thesis: x in 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 18;

then (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s c= the Sorts of (FreeMSA (X (\/) ( the carrier of S --> {0}))) . s ;

then x in Union (FreeSort (X (\/) ( the carrier of S --> {0}))) by A3, A1, CARD_5:2;

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 A3, Th23; :: thesis: verum