set I = the carrier of S;
set Y = X \/ (the carrier of S --> {0 });
set R = Reverse (X \/ (the carrier of S --> {0 }));
(Reverse (X \/ (the carrier of S --> {0 }))) "" X is ManySortedSubset of FreeGen (X \/ (the carrier of S --> {0 })) by EQUATION:9;
then A1: (Reverse (X \/ (the carrier of S --> {0 }))) "" X c= FreeGen (X \/ (the carrier of S --> {0 })) by PBOOLE:def 23;
FreeGen (X \/ (the carrier of S --> {0 })) c= the Sorts of (FreeMSA (X \/ (the carrier of S --> {0 }))) by PBOOLE:def 23;
then (Reverse (X \/ (the carrier of S --> {0 }))) "" X c= the Sorts of (FreeMSA (X \/ (the carrier of S --> {0 }))) by A1, PBOOLE:15;
then reconsider Z = (Reverse (X \/ (the carrier of S --> {0 }))) "" X as MSSubset of (FreeMSA (X \/ (the carrier of S --> {0 }))) by PBOOLE:def 23;
take GenMSAlg Z ; :: thesis: ex A being MSSubset of (FreeMSA (X \/ (the carrier of S --> {0 }))) st
( GenMSAlg Z = GenMSAlg A & A = (Reverse (X \/ (the carrier of S --> {0 }))) "" X )
take Z ; :: thesis: ( GenMSAlg Z = GenMSAlg Z & Z = (Reverse (X \/ (the carrier of S --> {0 }))) "" X )
thus ( GenMSAlg Z = GenMSAlg Z & Z = (Reverse (X \/ (the carrier of S --> {0 }))) "" X ) ; :: thesis: verum