let S be non void Signature; :: thesis: for X being V6() ManySortedSet of the carrier of S
for t being Element of (Free S,X) holds
( ex s being SortSymbol of S ex v being set st
( t = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free S,X) st
( t = [o,the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym o,(X \/ (the carrier of S --> {0 })) ) )
let X be V6() ManySortedSet of the carrier of S; :: thesis: for t being Element of (Free S,X) holds
( ex s being SortSymbol of S ex v being set st
( t = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free S,X) st
( t = [o,the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym o,(X \/ (the carrier of S --> {0 })) ) )
let t be Element of (Free S,X); :: thesis: ( ex s being SortSymbol of S ex v being set st
( t = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free S,X) st
( t = [o,the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym o,(X \/ (the carrier of S --> {0 })) ) )
set V = X \/ (the carrier of S --> {0 });
reconsider t9 = t as Term of S,(X \/ (the carrier of S --> {0 })) by MSAFREE3:9;
defpred S₁[ set ] means ( not $1 is Element of (Free S,X) or ex s being SortSymbol of S ex v being set st
( $1 = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free S,X) st
( $1 = [o,the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym o,(X \/ (the carrier of S --> {0 })) ) );
A1: for s being SortSymbol of S
for v being Element of (X \/ (the carrier of S --> {0 })) . s holds S₁[ root-tree [v,s]]

proof

let s be SortSymbol of S; :: thesis: for v being Element of (X \/ (the carrier of S --> {0 })) . s holds S₁[ root-tree [v,s]]
let v be Element of (X \/ (the carrier of S --> {0 })) . s; :: thesis: S₁[ root-tree [v,s]]
set t = root-tree [v,s];
assume A2: root-tree [v,s] is Element of (Free S,X) ; :: thesis: ( ex s being SortSymbol of S ex v being set st
( root-tree [v,s] = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free S,X) st
( root-tree [v,s] = [o,the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym o,(X \/ (the carrier of S --> {0 })) ) )
{} in dom (root-tree [v,s]) by TREES_1:47;
then (root-tree [v,s]) . {} in rng (root-tree [v,s]) by FUNCT_1:12;
then [v,s] in rng (root-tree [v,s]) by TREES_4:3;
then v in X . s by A2, MSAFREE3:36;
hence ( ex s being SortSymbol of S ex v being set st
( root-tree [v,s] = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free S,X) st
( root-tree [v,s] = [o,the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym o,(X \/ (the carrier of S --> {0 })) ) ) ; :: thesis: verum

end;

A3: 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]

proof

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 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]
set t = [o,the carrier of S] -tree p;
assume [o,the carrier of S] -tree p is Element of (Free S,X) ; :: thesis: ( ex s being SortSymbol of S ex v being set st
( [o,the carrier of S] -tree p = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free S,X) st
( [o,the carrier of S] -tree p = [o,the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym o,(X \/ (the carrier of S --> {0 })) ) )
then consider s being set such that
A4: s in dom the Sorts of (Free S,X) and
A5: [o,the carrier of S] -tree p in the Sorts of (Free S,X) . s by CARD_5:10;
reconsider s = s as Element of S by A4, PARTFUN1:def 4;
A6: the Sorts of (Free S,X) = S -Terms X,(X \/ (the carrier of S --> {0 })) by MSAFREE3:25;
the_sort_of ((Sym o,(X \/ (the carrier of S --> {0 }))) -tree p) = the_result_sort_of o by MSATERM:20;
then s = the_result_sort_of o by A5, A6, MSAFREE3:18;
then rng p c= Union (S -Terms X,(X \/ (the carrier of S --> {0 }))) by A5, A6, MSAFREE3:20;
then A7: p is FinSequence of (Free S,X) by A6, FINSEQ_1:def 4;
len (the_arity_of o) = len p by MSATERM:22;
hence ( ex s being SortSymbol of S ex v being set st
( [o,the carrier of S] -tree p = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free S,X) st
( [o,the carrier of S] -tree p = [o,the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym o,(X \/ (the carrier of S --> {0 })) ) ) by A7; :: thesis: verum

end;

for t being Term of S,(X \/ (the carrier of S --> {0 })) holds S₁[t] from MSATERM:sch 1(A1, A3);
then S₁[t9] ;
hence ( ex s being SortSymbol of S ex v being set st
( t = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free S,X) st
( t = [o,the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym o,(X \/ (the carrier of S --> {0 })) ) ) ; :: thesis: verum