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 (DTConMSA X) holds

( Sym (o,X) ==> roots p iff p in (((FreeSort X) #) * 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 (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 )

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) ) )

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

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 V5() 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

A15:
dom (roots p) = Seg (len (roots p))
by FINSEQ_1:def 3;
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))

end;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

hence
p in (((FreeSort X) #) * the Arity of S) . o
by A5, A3, A4, Th9; :: thesis: verum
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;

end;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;

end;

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;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

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;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

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

len r = len (the_arity_of o)
by A17, A1, A15, FINSEQ_1:def 3;
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) )

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;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 A29:
r . x in Union (coprod X)
; :: thesis: r . x in coprod (((the_arity_of o) . x),X)
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

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;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)] )

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 )( 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;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

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

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 )

then consider y being set such that ( 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;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

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

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