let S be non void Signature; 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; (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; verum