let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being FinSequence of TS (DTConMSA X) holds
( Sym (o,X) ==> roots p iff p in (((FreeSort X) #) * the Arity of S) . o )
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S
for p being FinSequence of TS (DTConMSA X) holds
( Sym (o,X) ==> roots p iff p in (((FreeSort X) #) * the Arity of S) . o )
let o be OperSymbol of S; :: thesis: for p being FinSequence of TS (DTConMSA X) holds
( Sym (o,X) ==> roots p iff p in (((FreeSort X) #) * the Arity of S) . o )
let p be FinSequence of TS (DTConMSA X); :: thesis: ( Sym (o,X) ==> roots p iff p in (((FreeSort X) #) * the Arity of S) . o )
set D = DTConMSA 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 ( Sym (o,X) ==> roots p implies p in (((FreeSort X) #) * the Arity of S) . o ) :: thesis: ( p in (((FreeSort X) #) * the Arity of S) . o implies Sym (o,X) ==> roots p )

proof

assume Sym (o,X) ==> roots p ; :: thesis: p in (((FreeSort X) #) * the Arity of S) . o
then A2: [[o, the carrier of S],(roots p)] in REL 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: ( dom r = Seg (len r) & Seg (len (the_arity_of o)) = dom (the_arity_of o) ) by FINSEQ_1:def 3;
A5: len r = len (the_arity_of o) by A2, Th5;
for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n))

proof

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

per cases ( r . n in [: the carrier' of S,{ the carrier of S}:] or r . n in Union (coprod X) ) by A9, XBOOLE_0:def 3;

suppose A10: r . n in [: the carrier' of S,{ the carrier of S}:] ; :: thesis: p . n in FreeSort (X,((the_arity_of o) /. n))

then consider o1 being OperSymbol of S, x2 being Element of { the carrier of S} such that
A11: r . n = [o1,x2] by DOMAIN_1:1;
A12: x2 = the carrier of S by TARSKI:def 1;
then the_result_sort_of o1 = (the_arity_of o) . n by A2, A3, A6, A10, A11, Th5
.= (the_arity_of o) /. n by A5, A3, A4, A6, PARTFUN1:def 6 ;
then ( ex x being set st
( x in X . ((the_arity_of o) /. n) & T = root-tree [x,((the_arity_of o) /. n)] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = T . {} & the_result_sort_of o = (the_arity_of o) /. n ) ) by A8, A11, A12;
hence p . n in FreeSort (X,((the_arity_of o) /. n)) by A7; :: thesis: verum

end;

suppose A13: r . n in Union (coprod X) ; :: thesis: p . n in FreeSort (X,((the_arity_of o) /. n))

then r . n in coprod (((the_arity_of o) . n),X) by A2, A3, A6, Th5;
then r . n in coprod (((the_arity_of o) /. n),X) by A5, A3, A4, A6, PARTFUN1:def 6;
then A14: ex a being set st
( a in X . ((the_arity_of o) /. n) & r . n = [a,((the_arity_of o) /. n)] ) by Def2;
reconsider t = r . n as Terminal of (DTConMSA X) by A13, Th6;
T = root-tree t by A8, DTCONSTR:9;
hence p . n in FreeSort (X,((the_arity_of o) /. n)) by A7, A14; :: thesis: verum

end;

end;

end;

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

end;

A15: 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;
assume A16: p in (((FreeSort X) #) * the Arity of S) . o ; :: thesis: Sym (o,X) ==> roots p
then A17: dom p = dom (the_arity_of o) by Th9;
A18: Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:] by Th4;
A19: 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 r . x in coprod (((the_arity_of o) . x),X) ) )

proof

let x be set ; :: thesis: ( x in dom r implies ( ( 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 r . x in coprod (((the_arity_of o) . x),X) ) ) )
assume A20: x in dom r ; :: thesis: ( ( 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 r . x in coprod (((the_arity_of o) . x),X) ) )
then reconsider n = x as Nat ;
A21: ex T being DecoratedTree st
( T = p . n & r . n = T . {} ) by A1, A20, TREES_3:def 18;
set s = (the_arity_of o) /. n;
p . n in FreeSort (X,((the_arity_of o) /. n)) by A16, A1, A20, Th9;
then consider a being Element of TS (DTConMSA X) such that
A22: a = p . n and
A23: ( ex x being set st
( x in X . ((the_arity_of o) /. n) & a = root-tree [x,((the_arity_of o) /. n)] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = (the_arity_of o) /. n ) ) ;
A24: (the_arity_of o) /. n = (the_arity_of o) . n by A17, A1, A20, PARTFUN1:def 6;
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: ( r . x in Union (coprod X) implies r . x in coprod (((the_arity_of o) . x),X) )

proof

assume A25: r . x in [: the carrier' of S,{ the carrier of S}:] ; :: thesis: 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

A26: now :: thesis: for y being set holds
( not y in X . ((the_arity_of o) /. n) or not a = root-tree [y,((the_arity_of o) /. n)] )

dom (coprod X) = the carrier of S by PARTFUN1:def 2;
then (coprod X) . ((the_arity_of o) /. n) in rng (coprod X) by FUNCT_1:def 3;
then A27: coprod (((the_arity_of o) /. n),X) in rng (coprod X) by Def3;
given y being set such that A28: ( y in X . ((the_arity_of o) /. n) & a = root-tree [y,((the_arity_of o) /. n)] ) ; :: thesis: contradiction
( r . x = [y,((the_arity_of o) /. n)] & [y,((the_arity_of o) /. n)] in coprod (((the_arity_of o) /. n),X) ) by A22, A21, A28, Def2, TREES_4:3;
then r . x in union (rng (coprod X)) by A27, TARSKI:def 4;
then r . x in Union (coprod X) by CARD_3:def 4;
hence contradiction by A18, A25, XBOOLE_0:3; :: thesis: verum

end;

let o1 be OperSymbol of S; :: thesis: ( [o1, the carrier of S] = r . x implies the_result_sort_of o1 = (the_arity_of o) . x )
assume [o1, the carrier of S] = r . x ; :: thesis: the_result_sort_of o1 = (the_arity_of o) . x
hence the_result_sort_of o1 = (the_arity_of o) . x by A22, A23, A21, A24, A26, XTUPLE_0:1; :: thesis: verum

end;

assume A29: r . x in Union (coprod X) ; :: thesis: r . x in coprod (((the_arity_of o) . x),X)

now :: thesis: for o1 being OperSymbol of S holds
( not [o1, the carrier of S] = a . {} or not the_result_sort_of o1 = (the_arity_of o) /. n )

given o1 being OperSymbol of S such that A30: [o1, the carrier of S] = a . {} and
the_result_sort_of o1 = (the_arity_of o) /. n ; :: thesis: contradiction
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 A18, A22, A21, A29, A30, XBOOLE_0:3; :: thesis: verum

end;

then consider y being set such that
A31: y in X . ((the_arity_of o) /. n) and
A32: a = root-tree [y,((the_arity_of o) /. n)] by A23;
r . x = [y,((the_arity_of o) /. n)] by A22, A21, A32, TREES_4:3;
hence r . x in coprod (((the_arity_of o) . x),X) by A24, A31, Def2; :: thesis: verum

end;

len r = len (the_arity_of o) by A17, A1, A15, FINSEQ_1:def 3;
then [[o, the carrier of S],r] in REL X by A19, Th5;
hence Sym (o,X) ==> roots p by LANG1:def 1; :: thesis: verum