let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being FinSequence of TS () holds
( Sym (o,X) ==> roots p iff p in ((() #) * the Arity of S) . o )

let X be V5() ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S
for p being FinSequence of TS () holds
( Sym (o,X) ==> roots p iff p in ((() #) * the Arity of S) . o )

let o be OperSymbol of S; :: thesis: for p being FinSequence of TS () holds
( Sym (o,X) ==> roots p iff p in ((() #) * the Arity of S) . o )

let p be FinSequence of TS (); :: thesis: ( Sym (o,X) ==> roots p iff p in ((() #) * 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 ());
A1: dom p = dom () by TREES_3:def 18;
thus ( Sym (o,X) ==> roots p implies p in ((() #) * the Arity of S) . o ) :: thesis: ( p in ((() #) * the Arity of S) . o implies Sym (o,X) ==> roots p )
proof
assume Sym (o,X) ==> roots p ; :: thesis: p in ((() #) * the Arity of S) . o
then A2: [[o, the carrier of S],()] in REL X by LANG1:def 1;
then reconsider r = roots p as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * by ZFMISC_1:87;
A3: dom p = dom r by TREES_3:def 18;
A4: ( dom r = Seg (len r) & Seg (len ()) = dom () ) by FINSEQ_1:def 3;
A5: len r = len () by ;
for n being Nat st n in dom p holds
p . n in FreeSort (X,(() /. n))
proof
let n be Nat; :: thesis: ( n in dom p implies p . n in FreeSort (X,(() /. n)) )
set s = () /. n;
assume A6: n in dom p ; :: thesis: p . n in FreeSort (X,(() /. 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 () & p . n in rng p ) by ;
then reconsider T = T as Element of TS () by A7;
A9: ( rng r c= [: the carrier' of S,{ the carrier of S}:] \/ (Union ()) & r . n in rng r ) by ;
per cases ( r . n in [: the carrier' of S,{ the carrier of S}:] or r . n in Union () ) by ;
suppose A10: r . n in [: the carrier' of S,{ the carrier of S}:] ; :: thesis: p . n in FreeSort (X,(() /. 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 = () . n by A2, A3, A6, A10, A11, Th5
.= () /. n by ;
then ( ex x being set st
( x in X . (() /. n) & T = root-tree [x,(() /. n)] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = T . {} & the_result_sort_of o = () /. n ) ) by A8, A11, A12;
hence p . n in FreeSort (X,(() /. n)) by A7; :: thesis: verum
end;
suppose A13: r . n in Union () ; :: thesis: p . n in FreeSort (X,(() /. n))
then r . n in coprod ((() . n),X) by A2, A3, A6, Th5;
then r . n in coprod ((() /. n),X) by ;
then A14: ex a being set st
( a in X . (() /. n) & r . n = [a,(() /. n)] ) by Def2;
reconsider t = r . n as Terminal of () by ;
T = root-tree t by ;
hence p . n in FreeSort (X,(() /. n)) by ; :: thesis: verum
end;
end;
end;
hence p in ((() #) * the Arity of S) . o by A5, A3, A4, Th9; :: thesis: verum
end;
A15: dom () = Seg (len ()) by FINSEQ_1:def 3;
reconsider r = roots p as FinSequence of [: the carrier' of S,{ the carrier of S}:] \/ (Union ()) ;
reconsider r = r as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * by FINSEQ_1:def 11;
assume A16: p in ((() #) * the Arity of S) . o ; :: thesis: Sym (o,X) ==> roots p
then A17: dom p = dom () by Th9;
A18: Union () 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 = () . x ) & ( r . x in Union () implies r . x in coprod ((() . 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 = () . x ) & ( r . x in Union () implies r . x in coprod ((() . 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 = () . x ) & ( r . x in Union () implies r . x in coprod ((() . x),X) ) )

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

A26: now :: thesis: for y being set holds
( not y in X . (() /. n) or not a = root-tree [y,(() /. n)] )
dom () = the carrier of S by PARTFUN1:def 2;
then (coprod X) . (() /. n) in rng () by FUNCT_1:def 3;
then A27: coprod ((() /. n),X) in rng () by Def3;
given y being set such that A28: ( y in X . (() /. n) & a = root-tree [y,(() /. n)] ) ; :: thesis: contradiction
( r . x = [y,(() /. n)] & [y,(() /. n)] in coprod ((() /. n),X) ) by ;
then r . x in union (rng ()) by ;
then r . x in Union () 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 = () . x )
assume [o1, the carrier of S] = r . x ; :: thesis:
hence the_result_sort_of o1 = () . x by ; :: thesis: verum
end;
assume A29: r . x in Union () ; :: thesis: r . x in coprod ((() . 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 = () /. n )
given o1 being OperSymbol of S such that A30: [o1, the carrier of S] = a . {} and
the_result_sort_of o1 = () /. 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 . (() /. n) and
A32: a = root-tree [y,(() /. n)] by A23;
r . x = [y,(() /. n)] by ;
hence r . x in coprod ((() . x),X) by ; :: thesis: verum
end;
len r = len () by ;
then [[o, the carrier of S],r] in REL X by ;
hence Sym (o,X) ==> roots p by LANG1:def 1; :: thesis: verum