let S be non void Signature; :: thesis: for X being empty-yielding 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 empty-yielding 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:8;
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:22;
then (root-tree [v,s]) . {} in rng (root-tree [v,s]) by FUNCT_1:3;
then [v,s] in rng (root-tree [v,s]) by TREES_4:3;
then v in X . s by A2, MSAFREE3:35;
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 object 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:2;
reconsider s = s as Element of S by A4;
A6: the Sorts of (Free (S,X)) = S -Terms (X,(X (\/) ( the carrier of S --> {0}))) by MSAFREE3:24;
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:17;
then rng p c= Union (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) by A5, A6, MSAFREE3:19;
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