let S be non void Signature; :: thesis: for X being ManySortedSet of 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 ; :: 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 });
A1: (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 })))) #) by Th22, MSUALG_2:def 16;
consider A being MSSubset of (FreeMSA (X \/ (the carrier of S --> {0 }))) such that
A2: ( Free S,X = GenMSAlg A & A = (Reverse (X \/ (the carrier of S --> {0 }))) "" X ) by Def2;
thus (FreeMSA (X \/ (the carrier of S --> {0 }))) | (S -Terms X,(X \/ (the carrier of S --> {0 }))) = Free S,X by A1, A2, Th25, MSUALG_2:10; :: thesis: verum