let S be non void Signature; :: thesis: for X being V9() 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 V9() 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:11

.= Union (FreeSort (X (\/) ( the carrier of S --> {0}))) by CARD_3:def 4 ;

A2: ( 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 14, PARTFUN1:def 2;

consider y being object such that

A3: y in dom the Sorts of (Free (S,X)) and

A4: x in the Sorts of (Free (S,X)) . y by CARD_5:2;

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;

then the Sorts of (Free (S,X)) is MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) by MSUALG_2:def 9;

then the Sorts of (Free (S,X)) c= the Sorts of (FreeMSA (X (\/) ( the carrier of S --> {0}))) by PBOOLE:def 18;

then the Sorts of (Free (S,X)) . y c= the Sorts of (FreeMSA (X (\/) ( the carrier of S --> {0}))) . y by A3;

hence x is Term of S,(X (\/) ( the carrier of S --> {0})) by A1, A3, A4, A2, CARD_5:2; :: thesis: verum

for x being Element of (Free (S,X)) holds x is Term of S,(X (\/) ( the carrier of S --> {0}))

let X be V9() 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:11

.= Union (FreeSort (X (\/) ( the carrier of S --> {0}))) by CARD_3:def 4 ;

A2: ( 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 14, PARTFUN1:def 2;

consider y being object such that

A3: y in dom the Sorts of (Free (S,X)) and

A4: x in the Sorts of (Free (S,X)) . y by CARD_5:2;

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;

then the Sorts of (Free (S,X)) is MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) by MSUALG_2:def 9;

then the Sorts of (Free (S,X)) c= the Sorts of (FreeMSA (X (\/) ( the carrier of S --> {0}))) by PBOOLE:def 18;

then the Sorts of (Free (S,X)) . y c= the Sorts of (FreeMSA (X (\/) ( the carrier of S --> {0}))) . y by A3;

hence x is Term of S,(X (\/) ( the carrier of S --> {0})) by A1, A3, A4, A2, CARD_5:2; :: thesis: verum