let S be non void Signature; :: thesis: for X being V6() ManySortedSet of the carrier of S
for x being Element of (Free S,X) holds x is Term of S,(X \/ (the carrier of S --> {0 }))
let X be V6() ManySortedSet of the carrier of S; :: thesis: for x being Element of (Free S,X) holds x is Term of S,(X \/ (the carrier of S --> {0 }))
set Y = X \/ (the carrier of S --> {0 });
let x be Element of (Free S,X); :: thesis: x is Term of S,(X \/ (the carrier of S --> {0 }))
A1: S -Terms (X \/ (the carrier of S --> {0 })) = TS (DTConMSA (X \/ (the carrier of S --> {0 }))) by MSATERM:def 1
.= union (rng (FreeSort (X \/ (the carrier of S --> {0 })))) by MSAFREE:12
.= Union (FreeSort (X \/ (the carrier of S --> {0 }))) by CARD_3:def 4 ;
A2: dom the Sorts of (Free S,X) = the carrier of S by PARTFUN1:def 4;
A3: ( FreeMSA (X \/ (the carrier of S --> {0 })) = MSAlgebra(# (FreeSort (X \/ (the carrier of S --> {0 }))),(FreeOper (X \/ (the carrier of S --> {0 }))) #) & dom the Sorts of (FreeMSA (X \/ (the carrier of S --> {0 }))) = the carrier of S ) by MSAFREE:def 16, PARTFUN1:def 4;
consider y being set such that
A4: y in dom the Sorts of (Free S,X) and
A5: x in the Sorts of (Free S,X) . y by CARD_5:10;
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;
then the Sorts of (Free S,X) is MSSubset of (FreeMSA (X \/ (the carrier of S --> {0 }))) by MSUALG_2:def 10;
then the Sorts of (Free S,X) c= the Sorts of (FreeMSA (X \/ (the carrier of S --> {0 }))) by PBOOLE:def 23;
then the Sorts of (Free S,X) . y c= the Sorts of (FreeMSA (X \/ (the carrier of S --> {0 }))) . y by A4, A2, PBOOLE:def 5;
hence x is Term of S,(X \/ (the carrier of S --> {0 })) by A1, A4, A5, A2, A3, CARD_5:10; :: thesis: verum