let S be OrderSortedSign; :: thesis:
let X be non-empty ManySortedSet of S; :: thesis:
let o be OperSymbol of S; :: thesis:
let p be FinSequence of TS (DTConOSA X); :: thesis:
set D = DTConOSA X;
set ar = the_arity_of o;
set r = roots p;
set OU = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
A1: dom p = dom (roots p) by TREES_3:def 18;
thus ( OSSym (o,X) ==> roots p implies p in (((ParsedTerms X) #) * the Arity of S) . o ) :: thesis:

assume OSSym (o,X) ==> roots p ; :: thesis:
then A2: [[o, the carrier of S],(roots p)] in OSREL X by LANG1:def 1;
then reconsider r = roots p as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:87;
A3: dom p = dom r by TREES_3:def 18;
A4: for n being Nat st n in dom p holds
p . n in ParsedTerms (X,((the_arity_of o) /. n))

let n be Nat; :: thesis:
set s = (the_arity_of o) /. n;
A5: rng r c= [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by FINSEQ_1:def 4;
A6: rng p c= TS (DTConOSA X) by FINSEQ_1:def 4;
assume A7: n in dom p ; :: thesis:
then consider T being DecoratedTree such that
A8: T = p . n and
A9: r . n = T . {} by TREES_3:def 18;
p . n in rng p by A7, FUNCT_1:def 3;
then reconsider T = T as Element of TS (DTConOSA X) by A8, A6;
A10: r . n in rng r by A3, A7, FUNCT_1:def 3;

per cases by A5, A10, XBOOLE_0:def 3;

suppose A11: r . n in [: the carrier' of S,{ the carrier of S}:] ; :: thesis:

then consider o1 being Element of the carrier' of S, x2 being Element of { the carrier of S} such that
A12: r . n = [o1,x2] by DOMAIN_1:1;
A13: x2 = the carrier of S by TARSKI:def 1;
then the_result_sort_of o1 <= (the_arity_of o) /. n by A2, A3, A7, A11, A12, Th2;
then ex o being OperSymbol of S st
( [o, the carrier of S] = T . {} & the_result_sort_of o <= (the_arity_of o) /. n ) by A9, A12, A13;
hence p . n in ParsedTerms (X,((the_arity_of o) /. n)) by A8; :: thesis:

end;

suppose A14: r . n in Union (coprod X) ; :: thesis:

then reconsider t = r . n as Terminal of (DTConOSA X) by Th3;
A15: T = root-tree t by A9, DTCONSTR:9;
consider i being Element of S such that
A16: i <= (the_arity_of o) /. n and
A17: r . n in coprod (i,X) by A2, A3, A7, A14, Th2;
ex a being set st
( a in X . i & r . n = [a,i] ) by A17, MSAFREE:def 2;
hence p . n in ParsedTerms (X,((the_arity_of o) /. n)) by A8, A16, A15; :: thesis:

end;

end;

end;

A18: Seg (len (the_arity_of o)) = dom (the_arity_of o) by FINSEQ_1:def 3;
A19: dom r = Seg (len r) by FINSEQ_1:def 3;
len r = len (the_arity_of o) by A2, Th2;
hence p in (((ParsedTerms X) #) * the Arity of S) . o by A3, A19, A18, A4, Th6; :: thesis:

end;

assume A20: p in (((ParsedTerms X) #) * the Arity of S) . o ; :: thesis:
A21: dom (roots p) = Seg (len (roots p)) by FINSEQ_1:def 3;
reconsider r = roots p as FinSequence of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) ;
reconsider r = r as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by FINSEQ_1:def 11;
A22: Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:] by MSAFREE:4;
A23: for x being set st x in dom r holds
( ( r . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = r . x holds
the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( r . x in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. x & r . x in coprod (i,X) ) ) )

let x be set ; :: thesis:
assume A24: x in dom r ; :: thesis:
then reconsider n = x as Nat ;
set s = (the_arity_of o) /. n;
p . n in ParsedTerms (X,((the_arity_of o) /. n)) by A20, A1, A24, Th6;
then consider a being Element of TS (DTConOSA X) such that
A25: a = p . n and
A26: ( ex s1 being Element of S ex x being object st
( s1 <= (the_arity_of o) /. n & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o <= (the_arity_of o) /. n ) ) ;
A27: ex T being DecoratedTree st
( T = p . n & r . n = T . {} ) by A1, A24, TREES_3:def 18;
thus ( r . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = r . x holds
the_result_sort_of o1 <= (the_arity_of o) /. x ) :: thesis:

assume A28: r . x in [: the carrier' of S,{ the carrier of S}:] ; :: thesis:

A29: now :: thesis:

given s1 being Element of S, y being set such that s1 <= (the_arity_of o) /. n and
A30: y in X . s1 and
A31: a = root-tree [y,s1] ; :: thesis:
A32: [y,s1] in coprod (s1,X) by A30, MSAFREE:def 2;
dom (coprod X) = the carrier of S by PARTFUN1:def 2;
then (coprod X) . s1 in rng (coprod X) by FUNCT_1:def 3;
then A33: coprod (s1,X) in rng (coprod X) by MSAFREE:def 3;
r . x = [y,s1] by A25, A27, A31, TREES_4:3;
then r . x in union (rng (coprod X)) by A32, A33, TARSKI:def 4;
then r . x in Union (coprod X) by CARD_3:def 4;
hence contradiction by A22, A28, XBOOLE_0:3; :: thesis:

end;

let o1 be OperSymbol of S; :: thesis:
assume [o1, the carrier of S] = r . x ; :: thesis:
hence the_result_sort_of o1 <= (the_arity_of o) /. x by A25, A26, A27, A29, XTUPLE_0:1; :: thesis:

end;

assume A34: r . x in Union (coprod X) ; :: thesis:

given o1 being OperSymbol of S such that A35: [o1, the carrier of S] = a . {} and
the_result_sort_of o1 <= (the_arity_of o) /. n ; :: thesis:
the carrier of S in { the carrier of S} by TARSKI:def 1;
then [o1, the carrier of S] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87;
hence contradiction by A22, A25, A27, A34, A35, XBOOLE_0:3; :: thesis:

end;

then consider s1 being Element of S, y being set such that
A36: s1 <= (the_arity_of o) /. n and
A37: y in X . s1 and
A38: a = root-tree [y,s1] by A26;
take s1 ; :: thesis:
r . x = [y,s1] by A25, A27, A38, TREES_4:3;
hence ( s1 <= (the_arity_of o) /. x & r . x in coprod (s1,X) ) by A36, A37, MSAFREE:def 2; :: thesis:

end;

dom p = dom (the_arity_of o) by A20, Th6;
then len r = len (the_arity_of o) by A1, A21, FINSEQ_1:def 3;
then [[o, the carrier of S],r] in OSREL X by A23, Th2;
hence OSSym (o,X) ==> roots p by LANG1:def 1; :: thesis: