let S be non void Signature; :: thesis: for X being ManySortedSet of the carrier of S holds (FreeMSA (X (\/) ( the carrier of S --> {0}))) | (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) = Free (S,X)

let X be ManySortedSet of the carrier of S; :: thesis: (FreeMSA (X (\/) ( the carrier of S --> {0}))) | (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) = Free (S,X)

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

( (FreeMSA (X (\/) ( the carrier of S --> {0}))) | (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) = 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})))))) #) & 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, Th21, MSUALG_2:def 15;

hence (FreeMSA (X (\/) ( the carrier of S --> {0}))) | (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) = Free (S,X) by Th24, MSUALG_2:9; :: thesis: verum

let X be ManySortedSet of the carrier of S; :: thesis: (FreeMSA (X (\/) ( the carrier of S --> {0}))) | (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) = Free (S,X)

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

( (FreeMSA (X (\/) ( the carrier of S --> {0}))) | (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) = 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})))))) #) & 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, Th21, MSUALG_2:def 15;

hence (FreeMSA (X (\/) ( the carrier of S --> {0}))) | (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) = Free (S,X) by Th24, MSUALG_2:9; :: thesis: verum