let S be non void Signature; :: thesis: for X being V8() ManySortedSet of the carrier of S holds Free (S,X) = FreeMSA X

let X be V8() ManySortedSet of the carrier of S; :: thesis: Free (S,X) = FreeMSA X

set Y = X (\/) ( the carrier of S --> {0});

A1: the Sorts of (Free (S,X)) = S -Terms (X,(X (\/) ( the carrier of S --> {0}))) by Th24;

A2: FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def 14;

A3: the Sorts of (Free (S,X)) = the Sorts of (FreeMSA X)

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

hence Free (S,X) = FreeMSA X by A3, Th26; :: thesis: verum

let X be V8() ManySortedSet of the carrier of S; :: thesis: Free (S,X) = FreeMSA X

set Y = X (\/) ( the carrier of S --> {0});

A1: the Sorts of (Free (S,X)) = S -Terms (X,(X (\/) ( the carrier of S --> {0}))) by Th24;

A2: FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def 14;

A3: the Sorts of (Free (S,X)) = the Sorts of (FreeMSA X)

proof

( FreeMSA X is MSSubAlgebra of FreeMSA X & ex A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) st
let s be Element of S; :: according to PBOOLE:def 21 :: thesis: the Sorts of (Free (S,X)) . s = the Sorts of (FreeMSA X) . s

reconsider s9 = s as SortSymbol of S ;

thus the Sorts of (Free (S,X)) . s c= the Sorts of (FreeMSA X) . s :: according to XBOOLE_0:def 10 :: thesis: the Sorts of (FreeMSA X) . s c= the Sorts of (Free (S,X)) . s

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the Sorts of (FreeMSA X) . s or x in the Sorts of (Free (S,X)) . s )

assume x in the Sorts of (FreeMSA X) . s ; :: thesis: x in the Sorts of (Free (S,X)) . s

then A5: x in FreeSort (X,s9) by A2, MSAFREE:def 11;

FreeSort (X,s9) c= S -Terms X by MSATERM:12;

then reconsider t = x as Term of S,X by A5;

X c= X (\/) ( the carrier of S --> {0}) by PBOOLE:14;

then reconsider t9 = t as Term of S,(X (\/) ( the carrier of S --> {0})) by MSATERM:26;

variables_in t = S variables_in t ;

then A6: variables_in t9 c= X by Th28;

the_sort_of t = s by A5, MSATERM:def 5;

then the_sort_of t9 = s by Th29;

then t in { q where q is Term of S,(X (\/) ( the carrier of S --> {0})) : ( the_sort_of q = s9 & variables_in q c= X ) } by A6;

hence x in the Sorts of (Free (S,X)) . s by A1, Def5; :: thesis: verum

end;reconsider s9 = s as SortSymbol of S ;

thus the Sorts of (Free (S,X)) . s c= the Sorts of (FreeMSA X) . s :: according to XBOOLE_0:def 10 :: thesis: the Sorts of (FreeMSA X) . s c= the Sorts of (Free (S,X)) . s

proof

reconsider s9 = s as SortSymbol of S ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the Sorts of (Free (S,X)) . s or x in the Sorts of (FreeMSA X) . s )

assume A4: x in the Sorts of (Free (S,X)) . s ; :: thesis: x in the Sorts of (FreeMSA X) . s

then reconsider t = x as Term of S,(X (\/) ( the carrier of S --> {0})) by A1, Th16;

variables_in t c= X by A1, A4, Th17;

then reconsider t9 = t as Term of S,X by Th30;

the_sort_of t = s by A1, A4, Th17;

then the_sort_of t9 = s by Th29;

then x in FreeSort (X,s9) by MSATERM:def 5;

hence x in the Sorts of (FreeMSA X) . s by A2, MSAFREE:def 11; :: thesis: verum

end;assume A4: x in the Sorts of (Free (S,X)) . s ; :: thesis: x in the Sorts of (FreeMSA X) . s

then reconsider t = x as Term of S,(X (\/) ( the carrier of S --> {0})) by A1, Th16;

variables_in t c= X by A1, A4, Th17;

then reconsider t9 = t as Term of S,X by Th30;

the_sort_of t = s by A1, A4, Th17;

then the_sort_of t9 = s by Th29;

then x in FreeSort (X,s9) by MSATERM:def 5;

hence x in the Sorts of (FreeMSA X) . s by A2, MSAFREE:def 11; :: thesis: verum

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the Sorts of (FreeMSA X) . s or x in the Sorts of (Free (S,X)) . s )

assume x in the Sorts of (FreeMSA X) . s ; :: thesis: x in the Sorts of (Free (S,X)) . s

then A5: x in FreeSort (X,s9) by A2, MSAFREE:def 11;

FreeSort (X,s9) c= S -Terms X by MSATERM:12;

then reconsider t = x as Term of S,X by A5;

X c= X (\/) ( the carrier of S --> {0}) by PBOOLE:14;

then reconsider t9 = t as Term of S,(X (\/) ( the carrier of S --> {0})) by MSATERM:26;

variables_in t = S variables_in t ;

then A6: variables_in t9 c= X by Th28;

the_sort_of t = s by A5, MSATERM:def 5;

then the_sort_of t9 = s by Th29;

then t in { q where q is Term of S,(X (\/) ( the carrier of S --> {0})) : ( the_sort_of q = s9 & variables_in q c= X ) } by A6;

hence x in the Sorts of (Free (S,X)) . s by A1, Def5; :: thesis: verum

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

hence Free (S,X) = FreeMSA X by A3, Th26; :: thesis: verum