let S be non void Signature; 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; 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)); 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; verum