let S be OrderSortedSign; :: thesis:
let X be V5 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;
A1: Union (coprod X) misses [:the carrier' of S,{the carrier of S}:] by MSAFREE:4;
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:106;
A3: ( len r = len (the_arity_of o) & ( 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 ) ) ) ) ) by A2, Th2;
A4: dom p = dom r by TREES_3:def 18;
A5: ( dom r = Seg (len r) & Seg (len (the_arity_of o)) = dom (the_arity_of o) ) by FINSEQ_1:def 3;
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;
assume A6: n in dom p ; :: thesis:
then consider T being DecoratedTree such that
A7: ( T = p . n & r . n = T . {} ) by TREES_3:def 18;
A8: rng r c= [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X)) by FINSEQ_1:def 4;
A9: r . n in rng r by A4, A6, FUNCT_1:def 5;
A10: rng p c= TS (DTConOSA X) by FINSEQ_1:def 4;
p . n in rng p by A6, FUNCT_1:def 5;
then reconsider T = T as Element of TS (DTConOSA X) by A7, A10;

per cases by A8, A9, 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:9;
A13: x2 = the carrier of S by TARSKI:def 1;
then the_result_sort_of o1 <= (the_arity_of o) /. n by A2, A4, A6, 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 A7, A12, A13;
hence p . n in ParsedTerms X,((the_arity_of o) /. n) by A7; :: thesis:

end;

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

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

end;

hence p in (((ParsedTerms X) # ) * the Arity of S) . o by A3, A4, A5, Th6; :: thesis:

end;

set r = roots p;
set OU = [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X));
assume A17: p in (((ParsedTerms X) # ) * the Arity of S) . o ; :: thesis:
then A18: ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds
p . n in ParsedTerms X,((the_arity_of o) /. n) ) ) by Th6;
A19: dom p = dom (roots p) by TREES_3:def 18;
A20: ( dom (roots p) = Seg (len (roots p)) & Seg (len (the_arity_of o)) = dom (the_arity_of o) ) 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;
A21: len r = len (the_arity_of o) by A18, A19, A20, FINSEQ_1:8;
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 A22: 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 A17, A19, A22, Th6;
then consider a being Element of TS (DTConOSA X) such that
A23: a = p . n and
A24: ( ex s1 being Element of S ex x being set 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 ) ) ;
consider T being DecoratedTree such that
A25: ( T = p . n & r . n = T . {} ) by A19, A22, 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 A26: r . x in [:the carrier' of S,{the carrier of S}:] ; :: thesis:
let o1 be OperSymbol of S; :: thesis:
assume A27: [o1,the carrier of S] = r . x ; :: thesis:

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

end;

then consider o2 being OperSymbol of S such that
A31: ( [o2,the carrier of S] = a . {} & the_result_sort_of o2 <= (the_arity_of o) /. n ) by A24;
thus the_result_sort_of o1 <= (the_arity_of o) /. x by A23, A25, A27, A31, ZFMISC_1:33; :: thesis:

end;

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

given o1 being OperSymbol of S such that A33: ( [o1,the carrier of S] = a . {} & 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:106;
hence contradiction by A1, A23, A25, A32, A33, XBOOLE_0:3; :: thesis:

end;

then consider s1 being Element of S, y being set such that
A34: ( s1 <= (the_arity_of o) /. n & y in X . s1 & a = root-tree [y,s1] ) by A24;
A35: r . x = [y,s1] by A23, A25, A34, TREES_4:3;
take s1 ; :: thesis:
thus ( s1 <= (the_arity_of o) /. x & r . x in coprod s1,X ) by A34, A35, MSAFREE:def 2; :: thesis:

end;

then [[o,the carrier of S],r] in OSREL X by A21, Th2;
hence OSSym o,X ==> roots p by LANG1:def 1; :: thesis: