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 Def2, Th22, MSUALG_2:def 16;
hence (FreeMSA (X \/ (the carrier of S --> {0 }))) | (S -Terms X,(X \/ (the carrier of S --> {0 }))) = Free S,X by Th25, MSUALG_2:10; :: thesis: verum