let S be non empty non void ManySortedSign ; :: thesis: for X being ManySortedSet of the carrier of S
for t being Term of S,(X (\/) ( the carrier of S --> {0}))
for s being SortSymbol of S st t in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s holds
t in the Sorts of (Free (S,X)) . s
let X be ManySortedSet of the carrier of S; :: thesis: for t being Term of S,(X (\/) ( the carrier of S --> {0}))
for s being SortSymbol of S st t in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s holds
t in the Sorts of (Free (S,X)) . s
set Y = X (\/) ( the carrier of S --> {0});
set T = the Sorts of (Free (S,X));
defpred S₁[ set ] means for s being SortSymbol of S st $1 in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s holds
$1 in the Sorts of (Free (S,X)) . s;
A1: 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 reconsider TT = the Sorts of (Free (S,X)) as MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) by MSUALG_2:def 9;

A2: now :: thesis: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0}))) st ( for t being Term of S,(X (\/) ( the carrier of S --> {0})) st t in rng p holds
S₁[t] ) holds
S₁[[o, the carrier of S] -tree p]

let o be OperSymbol of S; :: thesis: for p being ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0}))) st ( for t being Term of S,(X (\/) ( the carrier of S --> {0})) st t in rng p holds
S₁[t] ) holds
S₁[[o, the carrier of S] -tree p]
let p be ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0}))); :: thesis: ( ( for t being Term of S,(X (\/) ( the carrier of S --> {0})) st t in rng p holds
S₁[t] ) implies S₁[[o, the carrier of S] -tree p] )
assume A3: for t being Term of S,(X (\/) ( the carrier of S --> {0})) st t in rng p holds
S₁[t] ; :: thesis: S₁[[o, the carrier of S] -tree p]
thus S₁[[o, the carrier of S] -tree p] :: thesis: verum

proof

let s be SortSymbol of S; :: thesis: ( [o, the carrier of S] -tree p in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s implies [o, the carrier of S] -tree p in the Sorts of (Free (S,X)) . s )
assume A4: [o, the carrier of S] -tree p in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s ; :: thesis: [o, the carrier of S] -tree p in the Sorts of (Free (S,X)) . s
A5: Sym (o,(X (\/) ( the carrier of S --> {0}))) = [o, the carrier of S] by MSAFREE:def 9;
the_sort_of ((Sym (o,(X (\/) ( the carrier of S --> {0})))) -tree p) = the_result_sort_of o by MSATERM:20;
then A6: s = the_result_sort_of o by A4, A5, Th17;
then A7: rng p c= Union (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) by A4, A5, Th19;
A8: rng p c= Union TT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in Union TT )
assume A9: x in rng p ; :: thesis: x in Union TT
then consider y being object such that
A10: y in dom (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) and
A11: x in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . y by A7, CARD_5:2;
reconsider y = y as SortSymbol of S by A10;
(S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . y = (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . y ;
then reconsider x = x as Term of S,(X (\/) ( the carrier of S --> {0})) by A11, Th16;
( dom the Sorts of (Free (S,X)) = the carrier of S & x in the Sorts of (Free (S,X)) . y ) by A3, A9, A11, PARTFUN1:def 2;
hence x in Union TT by CARD_5:2; :: thesis: verum

end;

TT is opers_closed by A1, MSUALG_2:def 9;
hence [o, the carrier of S] -tree p in the Sorts of (Free (S,X)) . s by A5, A6, A8, Th20; :: thesis: verum

end;

end;

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

A13: now :: thesis: for s1 being SortSymbol of S
for v being Element of (X (\/) ( the carrier of S --> {0})) . s1 holds S₁[ root-tree [v,s1]]

let s1 be SortSymbol of S; :: thesis: for v being Element of (X (\/) ( the carrier of S --> {0})) . s1 holds S₁[ root-tree [v,s1]]
let v be Element of (X (\/) ( the carrier of S --> {0})) . s1; :: thesis: S₁[ root-tree [v,s1]]
thus S₁[ root-tree [v,s1]] :: thesis: verum

proof

reconsider t = root-tree [v,s1] as Term of S,(X (\/) ( the carrier of S --> {0})) by MSATERM:4;
let s be SortSymbol of S; :: thesis: ( root-tree [v,s1] in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s implies root-tree [v,s1] in the Sorts of (Free (S,X)) . s )
assume A14: root-tree [v,s1] in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s ; :: thesis: root-tree [v,s1] in the Sorts of (Free (S,X)) . s
(S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s c= the Sorts of (FreeMSA (X (\/) ( the carrier of S --> {0}))) . s by A12;
then A15: the_sort_of t = s by A14, Th7;
A16: the_sort_of t = s1 by MSATERM:14;
then v in X . s by A14, A15, Th18;
hence root-tree [v,s1] in the Sorts of (Free (S,X)) . s by A15, A16, Th4; :: thesis: verum

end;

end;

thus for t being Term of S,(X (\/) ( the carrier of S --> {0})) holds S₁[t] from MSATERM:sch 1(A13, A2); :: thesis: verum