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 Def2;
then reconsider TT = the Sorts of (Free S,X) as MSSubset of (FreeMSA (X \/ (the carrier of S --> {0 }))) by MSUALG_2:def 10;

A2: now

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 11;
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, Th18;
then A7: rng p c= Union (S -Terms X,(X \/ (the carrier of S --> {0 }))) by A4, A5, Th20;
A8: rng p c= Union TT

proof

let x be set ; :: 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 set 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:10;
reconsider y = y as SortSymbol of S by A10, PARTFUN1:def 4;
(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, Th17;
( 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 4;
hence x in Union TT by CARD_5:10; :: thesis: verum

end;

TT is opers_closed by A1, MSUALG_2:def 10;
hence [o,the carrier of S] -tree p in the Sorts of (Free S,X) . s by A5, A6, A8, Th21; :: 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 23;

A13: now

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, PBOOLE:def 5;
then A15: the_sort_of t = s by A14, Th8;
A16: the_sort_of t = s1 by MSATERM:14;
then v in X . s by A14, A15, Th19;
hence root-tree [v,s1] in the Sorts of (Free S,X) . s by A15, A16, Th5; :: 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