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 --> ))
for s being SortSymbol of S st t in (S -Terms (X,(X (\/) ( the carrier of S --> )))) . 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 --> ))
for s being SortSymbol of S st t in (S -Terms (X,(X (\/) ( the carrier of S --> )))) . s holds
t in the Sorts of (Free (S,X)) . s

set Y = X (\/) ( the carrier of S --> );
set T = the Sorts of (Free (S,X));
defpred S1[ set ] means for s being SortSymbol of S st \$1 in (S -Terms (X,(X (\/) ( the carrier of S --> )))) . s holds
\$1 in the Sorts of (Free (S,X)) . s;
A1: ex A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> ))) st
( Free (S,X) = GenMSAlg A & A = (Reverse (X (\/) ( the carrier of S --> ))) "" X ) by Def1;
then reconsider TT = the Sorts of (Free (S,X)) as MSSubset of (FreeMSA (X (\/) ( the carrier of S --> ))) 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 --> ))) st ( for t being Term of S,(X (\/) ( the carrier of S --> )) st t in rng p holds
S1[t] ) holds
S1[[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 --> ))) st ( for t being Term of S,(X (\/) ( the carrier of S --> )) st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]

let p be ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> ))); :: thesis: ( ( for t being Term of S,(X (\/) ( the carrier of S --> )) st t in rng p holds
S1[t] ) implies S1[[o, the carrier of S] -tree p] )

assume A3: for t being Term of S,(X (\/) ( the carrier of S --> )) st t in rng p holds
S1[t] ; :: thesis: S1[[o, the carrier of S] -tree p]
thus S1[[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 --> )))) . 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 --> )))) . 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 --> ))) = [o, the carrier of S] by MSAFREE:def 9;
the_sort_of ((Sym (o,(X (\/) ( the carrier of S --> )))) -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 --> )))) 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 --> )))) and
A11: x in (S -Terms (X,(X (\/) ( the carrier of S --> )))) . y by ;
reconsider y = y as SortSymbol of S by A10;
(S -Terms (X,(X (\/) ( the carrier of S --> )))) . y = (S -Terms (X,(X (\/) ( the carrier of S --> )))) . y ;
then reconsider x = x as Term of S,(X (\/) ( the carrier of S --> )) by ;
( dom the Sorts of (Free (S,X)) = the carrier of S & x in the Sorts of (Free (S,X)) . y ) by ;
hence x in Union TT by CARD_5:2; :: thesis: verum
end;
TT is opers_closed by ;
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 --> ))) c= the Sorts of (FreeMSA (X (\/) ( the carrier of S --> ))) by PBOOLE:def 18;
A13: now :: thesis: for s1 being SortSymbol of S
for v being Element of (X (\/) ( the carrier of S --> )) . s1 holds S1[ root-tree [v,s1]]
let s1 be SortSymbol of S; :: thesis: for v being Element of (X (\/) ( the carrier of S --> )) . s1 holds S1[ root-tree [v,s1]]
let v be Element of (X (\/) ( the carrier of S --> )) . s1; :: thesis: S1[ root-tree [v,s1]]
thus S1[ root-tree [v,s1]] :: thesis: verum
proof
reconsider t = root-tree [v,s1] as Term of S,(X (\/) ( the carrier of S --> )) by MSATERM:4;
let s be SortSymbol of S; :: thesis: ( root-tree [v,s1] in (S -Terms (X,(X (\/) ( the carrier of S --> )))) . 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 --> )))) . s ; :: thesis: root-tree [v,s1] in the Sorts of (Free (S,X)) . s
(S -Terms (X,(X (\/) ( the carrier of S --> )))) . s c= the Sorts of (FreeMSA (X (\/) ( the carrier of S --> ))) . s by A12;
then A15: the_sort_of t = s by ;
A16: the_sort_of t = s1 by MSATERM:14;
then v in X . s by ;
hence root-tree [v,s1] in the Sorts of (Free (S,X)) . s by ; :: thesis: verum
end;
end;
thus for t being Term of S,(X (\/) ( the carrier of S --> )) holds S1[t] from :: thesis: verum