:: MSAFREE3 semantic presentation

begin


registration
let S be non empty non void ManySortedSign ;
let A be non empty MSAlgebra over S;
cluster Union the Sorts of A ->  non empty ;
coherence
 not Union the Sorts of A is empty
proof
A1: dom the Sorts of A = the carrier of S by PARTFUN1:def_2;
consider i being set  such that
A2: i in the carrier of S and
A3: not the Sorts of A . i is empty by PBOOLE:def_12;
set x = the Element of the Sorts of A . i;
 the Element of the Sorts of A . i in the Sorts of A . i by A3;
hence  not Union the Sorts of A is empty by A2, A1, CARD_5:2; ::_thesis: verum
end;
end;

definition
let S be non empty non void ManySortedSign ;
let A be non empty MSAlgebra over S;
mode Element of A is Element of Union the Sorts of A;
end;

theorem :: MSAFREE3:1
for I being set
for A being ManySortedSet of I
for F being ManySortedFunction of I st F is "1-1" & A c= doms F holds
F "" (F .:.: A) = A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I
for F being ManySortedFunction of I st F is "1-1" & A c= doms F holds
F "" (F .:.: A) = A
let A be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of I st F is "1-1" & A c= doms F holds
F "" (F .:.: A) = A
let F be ManySortedFunction of I; ::_thesis: ( F is "1-1" & A c= doms F implies F "" (F .:.: A) = A )
assume that
A1: F is "1-1" and
A2: A c= doms F ; ::_thesis: F "" (F .:.: A) = A
A3: dom F = I by PARTFUN1:def_2;
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(F_""_(F_.:.:_A))_._i_=_A_._i
let i be set ; ::_thesis: ( i in I implies (F "" (F .:.: A)) . i = A . i )
assume A4: i in I ; ::_thesis: (F "" (F .:.: A)) . i = A . i
then A5: F . i is one-to-one by A1, A3, MSUALG_3:def_2;
 A . i c= (doms F) . i by A2, A4, PBOOLE:def_2;
then A6: A . i c= dom (F . i) by A3, A4, FUNCT_6:22;
thus (F "" (F .:.: A)) . i = (F . i) " ((F .:.: A) . i) by A4, EQUATION:def_1
.= (F . i) " ((F . i) .: (A . i)) by A4, PBOOLE:def_20
.= A . i by A6, A5, FUNCT_1:94 ; ::_thesis: verum
end;
hence  F "" (F .:.: A) = A by PBOOLE:3; ::_thesis: verum
end;

definition
let S be non void Signature;
let X be ManySortedSet of the carrier of S;
func Free (S,X) ->  strict MSAlgebra over S means :Def1: :: MSAFREE3:def 1
 ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st
( it = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X );
uniqueness
 for b1, b2 being strict MSAlgebra over S st ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st
( b1 = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) & ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st
( b2 = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) holds
b1 = b2 ;
existence
 ex b1 being strict MSAlgebra over S ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st
( b1 = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X )
proof
set I = the carrier of S;
set Y = X \/ ( the carrier of S --> {0});
set R = Reverse (X \/ ( the carrier of S --> {0}));
 (Reverse (X \/ ( the carrier of S --> {0}))) "" X is ManySortedSubset of FreeGen (X \/ ( the carrier of S --> {0})) by EQUATION:8;
then A1: (Reverse (X \/ ( the carrier of S --> {0}))) "" X c= FreeGen (X \/ ( the carrier of S --> {0})) by PBOOLE:def_18;
 FreeGen (X \/ ( the carrier of S --> {0})) c= the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) by PBOOLE:def_18;
then  (Reverse (X \/ ( the carrier of S --> {0}))) "" X c= the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) by A1, PBOOLE:13;
then reconsider Z = (Reverse (X \/ ( the carrier of S --> {0}))) "" X as MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) by PBOOLE:def_18;
take  GenMSAlg Z ; ::_thesis: ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st
( GenMSAlg Z = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X )
take  Z ; ::_thesis: ( GenMSAlg Z = GenMSAlg Z & Z = (Reverse (X \/ ( the carrier of S --> {0}))) "" X )
thus  ( GenMSAlg Z = GenMSAlg Z & Z = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) ; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Free MSAFREE3:def_1_:_
 for S being non void Signature
for X being ManySortedSet of the carrier of S
for b3 being strict MSAlgebra over S holds
( b3 = Free (S,X) iff ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st
( b3 = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) );

theorem Th2: :: MSAFREE3:2
for x being set
for S being non void Signature
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( [x,s] in the carrier of (DTConMSA X) iff x in X . s )
proof
let x be set ; ::_thesis: for S being non void Signature
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( [x,s] in the carrier of (DTConMSA X) iff x in X . s )
let S be non void Signature; ::_thesis: for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( [x,s] in the carrier of (DTConMSA X) iff x in X . s )
let X be ManySortedSet of the carrier of S; ::_thesis: for s being SortSymbol of S holds
( [x,s] in the carrier of (DTConMSA X) iff x in X . s )
let s be SortSymbol of S; ::_thesis: ( [x,s] in the carrier of (DTConMSA X) iff x in X . s )
A1: DTConMSA X = DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(REL X) #) by MSAFREE:def_8;
A2: dom (coprod X) = the carrier of S by PARTFUN1:def_2;
 s in the carrier of S ;
then  s <> the carrier of S ;
then  not s in { the carrier of S} by TARSKI:def_1;
then A3: not [x,s] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87;
hereby  ::_thesis: ( x in X . s implies [x,s] in the carrier of (DTConMSA X) )
assume  [x,s] in the carrier of (DTConMSA X) ; ::_thesis: x in X . s
then  [x,s] in Union (coprod X) by A1, A3, XBOOLE_0:def_3;
then consider y being set  such that
A4: y in dom (coprod X) and
A5: [x,s] in (coprod X) . y by CARD_5:2;
 (coprod X) . y = coprod (y,X) by A4, MSAFREE:def_3;
then consider z being set  such that
A6: z in X . y and
A7: [x,s] = [z,y] by A4, A5, MSAFREE:def_2;
 x = z by A7, XTUPLE_0:1;
hence  x in X . s by A6, A7, XTUPLE_0:1; ::_thesis: verum
end;
assume  x in X . s ; ::_thesis: [x,s] in the carrier of (DTConMSA X)
then  [x,s] in coprod (s,X) by MSAFREE:def_2;
then  [x,s] in (coprod X) . s by MSAFREE:def_3;
then  [x,s] in Union (coprod X) by A2, CARD_5:2;
hence  [x,s] in the carrier of (DTConMSA X) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th3: :: MSAFREE3:3
for x being set
for S being non void Signature
for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s )
proof
let x be set ; ::_thesis: for S being non void Signature
for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s )
let S be non void Signature; ::_thesis: for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s )
let Y be V8() ManySortedSet of the carrier of S; ::_thesis: for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s )
let X be ManySortedSet of the carrier of S; ::_thesis: for s being SortSymbol of S holds
( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s )
let s be SortSymbol of S; ::_thesis: ( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s )
A1: (Reverse Y) . s = Reverse (s,Y) by MSAFREE:def_18;
A2: dom (Reverse (s,Y)) = FreeGen (s,Y) by FUNCT_2:def_1;
hereby  ::_thesis: ( root-tree [x,s] in ((Reverse Y) "" X) . s implies ( x in X . s & x in Y . s ) )
assume that
A3: x in X . s and
A4: x in Y . s ; ::_thesis: root-tree [x,s] in ((Reverse Y) "" X) . s
A5: root-tree [x,s] in FreeGen (s,Y) by A4, MSAFREE:def_15;
 [x,s] in the carrier of (DTConMSA Y) by A4, Th2;
then ((Reverse Y) . s) . (root-tree [x,s]) = [x,s] `1 by A1, A5, MSAFREE:def_17
.= x ;
then  root-tree [x,s] in ((Reverse Y) . s) " (X . s) by A1, A2, A3, A5, FUNCT_1:def_7;
hence  root-tree [x,s] in ((Reverse Y) "" X) . s by EQUATION:def_1; ::_thesis: verum
end;
assume  root-tree [x,s] in ((Reverse Y) "" X) . s ; ::_thesis: ( x in X . s & x in Y . s )
then A6: root-tree [x,s] in ((Reverse Y) . s) " (X . s) by EQUATION:def_1;
then A7: (Reverse (s,Y)) . (root-tree [x,s]) in X . s by A1, FUNCT_1:def_7;
A8: root-tree [x,s] in FreeGen (s,Y) by A1, A2, A6, FUNCT_1:def_7;
then consider z being set  such that
A9: z in Y . s and
A10: root-tree [x,s] = root-tree [z,s] by MSAFREE:def_15;
A11: [x,s] = [z,s] by A10, TREES_4:4;
then  [x,s] in the carrier of (DTConMSA Y) by A9, Th2;
then  [x,s] `1 in X . s by A8, A7, MSAFREE:def_17;
hence  ( x in X . s & x in Y . s ) by A9, A11, MCART_1:7; ::_thesis: verum
end;

theorem Th4: :: MSAFREE3:4
for x being set
for S being non void Signature
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S st x in X . s holds
root-tree [x,s] in the Sorts of (Free (S,X)) . s
proof
let x be set ; ::_thesis: for S being non void Signature
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S st x in X . s holds
root-tree [x,s] in the Sorts of (Free (S,X)) . s
let S be non void Signature; ::_thesis: for X being ManySortedSet of the carrier of S
for s being SortSymbol of S st x in X . s holds
root-tree [x,s] in the Sorts of (Free (S,X)) . s
let X be ManySortedSet of the carrier of S; ::_thesis: for s being SortSymbol of S st x in X . s holds
root-tree [x,s] in the Sorts of (Free (S,X)) . s
let s be SortSymbol of S; ::_thesis: ( x in X . s implies root-tree [x,s] in the Sorts of (Free (S,X)) . s )
assume A1: x in X . s ; ::_thesis: root-tree [x,s] in the Sorts of (Free (S,X)) . s
set Y = X \/ ( the carrier of S --> {0});
consider A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) such that
A2: Free (S,X) = GenMSAlg A and
A3: A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X by Def1;
 A is MSSubset of (Free (S,X)) by A2, MSUALG_2:def_17;
then  A c= the Sorts of (Free (S,X)) by PBOOLE:def_18;
then A4: A . s c= the Sorts of (Free (S,X)) . s by PBOOLE:def_2;
 X c= X \/ ( the carrier of S --> {0}) by PBOOLE:14;
then  X . s c= (X \/ ( the carrier of S --> {0})) . s by PBOOLE:def_2;
then  root-tree [x,s] in A . s by A1, A3, Th3;
hence  root-tree [x,s] in the Sorts of (Free (S,X)) . s by A4; ::_thesis: verum
end;

theorem Th5: :: MSAFREE3:5
for S being non void Signature
for X being ManySortedSet of the carrier of S
for o being OperSymbol of S st the_arity_of o = {} holds
root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o)
proof
let S be non void Signature; ::_thesis: for X being ManySortedSet of the carrier of S
for o being OperSymbol of S st the_arity_of o = {} holds
root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o)
let X be ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S st the_arity_of o = {} holds
root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o)
let o be OperSymbol of S; ::_thesis: ( the_arity_of o = {} implies root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o) )
assume A1: the_arity_of o = {} ; ::_thesis: root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o)
set Y = X \/ ( the carrier of S --> {0});
A2: Args (o,(FreeMSA (X \/ ( the carrier of S --> {0})))) = (( the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) #) * the Arity of S) . o by MSUALG_1:def_4
.= ( the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) #) . ( the Arity of S . o) by FUNCT_2:15
.= ( the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) #) . (<*> the carrier of S) by A1, MSUALG_1:def_1
.= {{}} by PRE_CIRC:2 ;
then A3: dom (Den (o,(FreeMSA (X \/ ( the carrier of S --> {0}))))) c= {{}} ;
A4: ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st
( Free (S,X) = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) by Def1;
then reconsider FX = the Sorts of (Free (S,X)) as MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) by MSUALG_2:def_9;
((FX #) * the Arity of S) . o = (FX #) . ( the Arity of S . o) by FUNCT_2:15
.= (FX #) . (<*> the carrier of S) by A1, MSUALG_1:def_1
.= {{}} by PRE_CIRC:2 ;
then A5: (Den (o,(FreeMSA (X \/ ( the carrier of S --> {0}))))) | (((FX #) * the Arity of S) . o) = Den (o,(FreeMSA (X \/ ( the carrier of S --> {0})))) by A3, RELAT_1:68;
set a = the ArgumentSeq of Sym (o,(X \/ ( the carrier of S --> {0})));
reconsider a = the ArgumentSeq of Sym (o,(X \/ ( the carrier of S --> {0}))) as Element of Args (o,(FreeMSA (X \/ ( the carrier of S --> {0})))) by INSTALG1:1;
 a = {} by A2, TARSKI:def_1;
then  root-tree [o, the carrier of S] = [o, the carrier of S] -tree a by TREES_4:20;
then  (Den (o,(FreeMSA (X \/ ( the carrier of S --> {0}))))) . a = root-tree [o, the carrier of S] by INSTALG1:3;
then A6: root-tree [o, the carrier of S] in rng (Den (o,(FreeMSA (X \/ ( the carrier of S --> {0}))))) by FUNCT_2:4;
 FX is opers_closed by A4, MSUALG_2:def_9;
then  FX is_closed_on o by MSUALG_2:def_6;
then A7: rng ((Den (o,(FreeMSA (X \/ ( the carrier of S --> {0}))))) | (((FX #) * the Arity of S) . o)) c= (FX * the ResultSort of S) . o by MSUALG_2:def_5;
(FX * the ResultSort of S) . o = FX . ( the ResultSort of S . o) by FUNCT_2:15
.= FX . (the_result_sort_of o) by MSUALG_1:def_2 ;
hence  root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o) by A7, A5, A6; ::_thesis: verum
end;

registration
let S be non void Signature;
let X be V9() ManySortedSet of the carrier of S;
cluster Free (S,X) ->  strict non empty ;
coherence
 not Free (S,X) is empty
proof
consider s being set  such that
A1: s in the carrier of S and
A2: not X . s is empty by PBOOLE:def_12;
reconsider s = s as SortSymbol of S by A1;
set x = the Element of X . s;
 root-tree [ the Element of X . s,s] in the Sorts of (Free (S,X)) . s by A2, Th4;
hence  the Sorts of (Free (S,X)) is V9() ; :: according to CATALG_1:def_2 ::_thesis: verum
end;
end;

theorem :: MSAFREE3:6
for x being set
for S being non void Signature
for X being V8() ManySortedSet of the carrier of S holds
( x is Element of (FreeMSA X) iff x is Term of S,X )
proof
let x be set ; ::_thesis: for S being non void Signature
for X being V8() ManySortedSet of the carrier of S holds
( x is Element of (FreeMSA X) iff x is Term of S,X )
let S be non void Signature; ::_thesis: for X being V8() ManySortedSet of the carrier of S holds
( x is Element of (FreeMSA X) iff x is Term of S,X )
let X be V8() ManySortedSet of the carrier of S; ::_thesis: ( x is Element of (FreeMSA X) iff x is Term of S,X )
A1: S -Terms X = TS (DTConMSA X) by MSATERM:def_1
.= union (rng (FreeSort X)) by MSAFREE:11
.= Union (FreeSort X) by CARD_3:def_4 ;
 FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def_14;
hence  ( x is Element of (FreeMSA X) iff x is Term of S,X ) by A1; ::_thesis: verum
end;

theorem Th7: :: MSAFREE3:7
for S being non void Signature
for X being V8() ManySortedSet of the carrier of S
for s being SortSymbol of S
for x being Term of S,X holds
( x in the Sorts of (FreeMSA X) . s iff the_sort_of x = s )
proof
let S be non void Signature; ::_thesis: for X being V8() ManySortedSet of the carrier of S
for s being SortSymbol of S
for x being Term of S,X holds
( x in the Sorts of (FreeMSA X) . s iff the_sort_of x = s )
let X be V8() ManySortedSet of the carrier of S; ::_thesis: for s being SortSymbol of S
for x being Term of S,X holds
( x in the Sorts of (FreeMSA X) . s iff the_sort_of x = s )
let s be SortSymbol of S; ::_thesis: for x being Term of S,X holds
( x in the Sorts of (FreeMSA X) . s iff the_sort_of x = s )
 FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def_14;
then  the Sorts of (FreeMSA X) . s = FreeSort (X,s) by MSAFREE:def_11;
hence  for x being Term of S,X holds
( x in the Sorts of (FreeMSA X) . s iff the_sort_of x = s ) by MSATERM:def_5; ::_thesis: verum
end;

theorem Th8: :: MSAFREE3:8
for S being non void Signature
for X being V9() ManySortedSet of the carrier of S
for x being Element of (Free (S,X)) holds x is Term of S,(X \/ ( the carrier of S --> {0}))
proof
let S be non void Signature; ::_thesis: for X being V9() ManySortedSet of the carrier of S
for x being Element of (Free (S,X)) holds x is Term of S,(X \/ ( the carrier of S --> {0}))
let X be V9() ManySortedSet of the carrier of S; ::_thesis: for x being Element of (Free (S,X)) holds x is Term of S,(X \/ ( the carrier of S --> {0}))
set Y = X \/ ( the carrier of S --> {0});
let x be Element of (Free (S,X)); ::_thesis: x is Term of S,(X \/ ( the carrier of S --> {0}))
A1: S -Terms (X \/ ( the carrier of S --> {0})) = TS (DTConMSA (X \/ ( the carrier of S --> {0}))) by MSATERM:def_1
.= union (rng (FreeSort (X \/ ( the carrier of S --> {0})))) by MSAFREE:11
.= Union (FreeSort (X \/ ( the carrier of S --> {0}))) by CARD_3:def_4 ;
A2: ( FreeMSA (X \/ ( the carrier of S --> {0})) = MSAlgebra(# (FreeSort (X \/ ( the carrier of S --> {0}))),(FreeOper (X \/ ( the carrier of S --> {0}))) #) & dom the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) = the carrier of S ) by MSAFREE:def_14, PARTFUN1:def_2;
consider y being set  such that
A3: y in dom the Sorts of (Free (S,X)) and
A4: x in the Sorts of (Free (S,X)) . y by CARD_5:2;
 ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st
( Free (S,X) = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) by Def1;
then  the Sorts of (Free (S,X)) is MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) by MSUALG_2:def_9;
then  the Sorts of (Free (S,X)) c= the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) by PBOOLE:def_18;
then  the Sorts of (Free (S,X)) . y c= the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) . y by A3, PBOOLE:def_2;
hence  x is Term of S,(X \/ ( the carrier of S --> {0})) by A1, A3, A4, A2, CARD_5:2; ::_thesis: verum
end;

registration
let S be non empty non void ManySortedSign ;
let X be V9() ManySortedSet of the carrier of S;
cluster  ->  Relation-like Function-like for Element of Union the Sorts of (Free (S,X));
coherence
 for b1 being Element of (Free (S,X)) holds
( b1 is Relation-like & b1 is Function-like ) by Th8;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V9() ManySortedSet of the carrier of S;
cluster  ->  finite DecoratedTree-like for Element of Union the Sorts of (Free (S,X));
coherence
 for b1 being Element of (Free (S,X)) holds
( b1 is finite & b1 is DecoratedTree-like ) by Th8;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V9() ManySortedSet of the carrier of S;
cluster  ->  finite-branching for Element of Union the Sorts of (Free (S,X));
coherence
 for b1 being Element of (Free (S,X)) holds b1 is finite-branching ;
end;

registration
cluster Relation-like Function-like DecoratedTree-like  ->  non empty for set ;
coherence
 for b1 being DecoratedTree holds not b1 is empty by RELAT_1:38;
end;

definition
let S be ManySortedSign ;
let t be non empty Relation;
funcS variables_in t ->  ManySortedSet of the carrier of S means :Def2: :: MSAFREE3:def 2
 for s being set st s in the carrier of S holds
it . s =  {  (a `1) where a is Element of rng t : a `2 = s  }  ;
existence
 ex b1 being ManySortedSet of the carrier of S st
for s being set st s in the carrier of S holds
b1 . s =  {  (a `1) where a is Element of rng t : a `2 = s  }
proof
deffunc H1( set ) ->  set =  {  (a `1) where a is Element of rng t : a `2 = $1  }  ;
 ex f being ManySortedSet of the carrier of S st
for i being set st i in the carrier of S holds
f . i = H1(i) from PBOOLE:sch_4();
hence  ex b1 being ManySortedSet of the carrier of S st
for s being set st s in the carrier of S holds
b1 . s =  {  (a `1) where a is Element of rng t : a `2 = s  }  ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedSet of the carrier of S st ( for s being set st s in the carrier of S holds
b1 . s =  {  (a `1) where a is Element of rng t : a `2 = s  }  ) & ( for s being set st s in the carrier of S holds
b2 . s =  {  (a `1) where a is Element of rng t : a `2 = s  }  ) holds
b1 = b2
proof
let V1, V2 be ManySortedSet of the carrier of S; ::_thesis: ( ( for s being set st s in the carrier of S holds
V1 . s =  {  (a `1) where a is Element of rng t : a `2 = s  }  ) & ( for s being set st s in the carrier of S holds
V2 . s =  {  (a `1) where a is Element of rng t : a `2 = s  }  ) implies V1 = V2 )
assume that
A1: for s being set st s in the carrier of S holds
V1 . s =  {  (a `1) where a is Element of rng t : a `2 = s  }  and
A2: for s being set st s in the carrier of S holds
V2 . s =  {  (a `1) where a is Element of rng t : a `2 = s  }  ; ::_thesis: V1 = V2
now__::_thesis:_for_s_being_set_st_s_in_the_carrier_of_S_holds_
V1_._s_=_V2_._s
let s be set ; ::_thesis: ( s in the carrier of S implies V1 . s = V2 . s )
assume A3: s in the carrier of S ; ::_thesis: V1 . s = V2 . s
hence V1 . s =  {  (a `1) where a is Element of rng t : a `2 = s  }  by A1
.= V2 . s by A2, A3 ;
::_thesis: verum
end;
hence  V1 = V2 by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines variables_in MSAFREE3:def_2_:_
 for S being ManySortedSign
for t being non empty Relation
for b3 being ManySortedSet of the carrier of S holds
( b3 = S variables_in t iff for s being set st s in the carrier of S holds
b3 . s =  {  (a `1) where a is Element of rng t : a `2 = s  }  );

definition
let S be ManySortedSign ;
let X be ManySortedSet of the carrier of S;
let t be non empty Relation;
funcX variables_in t ->  ManySortedSubset of X equals :: MSAFREE3:def 3
X /\ (S variables_in t);
coherence
 X /\ (S variables_in t) is ManySortedSubset of X
proof
thus  X /\ (S variables_in t) c= X by PBOOLE:15; :: according to PBOOLE:def_18 ::_thesis: verum
end;
end;

:: deftheorem  defines variables_in MSAFREE3:def_3_:_
 for S being ManySortedSign
for X being ManySortedSet of the carrier of S
for t being non empty Relation holds X variables_in t = X /\ (S variables_in t);

theorem Th9: :: MSAFREE3:9
for S being ManySortedSign
for X being ManySortedSet of the carrier of S
for t being non empty Relation
for V being ManySortedSubset of X holds
( V = X variables_in t iff for s being set st s in the carrier of S holds
V . s = (X . s) /\  {  (a `1) where a is Element of rng t : a `2 = s  }  )
proof
let S be ManySortedSign ; ::_thesis: for X being ManySortedSet of the carrier of S
for t being non empty Relation
for V being ManySortedSubset of X holds
( V = X variables_in t iff for s being set st s in the carrier of S holds
V . s = (X . s) /\  {  (a `1) where a is Element of rng t : a `2 = s  }  )
let X be ManySortedSet of the carrier of S; ::_thesis: for t being non empty Relation
for V being ManySortedSubset of X holds
( V = X variables_in t iff for s being set st s in the carrier of S holds
V . s = (X . s) /\  {  (a `1) where a is Element of rng t : a `2 = s  }  )
let t be non empty Relation; ::_thesis: for V being ManySortedSubset of X holds
( V = X variables_in t iff for s being set st s in the carrier of S holds
V . s = (X . s) /\  {  (a `1) where a is Element of rng t : a `2 = s  }  )
let V be ManySortedSubset of X; ::_thesis: ( V = X variables_in t iff for s being set st s in the carrier of S holds
V . s = (X . s) /\  {  (a `1) where a is Element of rng t : a `2 = s  }  )
hereby  ::_thesis: ( ( for s being set st s in the carrier of S holds
V . s = (X . s) /\  {  (a `1) where a is Element of rng t : a `2 = s  }  ) implies V = X variables_in t )
assume A1: V = X variables_in t ; ::_thesis: for s being set st s in the carrier of S holds
V . s = (X . s) /\  {  (a `1) where a is Element of rng t : a `2 = s  }
let s be set ; ::_thesis: ( s in the carrier of S implies V . s = (X . s) /\  {  (a `1) where a is Element of rng t : a `2 = s  }  )
assume A2: s in the carrier of S ; ::_thesis: V . s = (X . s) /\  {  (a `1) where a is Element of rng t : a `2 = s  }
then  V . s = (X . s) /\ ((S variables_in t) . s) by A1, PBOOLE:def_5;
hence  V . s = (X . s) /\  {  (a `1) where a is Element of rng t : a `2 = s  }  by A2, Def2; ::_thesis: verum
end;
assume A3: for s being set st s in the carrier of S holds
V . s = (X . s) /\  {  (a `1) where a is Element of rng t : a `2 = s  }  ; ::_thesis: V = X variables_in t
now__::_thesis:_for_s_being_set_st_s_in_the_carrier_of_S_holds_
V_._s_=_(X_._s)_/\_((S_variables_in_t)_._s)
let s be set ; ::_thesis: ( s in the carrier of S implies V . s = (X . s) /\ ((S variables_in t) . s) )
assume A4: s in the carrier of S ; ::_thesis: V . s = (X . s) /\ ((S variables_in t) . s)
hence V . s = (X . s) /\  {  (a `1) where a is Element of rng t : a `2 = s  }  by A3
.= (X . s) /\ ((S variables_in t) . s) by A4, Def2 ;
::_thesis: verum
end;
hence  V = X variables_in t by PBOOLE:def_5; ::_thesis: verum
end;

theorem Th10: :: MSAFREE3:10
for S being ManySortedSign
for s, x being set holds
( ( s in the carrier of S implies (S variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not s in the carrier of S ) holds
(S variables_in (root-tree [x,s])) . s9 = {} ) )
proof
let S be ManySortedSign ; ::_thesis: for s, x being set holds
( ( s in the carrier of S implies (S variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not s in the carrier of S ) holds
(S variables_in (root-tree [x,s])) . s9 = {} ) )
let s, x be set ; ::_thesis: ( ( s in the carrier of S implies (S variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not s in the carrier of S ) holds
(S variables_in (root-tree [x,s])) . s9 = {} ) )
reconsider t = root-tree [x,s] as DecoratedTree ;
A1: [x,s] `2 = s ;
 t = {[{},[x,s]]} by TREES_4:6;
then A2: rng t = {[x,s]} by RELAT_1:9;
A3: [x,s] `1 = x ;
hereby  ::_thesis: for s9 being set st ( s9 <> s or not s in the carrier of S ) holds
(S variables_in (root-tree [x,s])) . s9 = {}
assume  s in the carrier of S ; ::_thesis: (S variables_in (root-tree [x,s])) . s = {x}
then A4: (S variables_in t) . s =  {  (a `1) where a is Element of rng t : a `2 = s  }  by Def2;
thus  (S variables_in (root-tree [x,s])) . s = {x} ::_thesis: verum
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {x} c= (S variables_in (root-tree [x,s])) . s
let y be set ; ::_thesis: ( y in (S variables_in (root-tree [x,s])) . s implies y in {x} )
assume  y in (S variables_in (root-tree [x,s])) . s ; ::_thesis: y in {x}
then consider a being Element of rng t such that
A5: y = a `1 and
 a `2 = s by A4;
 a = [x,s] by A2, TARSKI:def_1;
hence  y in {x} by A3, A5, TARSKI:def_1; ::_thesis: verum
end;
 [x,s] in rng t by A2, TARSKI:def_1;
then  x in  {  (a `1) where a is Element of rng t : a `2 = s  }  by A3, A1;
hence  {x} c= (S variables_in (root-tree [x,s])) . s by A4, ZFMISC_1:31; ::_thesis: verum
end;
end;
let s9 be set ; ::_thesis: ( ( s9 <> s or not s in the carrier of S ) implies (S variables_in (root-tree [x,s])) . s9 = {} )
assume A6: ( s9 <> s or not s in the carrier of S ) ; ::_thesis: (S variables_in (root-tree [x,s])) . s9 = {}
set y = the Element of (S variables_in (root-tree [x,s])) . s9;
assume A7: (S variables_in (root-tree [x,s])) . s9 <> {} ; ::_thesis: contradiction
then A8: the Element of (S variables_in (root-tree [x,s])) . s9 in (S variables_in t) . s9 ;
 dom (S variables_in t) = the carrier of S by PARTFUN1:def_2;
then A9: s9 in the carrier of S by A7, FUNCT_1:def_2;
then  (S variables_in t) . s9 =  {  (a `1) where a is Element of rng t : a `2 = s9  }  by Def2;
then  ex a being Element of rng t st
( the Element of (S variables_in (root-tree [x,s])) . s9 = a `1 & a `2 = s9 ) by A8;
hence  contradiction by A2, A1, A6, A9, TARSKI:def_1; ::_thesis: verum
end;

theorem Th11: :: MSAFREE3:11
for x, z being set
for S being ManySortedSign
for s being set st s in the carrier of S holds
for p being DTree-yielding FinSequence holds
( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (S variables_in t) . s ) )
proof
let x, z be set ; ::_thesis: for S being ManySortedSign
for s being set st s in the carrier of S holds
for p being DTree-yielding FinSequence holds
( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (S variables_in t) . s ) )
let S be ManySortedSign ; ::_thesis: for s being set st s in the carrier of S holds
for p being DTree-yielding FinSequence holds
( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (S variables_in t) . s ) )
let s be set ; ::_thesis: ( s in the carrier of S implies for p being DTree-yielding FinSequence holds
( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (S variables_in t) . s ) ) )
assume A1: s in the carrier of S ; ::_thesis: for p being DTree-yielding FinSequence holds
( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (S variables_in t) . s ) )
let p be DTree-yielding FinSequence; ::_thesis: ( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (S variables_in t) . s ) )
reconsider q = [z, the carrier of S] -tree p as DecoratedTree ;
A2: (S variables_in q) . s =  {  (a `1) where a is Element of rng q : a `2 = s  }  by A1, Def2;
A3: dom q = tree (doms p) by TREES_4:10;
A4: dom (doms p) = dom p by TREES_3:37;
then A5: len p = len (doms p) by FINSEQ_3:29;
hereby  ::_thesis: ( ex t being DecoratedTree st
( t in rng p & x in (S variables_in t) . s ) implies x in (S variables_in ([z, the carrier of S] -tree p)) . s )
assume  x in (S variables_in ([z, the carrier of S] -tree p)) . s ; ::_thesis: ex t being DecoratedTree st
( t in rng p & x in (S variables_in t) . s )
then consider a being Element of rng q such that
A6: x = a `1 and
A7: a `2 = s by A2;
consider y being set  such that
A8: y in dom q and
A9: a = q . y by FUNCT_1:def_3;
reconsider y = y as Element of dom q by A8;
 ( q . {} = [z, the carrier of S] & s <> the carrier of S ) by A1, TREES_4:def_4;
then  y <> {} by A7, A9, MCART_1:7;
then consider n being Element of NAT , r being FinSequence such that
A10: n < len (doms p) and
A11: r in (doms p) . (n + 1) and
A12: y = <*n*> ^ r by A3, TREES_3:def_15;
 ( 1 <= n + 1 & n + 1 <= len (doms p) ) by A10, NAT_1:11, NAT_1:13;
then A13: n + 1 in dom (doms p) by FINSEQ_3:25;
then reconsider t = p . (n + 1) as DecoratedTree by A4, TREES_3:24;
reconsider r = r as FinSequence of NAT by A12, FINSEQ_1:36;
take t = t; ::_thesis: ( t in rng p & x in (S variables_in t) . s )
thus  t in rng p by A4, A13, FUNCT_1:def_3; ::_thesis: x in (S variables_in t) . s
A14: (doms p) . (n + 1) = dom t by A4, A13, FUNCT_6:22;
A15: t = q | <*n*> by A5, A10, TREES_4:def_4;
then  dom t = (dom q) | <*n*> by TREES_2:def_10;
then  a = t . r by A9, A11, A12, A15, A14, TREES_2:def_10;
then  a in rng t by A11, A14, FUNCT_1:def_3;
then  x in  {  (b `1) where b is Element of rng t : b `2 = s  }  by A6, A7;
hence  x in (S variables_in t) . s by A1, Def2; ::_thesis: verum
end;
given t being DecoratedTree such that A16: t in rng p and
A17: x in (S variables_in t) . s ; ::_thesis: x in (S variables_in ([z, the carrier of S] -tree p)) . s
consider y being set  such that
A18: y in dom p and
A19: t = p . y by A16, FUNCT_1:def_3;
reconsider y = y as Element of NAT by A18;
 y >= 1 by A18, FINSEQ_3:25;
then consider n being Nat such that
A20: y = 1 + n by NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
 y <= len p by A18, FINSEQ_3:25;
then A21: n < len p by A20, NAT_1:13;
then A22: t = q | <*n*> by A19, A20, TREES_4:def_4;
A23: ( {} in dom t & <*n*> ^ {} = <*n*> ) by FINSEQ_1:34, TREES_1:22;
 dom t = (doms p) . (n + 1) by A18, A19, A20, FUNCT_6:22;
then  <*n*> in dom q by A3, A5, A21, A23, TREES_3:def_15;
then A24: rng t c= rng q by A22, TREES_2:32;
 x in  {  (b `1) where b is Element of rng t : b `2 = s  }  by A1, A17, Def2;
then consider b being Element of rng t such that
A25: ( x = b `1 & b `2 = s ) ;
 b in rng t ;
hence  x in (S variables_in ([z, the carrier of S] -tree p)) . s by A2, A25, A24; ::_thesis: verum
end;

theorem Th12: :: MSAFREE3:12
for S being ManySortedSign
for X being ManySortedSet of the carrier of S
for s, x being set holds
( ( x in X . s implies (X variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not x in X . s ) holds
(X variables_in (root-tree [x,s])) . s9 = {} ) )
proof
let S be ManySortedSign ; ::_thesis: for X being ManySortedSet of the carrier of S
for s, x being set holds
( ( x in X . s implies (X variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not x in X . s ) holds
(X variables_in (root-tree [x,s])) . s9 = {} ) )
let X be ManySortedSet of the carrier of S; ::_thesis: for s, x being set holds
( ( x in X . s implies (X variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not x in X . s ) holds
(X variables_in (root-tree [x,s])) . s9 = {} ) )
let s, x be set ; ::_thesis: ( ( x in X . s implies (X variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not x in X . s ) holds
(X variables_in (root-tree [x,s])) . s9 = {} ) )
reconsider t = root-tree [x,s] as DecoratedTree ;
A1: ( [x,s] `1 = x & [x,s] `2 = s ) ;
hereby  ::_thesis: for s9 being set st ( s9 <> s or not x in X . s ) holds
(X variables_in (root-tree [x,s])) . s9 = {}
assume A2: x in X . s ; ::_thesis: (X variables_in (root-tree [x,s])) . s = {x}
then A3: {x} c= X . s by ZFMISC_1:31;
 dom X = the carrier of S by PARTFUN1:def_2;
then A4: s in the carrier of S by A2, FUNCT_1:def_2;
then  (S variables_in (root-tree [x,s])) . s = {x} by Th10;
then  (X . s) /\ ((S variables_in (root-tree [x,s])) . s) = {x} by A3, XBOOLE_1:28;
hence  (X variables_in (root-tree [x,s])) . s = {x} by A4, PBOOLE:def_5; ::_thesis: verum
end;
let s9 be set ; ::_thesis: ( ( s9 <> s or not x in X . s ) implies (X variables_in (root-tree [x,s])) . s9 = {} )
assume A5: ( s9 <> s or not x in X . s ) ; ::_thesis: (X variables_in (root-tree [x,s])) . s9 = {}
set y = the Element of (X variables_in (root-tree [x,s])) . s9;
assume A6: (X variables_in (root-tree [x,s])) . s9 <> {} ; ::_thesis: contradiction
 dom (X variables_in t) = the carrier of S by PARTFUN1:def_2;
then  s9 in the carrier of S by A6, FUNCT_1:def_2;
then A7: (X variables_in t) . s9 = (X . s9) /\  {  (a `1) where a is Element of rng t : a `2 = s9  }  by Th9;
then  the Element of (X variables_in (root-tree [x,s])) . s9 in  {  (a `1) where a is Element of rng t : a `2 = s9  }  by A6, XBOOLE_0:def_4;
then consider a being Element of rng t such that
A8: ( the Element of (X variables_in (root-tree [x,s])) . s9 = a `1 & a `2 = s9 ) ;
 t = {[{},[x,s]]} by TREES_4:6;
then  rng t = {[x,s]} by RELAT_1:9;
then  a = [x,s] by TARSKI:def_1;
hence  contradiction by A1, A5, A6, A7, A8, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th13: :: MSAFREE3:13
for x, z being set
for S being ManySortedSign
for X being ManySortedSet of the carrier of S
for s being set st s in the carrier of S holds
for p being DTree-yielding FinSequence holds
( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (X variables_in t) . s ) )
proof
let x, z be set ; ::_thesis: for S being ManySortedSign
for X being ManySortedSet of the carrier of S
for s being set st s in the carrier of S holds
for p being DTree-yielding FinSequence holds
( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (X variables_in t) . s ) )
let S be ManySortedSign ; ::_thesis: for X being ManySortedSet of the carrier of S
for s being set st s in the carrier of S holds
for p being DTree-yielding FinSequence holds
( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (X variables_in t) . s ) )
let X be ManySortedSet of the carrier of S; ::_thesis: for s being set st s in the carrier of S holds
for p being DTree-yielding FinSequence holds
( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (X variables_in t) . s ) )
let s be set ; ::_thesis: ( s in the carrier of S implies for p being DTree-yielding FinSequence holds
( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (X variables_in t) . s ) ) )
assume A1: s in the carrier of S ; ::_thesis: for p being DTree-yielding FinSequence holds
( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (X variables_in t) . s ) )
let p be DTree-yielding FinSequence; ::_thesis: ( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (X variables_in t) . s ) )
reconsider q = [z, the carrier of S] -tree p as DecoratedTree ;
 (X variables_in q) . s = (X . s) /\ ((S variables_in q) . s) by A1, PBOOLE:def_5;
then A2: ( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ( x in X . s & x in (S variables_in ([z, the carrier of S] -tree p)) . s ) ) by XBOOLE_0:def_4;
then A3: ( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ( x in X . s & ex t being DecoratedTree st
( t in rng p & x in (S variables_in t) . s ) ) ) by A1, Th11;
hereby  ::_thesis: ( ex t being DecoratedTree st
( t in rng p & x in (X variables_in t) . s ) implies x in (X variables_in ([z, the carrier of S] -tree p)) . s )
assume  x in (X variables_in ([z, the carrier of S] -tree p)) . s ; ::_thesis: ex t being DecoratedTree st
( t in rng p & x in (X variables_in t) . s )
then consider t being DecoratedTree such that
A4: t in rng p and
A5: ( x in X . s & x in (S variables_in t) . s ) by A3;
take t = t; ::_thesis: ( t in rng p & x in (X variables_in t) . s )
thus  t in rng p by A4; ::_thesis: x in (X variables_in t) . s
 x in (X . s) /\ ((S variables_in t) . s) by A5, XBOOLE_0:def_4;
hence  x in (X variables_in t) . s by A1, PBOOLE:def_5; ::_thesis: verum
end;
given t being DecoratedTree such that A6: t in rng p and
A7: x in (X variables_in t) . s ; ::_thesis: x in (X variables_in ([z, the carrier of S] -tree p)) . s
A8: (X variables_in t) . s = (X . s) /\ ((S variables_in t) . s) by A1, PBOOLE:def_5;
then  x in (S variables_in t) . s by A7, XBOOLE_0:def_4;
hence  x in (X variables_in ([z, the carrier of S] -tree p)) . s by A1, A2, A6, A7, A8, Th11, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th14: :: MSAFREE3:14
for S being non void Signature
for X being V8() ManySortedSet of the carrier of S
for t being Term of S,X holds S variables_in t c= X
proof
let S be non void Signature; ::_thesis: for X being V8() ManySortedSet of the carrier of S
for t being Term of S,X holds S variables_in t c= X
let X be V8() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,X holds S variables_in t c= X
defpred S1[ DecoratedTree] means S variables_in $1 c= X;
A1: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st ( for t being Term of S,X st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]
proof
let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,X) st ( for t being Term of S,X st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]
let p be ArgumentSeq of Sym (o,X); ::_thesis: ( ( for t being Term of S,X st t in rng p holds
S1[t] ) implies S1[[o, the carrier of S] -tree p] )
assume A2: for t being Term of S,X st t in rng p holds
S variables_in t c= X ; ::_thesis: S1[[o, the carrier of S] -tree p]
set q = [o, the carrier of S] -tree p;
thus  S variables_in ([o, the carrier of S] -tree p) c= X ::_thesis: verum
proof
let s9 be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s9 in the carrier of S or (S variables_in ([o, the carrier of S] -tree p)) . s9 c= X . s9 )
assume  s9 in the carrier of S ; ::_thesis: (S variables_in ([o, the carrier of S] -tree p)) . s9 c= X . s9
then reconsider z = s9 as SortSymbol of S ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (S variables_in ([o, the carrier of S] -tree p)) . s9 or x in X . s9 )
assume  x in (S variables_in ([o, the carrier of S] -tree p)) . s9 ; ::_thesis: x in X . s9
then consider t being DecoratedTree such that
A3: t in rng p and
A4: x in (S variables_in t) . z by Th11;
consider i being set  such that
A5: i in dom p and
A6: t = p . i by A3, FUNCT_1:def_3;
reconsider i = i as Nat by A5;
reconsider t = p . i as Term of S,X by A5, MSATERM:22;
 S variables_in t c= X by A2, A3, A6;
then  (S variables_in t) . z c= X . z by PBOOLE:def_2;
hence  x in X . s9 by A4, A6; ::_thesis: verum
end;
end;
A7: for s being SortSymbol of S
for v being Element of X . s holds S1[ root-tree [v,s]]
proof
let s be SortSymbol of S; ::_thesis: for v being Element of X . s holds S1[ root-tree [v,s]]
let v be Element of X . s; ::_thesis: S1[ root-tree [v,s]]
thus  S variables_in (root-tree [v,s]) c= X ::_thesis: verum
proof
let s9 be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s9 in the carrier of S or (S variables_in (root-tree [v,s])) . s9 c= X . s9 )
assume  s9 in the carrier of S ; ::_thesis: (S variables_in (root-tree [v,s])) . s9 c= X . s9
then reconsider z = s9 as SortSymbol of S ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (S variables_in (root-tree [v,s])) . s9 or x in X . s9 )
assume A8: x in (S variables_in (root-tree [v,s])) . s9 ; ::_thesis: x in X . s9
then A9: ( s <> z implies x in {} ) by Th10;
 ( s = z implies x in {v} ) by A8, Th10;
hence  x in X . s9 by A9; ::_thesis: verum
end;
end;
 for t being Term of S,X holds S1[t] from MSATERM:sch_1(A7, A1);
hence  for t being Term of S,X holds S variables_in t c= X ; ::_thesis: verum
end;

definition
let S be non void Signature;
let X be V8() ManySortedSet of the carrier of S;
let t be Term of S,X;
func variables_in t ->  ManySortedSubset of X equals :: MSAFREE3:def 4
S variables_in t;
correctness
coherence
S variables_in t is ManySortedSubset of X;
proof
 S variables_in t c= X by Th14;
then  S variables_in t = X variables_in t by PBOOLE:23;
hence  S variables_in t is ManySortedSubset of X ; ::_thesis: verum
end;
end;

:: deftheorem  defines variables_in MSAFREE3:def_4_:_
 for S being non void Signature
for X being V8() ManySortedSet of the carrier of S
for t being Term of S,X holds variables_in t = S variables_in t;

theorem Th15: :: MSAFREE3:15
for S being non void Signature
for X being V8() ManySortedSet of the carrier of S
for t being Term of S,X holds variables_in t = X variables_in t by Th14, PBOOLE:23;

definition
let S be non void Signature;
let Y be V8() ManySortedSet of the carrier of S;
let X be ManySortedSet of the carrier of S;
funcS -Terms (X,Y) ->  MSSubset of (FreeMSA Y) means :Def5: :: MSAFREE3:def 5
 for s being SortSymbol of S holds it . s =  {  t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X )  }  ;
existence
 ex b1 being MSSubset of (FreeMSA Y) st
for s being SortSymbol of S holds b1 . s =  {  t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X )  }
proof
deffunc H1( SortSymbol of S) ->  set =  {  t where t is Term of S,Y : ( the_sort_of t = $1 & variables_in t c= X )  }  ;
consider T being ManySortedSet of the carrier of S such that
A1: for s being SortSymbol of S holds T . s = H1(s) from PBOOLE:sch_5();
 T c= the Sorts of (FreeMSA Y)
proof
let s be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s in the carrier of S or T . s c= the Sorts of (FreeMSA Y) . s )
assume  s in the carrier of S ; ::_thesis: T . s c= the Sorts of (FreeMSA Y) . s
then reconsider s9 = s as SortSymbol of S ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T . s or x in the Sorts of (FreeMSA Y) . s )
assume A2: x in T . s ; ::_thesis: x in the Sorts of (FreeMSA Y) . s
 T . s9 =  {  t where t is Term of S,Y : ( the_sort_of t = s9 & variables_in t c= X )  }  by A1;
then  ex t being Term of S,Y st
( x = t & the_sort_of t = s9 & variables_in t c= X ) by A2;
hence  x in the Sorts of (FreeMSA Y) . s by Th7; ::_thesis: verum
end;
then reconsider T = T as MSSubset of (FreeMSA Y) by PBOOLE:def_18;
take  T ; ::_thesis: for s being SortSymbol of S holds T . s =  {  t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X )  }
thus  for s being SortSymbol of S holds T . s =  {  t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X )  }  by A1; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being MSSubset of (FreeMSA Y) st ( for s being SortSymbol of S holds b1 . s =  {  t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X )  }  ) & ( for s being SortSymbol of S holds b2 . s =  {  t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X )  }  ) holds
b1 = b2;
proof
let T1, T2 be MSSubset of (FreeMSA Y); ::_thesis: ( ( for s being SortSymbol of S holds T1 . s =  {  t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X )  }  ) & ( for s being SortSymbol of S holds T2 . s =  {  t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X )  }  ) implies T1 = T2 )
assume that
A3: for s being SortSymbol of S holds T1 . s =  {  t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X )  }  and
A4: for s being SortSymbol of S holds T2 . s =  {  t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X )  }  ; ::_thesis: T1 = T2
now__::_thesis:_for_s_being_set_st_s_in_the_carrier_of_S_holds_
T1_._s_=_T2_._s
let s be set ; ::_thesis: ( s in the carrier of S implies T1 . s = T2 . s )
assume A5: s in the carrier of S ; ::_thesis: T1 . s = T2 . s
hence T1 . s =  {  t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X )  }  by A3
.= T2 . s by A4, A5 ;
::_thesis: verum
end;
hence  T1 = T2 by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines -Terms MSAFREE3:def_5_:_
 for S being non void Signature
for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for b4 being MSSubset of (FreeMSA Y) holds
( b4 = S -Terms (X,Y) iff for s being SortSymbol of S holds b4 . s =  {  t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X )  }  );

theorem Th16: :: MSAFREE3:16
for x being set
for S being non void Signature
for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S st x in (S -Terms (X,Y)) . s holds
x is Term of S,Y
proof
let x be set ; ::_thesis: for S being non void Signature
for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S st x in (S -Terms (X,Y)) . s holds
x is Term of S,Y
let S be non void Signature; ::_thesis: for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S st x in (S -Terms (X,Y)) . s holds
x is Term of S,Y
let Y be V8() ManySortedSet of the carrier of S; ::_thesis: for X being ManySortedSet of the carrier of S
for s being SortSymbol of S st x in (S -Terms (X,Y)) . s holds
x is Term of S,Y
let X be ManySortedSet of the carrier of S; ::_thesis: for s being SortSymbol of S st x in (S -Terms (X,Y)) . s holds
x is Term of S,Y
let s be SortSymbol of S; ::_thesis: ( x in (S -Terms (X,Y)) . s implies x is Term of S,Y )
assume  x in (S -Terms (X,Y)) . s ; ::_thesis: x is Term of S,Y
then  x in  {  t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X )  }  by Def5;
then  ex t being Term of S,Y st
( x = t & the_sort_of t = s & variables_in t c= X ) ;
hence  x is Term of S,Y ; ::_thesis: verum
end;

theorem Th17: :: MSAFREE3:17
for S being non void Signature
for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for t being Term of S,Y
for s being SortSymbol of S st t in (S -Terms (X,Y)) . s holds
( the_sort_of t = s & variables_in t c= X )
proof
let S be non void Signature; ::_thesis: for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for t being Term of S,Y
for s being SortSymbol of S st t in (S -Terms (X,Y)) . s holds
( the_sort_of t = s & variables_in t c= X )
let Y be V8() ManySortedSet of the carrier of S; ::_thesis: for X being ManySortedSet of the carrier of S
for t being Term of S,Y
for s being SortSymbol of S st t in (S -Terms (X,Y)) . s holds
( the_sort_of t = s & variables_in t c= X )
let X be ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,Y
for s being SortSymbol of S st t in (S -Terms (X,Y)) . s holds
( the_sort_of t = s & variables_in t c= X )
let q be Term of S,Y; ::_thesis: for s being SortSymbol of S st q in (S -Terms (X,Y)) . s holds
( the_sort_of q = s & variables_in q c= X )
let s be SortSymbol of S; ::_thesis: ( q in (S -Terms (X,Y)) . s implies ( the_sort_of q = s & variables_in q c= X ) )
assume A1: q in (S -Terms (X,Y)) . s ; ::_thesis: ( the_sort_of q = s & variables_in q c= X )
 (S -Terms (X,Y)) . s =  {  t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X )  }  by Def5;
then  ex t being Term of S,Y st
( q = t & the_sort_of t = s & variables_in t c= X ) by A1;
hence  ( the_sort_of q = s & variables_in q c= X ) ; ::_thesis: verum
end;

theorem Th18: :: MSAFREE3:18
for x being set
for S being non void Signature
for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) )
proof
let x be set ; ::_thesis: for S being non void Signature
for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) )
let S be non void Signature; ::_thesis: for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) )
let Y be V8() ManySortedSet of the carrier of S; ::_thesis: for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) )
let X be ManySortedSet of the carrier of S; ::_thesis: for s being SortSymbol of S holds
( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) )
let s be SortSymbol of S; ::_thesis: ( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) )
A1: (S -Terms (X,Y)) . s =  {  t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X )  }  by Def5;
hereby  ::_thesis: ( x in X . s & x in Y . s implies root-tree [x,s] in (S -Terms (X,Y)) . s )
assume  root-tree [x,s] in (S -Terms (X,Y)) . s ; ::_thesis: ( x in X . s & x in Y . s )
then consider t being Term of S,Y such that
A2: root-tree [x,s] = t and
 the_sort_of t = s and
A3: variables_in t c= X by A1;
A4: t . {} = [x,s] by A2, TREES_4:3;
 s in the carrier of S ;
then  s <> the carrier of S ;
then  not s in { the carrier of S} by TARSKI:def_1;
then  not t . {} in [: the carrier' of S,{ the carrier of S}:] by A4, ZFMISC_1:87;
then consider s9 being SortSymbol of S, v being Element of Y . s9 such that
A5: t . {} = [v,s9] by MSATERM:2;
A6: ( s = s9 & x = v ) by A4, A5, XTUPLE_0:1;
 ( (S variables_in t) . s = {x} & (variables_in t) . s c= X . s ) by A2, A3, Th10, PBOOLE:def_2;
hence  ( x in X . s & x in Y . s ) by A6, ZFMISC_1:31; ::_thesis: verum
end;
assume that
A7: x in X . s and
A8: x in Y . s ; ::_thesis: root-tree [x,s] in (S -Terms (X,Y)) . s
reconsider t = root-tree [x,s] as Term of S,Y by A8, MSATERM:4;
A9: variables_in t c= X
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or (variables_in t) . i c= X . i )
assume  i in the carrier of S ; ::_thesis: (variables_in t) . i c= X . i
A10: (S variables_in t) . s = {x} by Th10;
 ( i <> s implies (S variables_in t) . i = {} ) by Th10;
hence  (variables_in t) . i c= X . i by A7, A10, XBOOLE_1:2, ZFMISC_1:31; ::_thesis: verum
end;
 the_sort_of t = s by A8, MSATERM:14;
hence  root-tree [x,s] in (S -Terms (X,Y)) . s by A1, A9; ::_thesis: verum
end;

theorem Th19: :: MSAFREE3:19
for S being non void Signature
for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,Y) holds
( (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) iff rng p c= Union (S -Terms (X,Y)) )
proof
let S be non void Signature; ::_thesis: for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,Y) holds
( (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) iff rng p c= Union (S -Terms (X,Y)) )
let Y be V8() ManySortedSet of the carrier of S; ::_thesis: for X being ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,Y) holds
( (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) iff rng p c= Union (S -Terms (X,Y)) )
let X be ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,Y) holds
( (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) iff rng p c= Union (S -Terms (X,Y)) )
let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,Y) holds
( (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) iff rng p c= Union (S -Terms (X,Y)) )
let p be ArgumentSeq of Sym (o,Y); ::_thesis: ( (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) iff rng p c= Union (S -Terms (X,Y)) )
set s = the_result_sort_of o;
A1: dom (S -Terms (X,Y)) = the carrier of S by PARTFUN1:def_2;
A2: Sym (o,Y) = [o, the carrier of S] by MSAFREE:def_9;
A3: (S -Terms (X,Y)) . (the_result_sort_of o) =  {  t where t is Term of S,Y : ( the_sort_of t = the_result_sort_of o & variables_in t c= X )  }  by Def5;
hereby  ::_thesis: ( rng p c= Union (S -Terms (X,Y)) implies (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) )
assume  (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) ; ::_thesis: rng p c= Union (S -Terms (X,Y))
then consider t being Term of S,Y such that
A4: [o, the carrier of S] -tree p = t and
 the_sort_of t = the_result_sort_of o and
A5: variables_in t c= X by A3, A2;
thus  rng p c= Union (S -Terms (X,Y)) ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in Union (S -Terms (X,Y)) )
assume A6: y in rng p ; ::_thesis: y in Union (S -Terms (X,Y))
then consider x being set  such that
A7: x in dom p and
A8: y = p . x by FUNCT_1:def_3;
reconsider x = x as Nat by A7;
reconsider q = p . x as Term of S,Y by A7, MSATERM:22;
A9: variables_in q c= X
proof
let z be set ; :: according to PBOOLE:def_2 ::_thesis: ( not z in the carrier of S or (variables_in q) . z c= X . z )
assume A10: z in the carrier of S ; ::_thesis: (variables_in q) . z c= X . z
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (variables_in q) . z or a in X . z )
assume  a in (variables_in q) . z ; ::_thesis: a in X . z
then A11: a in (variables_in t) . z by A4, A6, A8, A10, Th11;
 (variables_in t) . z c= X . z by A5, A10, PBOOLE:def_2;
hence  a in X . z by A11; ::_thesis: verum
end;
set sq = the_sort_of q;
 (S -Terms (X,Y)) . (the_sort_of q) =  {  t9 where t9 is Term of S,Y : ( the_sort_of t9 = the_sort_of q & variables_in t9 c= X )  }  by Def5;
then  q in (S -Terms (X,Y)) . (the_sort_of q) by A9;
hence  y in Union (S -Terms (X,Y)) by A1, A8, CARD_5:2; ::_thesis: verum
end;
end;
set t = (Sym (o,Y)) -tree p;
assume A12: rng p c= Union (S -Terms (X,Y)) ; ::_thesis: (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o)
A13: variables_in ((Sym (o,Y)) -tree p) c= X
proof
let z be set ; :: according to PBOOLE:def_2 ::_thesis: ( not z in the carrier of S or (variables_in ((Sym (o,Y)) -tree p)) . z c= X . z )
assume A14: z in the carrier of S ; ::_thesis: (variables_in ((Sym (o,Y)) -tree p)) . z c= X . z
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (variables_in ((Sym (o,Y)) -tree p)) . z or x in X . z )
assume  x in (variables_in ((Sym (o,Y)) -tree p)) . z ; ::_thesis: x in X . z
then consider q being DecoratedTree such that
A15: q in rng p and
A16: x in (S variables_in q) . z by A2, A14, Th11;
consider y being set  such that
A17: y in the carrier of S and
A18: q in (S -Terms (X,Y)) . y by A1, A12, A15, CARD_5:2;
 (S -Terms (X,Y)) . y =  {  t9 where t9 is Term of S,Y : ( the_sort_of t9 = y & variables_in t9 c= X )  }  by A17, Def5;
then consider t9 being Term of S,Y such that
A19: q = t9 and
 the_sort_of t9 = y and
A20: variables_in t9 c= X by A18;
 (variables_in t9) . z c= X . z by A14, A20, PBOOLE:def_2;
hence  x in X . z by A16, A19; ::_thesis: verum
end;
 the_sort_of ((Sym (o,Y)) -tree p) = the_result_sort_of o by MSATERM:20;
hence  (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) by A3, A13; ::_thesis: verum
end;

theorem Th20: :: MSAFREE3:20
for S being non void Signature
for X being V8() ManySortedSet of the carrier of S
for A being MSSubset of (FreeMSA X) holds
( A is opers_closed iff for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union A holds
(Sym (o,X)) -tree p in A . (the_result_sort_of o) )
proof
let S be non void Signature; ::_thesis: for X being V8() ManySortedSet of the carrier of S
for A being MSSubset of (FreeMSA X) holds
( A is opers_closed iff for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union A holds
(Sym (o,X)) -tree p in A . (the_result_sort_of o) )
let X be V8() ManySortedSet of the carrier of S; ::_thesis: for A being MSSubset of (FreeMSA X) holds
( A is opers_closed iff for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union A holds
(Sym (o,X)) -tree p in A . (the_result_sort_of o) )
set A = FreeMSA X;
let T be MSSubset of (FreeMSA X); ::_thesis: ( T is opers_closed iff for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds
(Sym (o,X)) -tree p in T . (the_result_sort_of o) )
hereby  ::_thesis: ( ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds
(Sym (o,X)) -tree p in T . (the_result_sort_of o) ) implies T is opers_closed )
assume A1: T is opers_closed ; ::_thesis: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds
(Sym (o,X)) -tree p in T . (the_result_sort_of o)
let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds
(Sym (o,X)) -tree p in T . (the_result_sort_of o)
let p be ArgumentSeq of Sym (o,X); ::_thesis: ( rng p c= Union T implies (Sym (o,X)) -tree p in T . (the_result_sort_of o) )
 T is_closed_on o by A1, MSUALG_2:def_6;
then A2: rng ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) c= (T * the ResultSort of S) . o by MSUALG_2:def_5;
A3: p is Element of Args (o,(FreeMSA X)) by INSTALG1:1;
A4: dom p = dom (the_arity_of o) by MSATERM:22;
A5: dom T = the carrier of S by PARTFUN1:def_2;
assume A6: rng p c= Union T ; ::_thesis: (Sym (o,X)) -tree p in T . (the_result_sort_of o)
A7: now__::_thesis:_for_x_being_set_st_x_in_dom_(the_arity_of_o)_holds_
p_._x_in_(T_*_(the_arity_of_o))_._x
let x be set ; ::_thesis: ( x in dom (the_arity_of o) implies p . x in (T * (the_arity_of o)) . x )
assume A8: x in dom (the_arity_of o) ; ::_thesis: p . x in (T * (the_arity_of o)) . x
then reconsider i = x as Nat ;
reconsider t = p . i as Term of S,X by A4, A8, MSATERM:22;
A9: ( the_sort_of t = (the_arity_of o) . x & (T * (the_arity_of o)) . x = T . ((the_arity_of o) . x) ) by A4, A8, FUNCT_1:13, MSATERM:23;
 p . x in rng p by A4, A8, FUNCT_1:def_3;
then consider y being set  such that
A10: y in dom T and
A11: p . x in T . y by A6, CARD_5:2;
 T c= the Sorts of (FreeMSA X) by PBOOLE:def_18;
then  T . y c= the Sorts of (FreeMSA X) . y by A10, PBOOLE:def_2;
hence  p . x in (T * (the_arity_of o)) . x by A10, A11, A9, Th7; ::_thesis: verum
end;
 rng (the_arity_of o) c= dom T by A5;
then  dom (T * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
then A12: p in product (T * (the_arity_of o)) by A4, A7, CARD_3:9;
A13: ((T #) * the Arity of S) . o = (T #) . ( the Arity of S . o) by FUNCT_2:15
.= (T #) . (the_arity_of o) by MSUALG_1:def_1
.= product (T * (the_arity_of o)) by FINSEQ_2:def_5 ;
then A14: ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) . p = (Den (o,(FreeMSA X))) . p by A12, FUNCT_1:49;
 dom (Den (o,(FreeMSA X))) = Args (o,(FreeMSA X)) by FUNCT_2:def_1;
then  p in dom ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) by A13, A3, A12, RELAT_1:57;
then A15: (Den (o,(FreeMSA X))) . p in rng ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) by A14, FUNCT_1:def_3;
(T * the ResultSort of S) . o = T . ( the ResultSort of S . o) by FUNCT_2:15
.= T . (the_result_sort_of o) by MSUALG_1:def_2 ;
then  ( [o, the carrier of S] = Sym (o,X) & (Den (o,(FreeMSA X))) . p in T . (the_result_sort_of o) ) by A2, A15, MSAFREE:def_9;
hence  (Sym (o,X)) -tree p in T . (the_result_sort_of o) by A3, INSTALG1:3; ::_thesis: verum
end;
assume A16: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st rng p c= Union T holds
(Sym (o,X)) -tree p in T . (the_result_sort_of o) ; ::_thesis: T is opers_closed
let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: T is_closed_on o
let x be set ; :: according to TARSKI:def_3,MSUALG_2:def_5 ::_thesis: ( not x in proj2 ((Den (o,(FreeMSA X))) | (( the Arity of S * (T #)) . o)) or x in ( the ResultSort of S * T) . o )
A17: (T * the ResultSort of S) . o = T . ( the ResultSort of S . o) by FUNCT_2:15
.= T . (the_result_sort_of o) by MSUALG_1:def_2 ;
assume  x in rng ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) ; ::_thesis: x in ( the ResultSort of S * T) . o
then consider y being set  such that
A18: y in dom ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) and
A19: x = ((Den (o,(FreeMSA X))) | (((T #) * the Arity of S) . o)) . y by FUNCT_1:def_3;
 y in dom (Den (o,(FreeMSA X))) by A18, RELAT_1:57;
then reconsider y = y as Element of Args (o,(FreeMSA X)) ;
reconsider p = y as ArgumentSeq of Sym (o,X) by INSTALG1:1;
A20: ((T #) * the Arity of S) . o = (T #) . ( the Arity of S . o) by FUNCT_2:15
.= (T #) . (the_arity_of o) by MSUALG_1:def_1
.= product (T * (the_arity_of o)) by FINSEQ_2:def_5 ;
A21: rng p c= Union T
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng p or z in Union T )
A22: dom T = the carrier of S by PARTFUN1:def_2;
assume  z in rng p ; ::_thesis: z in Union T
then consider a being set  such that
A23: a in dom p and
A24: z = p . a by FUNCT_1:def_3;
A25: dom p = dom (T * (the_arity_of o)) by A18, A20, CARD_3:9;
then A26: ( z in (T * (the_arity_of o)) . a & (T * (the_arity_of o)) . a = T . ((the_arity_of o) . a) ) by A18, A20, A23, A24, CARD_3:9, FUNCT_1:12;
 rng (the_arity_of o) c= the carrier of S ;
then  dom (T * (the_arity_of o)) = dom (the_arity_of o) by A22, RELAT_1:27;
then  (the_arity_of o) . a in rng (the_arity_of o) by A23, A25, FUNCT_1:def_3;
hence  z in Union T by A22, A26, CARD_5:2; ::_thesis: verum
end;
x = (Den (o,(FreeMSA X))) . y by A18, A19, FUNCT_1:47
.= [o, the carrier of S] -tree y by INSTALG1:3
.= (Sym (o,X)) -tree p by MSAFREE:def_9 ;
hence  x in ( the ResultSort of S * T) . o by A16, A17, A21; ::_thesis: verum
end;

theorem Th21: :: MSAFREE3:21
for S being non void Signature
for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S holds S -Terms (X,Y) is opers_closed
proof
let S be non void Signature; ::_thesis: for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S holds S -Terms (X,Y) is opers_closed
let Y be V8() ManySortedSet of the carrier of S; ::_thesis: for X being ManySortedSet of the carrier of S holds S -Terms (X,Y) is opers_closed
let X be ManySortedSet of the carrier of S; ::_thesis: S -Terms (X,Y) is opers_closed
 for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,Y) st rng p c= Union (S -Terms (X,Y)) holds
(Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) by Th19;
hence  S -Terms (X,Y) is opers_closed by Th20; ::_thesis: verum
end;

theorem Th22: :: MSAFREE3:22
for S being non void Signature
for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S holds (Reverse Y) "" X c= S -Terms (X,Y)
proof
let S be non void Signature; ::_thesis: for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S holds (Reverse Y) "" X c= S -Terms (X,Y)
let Y be V8() ManySortedSet of the carrier of S; ::_thesis: for X being ManySortedSet of the carrier of S holds (Reverse Y) "" X c= S -Terms (X,Y)
let X be ManySortedSet of the carrier of S; ::_thesis: (Reverse Y) "" X c= S -Terms (X,Y)
let s be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s in the carrier of S or ((Reverse Y) "" X) . s c= (S -Terms (X,Y)) . s )
assume  s in the carrier of S ; ::_thesis: ((Reverse Y) "" X) . s c= (S -Terms (X,Y)) . s
then reconsider s9 = s as SortSymbol of S ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((Reverse Y) "" X) . s or x in (S -Terms (X,Y)) . s )
assume  x in ((Reverse Y) "" X) . s ; ::_thesis: x in (S -Terms (X,Y)) . s
then A1: x in ((Reverse Y) . s9) " (X . s9) by EQUATION:def_1;
then A2: x in dom ((Reverse Y) . s) by FUNCT_1:def_7;
A3: ((Reverse Y) . s) . x in X . s by A1, FUNCT_1:def_7;
A4: (Reverse Y) . s = Reverse (s9,Y) by MSAFREE:def_18;
then A5: dom ((Reverse Y) . s) = FreeGen (s9,Y) by FUNCT_2:def_1;
then consider b being set  such that
A6: b in Y . s9 and
A7: x = root-tree [b,s9] by A2, MSAFREE:def_15;
 FreeGen (s9,Y) =  {  (root-tree t) where t is Symbol of (DTConMSA Y) : ( t in Terminals (DTConMSA Y) & t `2 = s )  }  by MSAFREE:13;
then consider a being Symbol of (DTConMSA Y) such that
A8: x = root-tree a and
 a in Terminals (DTConMSA Y) and
 a `2 = s by A2, A5;
(Reverse (s9,Y)) . x = a `1 by A2, A5, A8, MSAFREE:def_17
.= [b,s] `1 by A8, A7, TREES_4:4
.= b ;
hence  x in (S -Terms (X,Y)) . s by A3, A4, A6, A7, Th18; ::_thesis: verum
end;

theorem Th23: :: MSAFREE3:23
for S being non void Signature
for X being ManySortedSet of the carrier of S
for t being Term of S,(X \/ ( the carrier of S --> {0}))
for s being SortSymbol of S st t in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s holds
t in the Sorts of (Free (S,X)) . s
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being ManySortedSet of the carrier of S
for t being Term of S,(X \/ ( the carrier of S --> {0}))
for s being SortSymbol of S st t in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s holds
t in the Sorts of (Free (S,X)) . s
let X be ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,(X \/ ( the carrier of S --> {0}))
for s being SortSymbol of S st t in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s holds
t in the Sorts of (Free (S,X)) . s
set Y = X \/ ( the carrier of S --> {0});
set T = the Sorts of (Free (S,X));
defpred S1[ set ] means  for s being SortSymbol of S st $1 in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s holds
$1 in the Sorts of (Free (S,X)) . s;
A1: ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st
( Free (S,X) = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) by Def1;
then reconsider TT = the Sorts of (Free (S,X)) as MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) by MSUALG_2:def_9;
A2: now__::_thesis:_for_o_being_OperSymbol_of_S
for_p_being_ArgumentSeq_of_Sym_(o,(X_\/_(_the_carrier_of_S_-->_{0})))_st_(_for_t_being_Term_of_S,(X_\/_(_the_carrier_of_S_-->_{0}))_st_t_in_rng_p_holds_
S1[t]_)_holds_
S1[[o,_the_carrier_of_S]_-tree_p]
let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,(X \/ ( the carrier of S --> {0}))) st ( for t being Term of S,(X \/ ( the carrier of S --> {0})) st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]
let p be ArgumentSeq of Sym (o,(X \/ ( the carrier of S --> {0}))); ::_thesis: ( ( for t being Term of S,(X \/ ( the carrier of S --> {0})) st t in rng p holds
S1[t] ) implies S1[[o, the carrier of S] -tree p] )
assume A3: for t being Term of S,(X \/ ( the carrier of S --> {0})) st t in rng p holds
S1[t] ; ::_thesis: S1[[o, the carrier of S] -tree p]
thus  S1[[o, the carrier of S] -tree p] ::_thesis: verum
proof
let s be SortSymbol of S; ::_thesis: ( [o, the carrier of S] -tree p in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s implies [o, the carrier of S] -tree p in the Sorts of (Free (S,X)) . s )
assume A4: [o, the carrier of S] -tree p in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s ; ::_thesis: [o, the carrier of S] -tree p in the Sorts of (Free (S,X)) . s
A5: Sym (o,(X \/ ( the carrier of S --> {0}))) = [o, the carrier of S] by MSAFREE:def_9;
 the_sort_of ((Sym (o,(X \/ ( the carrier of S --> {0})))) -tree p) = the_result_sort_of o by MSATERM:20;
then A6: s = the_result_sort_of o by A4, A5, Th17;
then A7: rng p c= Union (S -Terms (X,(X \/ ( the carrier of S --> {0})))) by A4, A5, Th19;
A8: rng p c= Union TT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in Union TT )
assume A9: x in rng p ; ::_thesis: x in Union TT
then consider y being set  such that
A10: y in dom (S -Terms (X,(X \/ ( the carrier of S --> {0})))) and
A11: x in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . y by A7, CARD_5:2;
reconsider y = y as SortSymbol of S by A10;
 (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . y = (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . y ;
then reconsider x = x as Term of S,(X \/ ( the carrier of S --> {0})) by A11, Th16;
 ( dom the Sorts of (Free (S,X)) = the carrier of S & x in the Sorts of (Free (S,X)) . y ) by A3, A9, A11, PARTFUN1:def_2;
hence  x in Union TT by CARD_5:2; ::_thesis: verum
end;
 TT is opers_closed by A1, MSUALG_2:def_9;
hence  [o, the carrier of S] -tree p in the Sorts of (Free (S,X)) . s by A5, A6, A8, Th20; ::_thesis: verum
end;
end;
A12: S -Terms (X,(X \/ ( the carrier of S --> {0}))) c= the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) by PBOOLE:def_18;
A13: now__::_thesis:_for_s1_being_SortSymbol_of_S
for_v_being_Element_of_(X_\/_(_the_carrier_of_S_-->_{0}))_._s1_holds_S1[_root-tree_[v,s1]]
let s1 be SortSymbol of S; ::_thesis: for v being Element of (X \/ ( the carrier of S --> {0})) . s1 holds S1[ root-tree [v,s1]]
let v be Element of (X \/ ( the carrier of S --> {0})) . s1; ::_thesis: S1[ root-tree [v,s1]]
thus  S1[ root-tree [v,s1]] ::_thesis: verum
proof
reconsider t = root-tree [v,s1] as Term of S,(X \/ ( the carrier of S --> {0})) by MSATERM:4;
let s be SortSymbol of S; ::_thesis: ( root-tree [v,s1] in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s implies root-tree [v,s1] in the Sorts of (Free (S,X)) . s )
assume A14: root-tree [v,s1] in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s ; ::_thesis: root-tree [v,s1] in the Sorts of (Free (S,X)) . s
 (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s c= the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) . s by A12, PBOOLE:def_2;
then A15: the_sort_of t = s by A14, Th7;
A16: the_sort_of t = s1 by MSATERM:14;
then  v in X . s by A14, A15, Th18;
hence  root-tree [v,s1] in the Sorts of (Free (S,X)) . s by A15, A16, Th4; ::_thesis: verum
end;
end;
thus  for t being Term of S,(X \/ ( the carrier of S --> {0})) holds S1[t] from MSATERM:sch_1(A13, A2); ::_thesis: verum
end;

theorem Th24: :: MSAFREE3:24
for S being non void Signature
for X being ManySortedSet of the carrier of S holds the Sorts of (Free (S,X)) = S -Terms (X,(X \/ ( the carrier of S --> {0})))
proof
let S be non void Signature; ::_thesis: for X being ManySortedSet of the carrier of S holds the Sorts of (Free (S,X)) = S -Terms (X,(X \/ ( the carrier of S --> {0})))
let X be ManySortedSet of the carrier of S; ::_thesis: the Sorts of (Free (S,X)) = S -Terms (X,(X \/ ( the carrier of S --> {0})))
set Y = X \/ ( the carrier of S --> {0});
set B = MSAlgebra(# (S -Terms (X,(X \/ ( the carrier of S --> {0})))),(Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S -Terms (X,(X \/ ( the carrier of S --> {0})))))) #);
 for Z being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st Z = the Sorts of MSAlgebra(# (S -Terms (X,(X \/ ( the carrier of S --> {0})))),(Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S -Terms (X,(X \/ ( the carrier of S --> {0})))))) #) holds
( Z is opers_closed & the Charact of MSAlgebra(# (S -Terms (X,(X \/ ( the carrier of S --> {0})))),(Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S -Terms (X,(X \/ ( the carrier of S --> {0})))))) #) = Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),Z) ) by Th21;
then reconsider B = MSAlgebra(# (S -Terms (X,(X \/ ( the carrier of S --> {0})))),(Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S -Terms (X,(X \/ ( the carrier of S --> {0})))))) #) as MSSubAlgebra of FreeMSA (X \/ ( the carrier of S --> {0})) by MSUALG_2:def_9;
A1: ( FreeMSA (X \/ ( the carrier of S --> {0})) = MSAlgebra(# (FreeSort (X \/ ( the carrier of S --> {0}))),(FreeOper (X \/ ( the carrier of S --> {0}))) #) & dom (FreeSort (X \/ ( the carrier of S --> {0}))) = the carrier of S ) by MSAFREE:def_14, PARTFUN1:def_2;
 (Reverse (X \/ ( the carrier of S --> {0}))) "" X c= S -Terms (X,(X \/ ( the carrier of S --> {0}))) by Th22;
then A2: (Reverse (X \/ ( the carrier of S --> {0}))) "" X is MSSubset of B by PBOOLE:def_18;
let s be Element of S; :: according to PBOOLE:def_21 ::_thesis: the Sorts of (Free (S,X)) . s = (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s
 ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st
( Free (S,X) = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) by Def1;
then  Free (S,X) is MSSubAlgebra of B by A2, MSUALG_2:def_17;
then  the Sorts of (Free (S,X)) is MSSubset of B by MSUALG_2:def_9;
then  the Sorts of (Free (S,X)) c= S -Terms (X,(X \/ ( the carrier of S --> {0}))) by PBOOLE:def_18;
hence  the Sorts of (Free (S,X)) . s c= (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s by PBOOLE:def_2; :: according to XBOOLE_0:def_10 ::_thesis: (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s c= the Sorts of (Free (S,X)) . s
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s or x in the Sorts of (Free (S,X)) . s )
assume A3: x in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s ; ::_thesis: x in the Sorts of (Free (S,X)) . s
 S -Terms (X,(X \/ ( the carrier of S --> {0}))) c= the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) by PBOOLE:def_18;
then  (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s c= the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) . s by PBOOLE:def_2;
then  x in Union (FreeSort (X \/ ( the carrier of S --> {0}))) by A3, A1, CARD_5:2;
then  x is Term of S,(X \/ ( the carrier of S --> {0})) by MSATERM:13;
hence  x in the Sorts of (Free (S,X)) . s by A3, Th23; ::_thesis: verum
end;

theorem :: MSAFREE3:25
for S being non void Signature
for X being ManySortedSet of the carrier of S holds (FreeMSA (X \/ ( the carrier of S --> {0}))) | (S -Terms (X,(X \/ ( the carrier of S --> {0})))) = Free (S,X)
proof
let S be non void Signature; ::_thesis: for X being ManySortedSet of the carrier of S holds (FreeMSA (X \/ ( the carrier of S --> {0}))) | (S -Terms (X,(X \/ ( the carrier of S --> {0})))) = Free (S,X)
let X be ManySortedSet of the carrier of S; ::_thesis: (FreeMSA (X \/ ( the carrier of S --> {0}))) | (S -Terms (X,(X \/ ( the carrier of S --> {0})))) = Free (S,X)
set Y = X \/ ( the carrier of S --> {0});
 ( (FreeMSA (X \/ ( the carrier of S --> {0}))) | (S -Terms (X,(X \/ ( the carrier of S --> {0})))) = MSAlgebra(# (S -Terms (X,(X \/ ( the carrier of S --> {0})))),(Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S -Terms (X,(X \/ ( the carrier of S --> {0})))))) #) & ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st
( Free (S,X) = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) ) by Def1, Th21, MSUALG_2:def_15;
hence  (FreeMSA (X \/ ( the carrier of S --> {0}))) | (S -Terms (X,(X \/ ( the carrier of S --> {0})))) = Free (S,X) by Th24, MSUALG_2:9; ::_thesis: verum
end;

theorem Th26: :: MSAFREE3:26
for S being non void Signature
for X, Y being V8() ManySortedSet of the carrier of S
for A being MSSubAlgebra of FreeMSA X
for B being MSSubAlgebra of FreeMSA Y st the Sorts of A = the Sorts of B holds
MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)
proof
let S be non void Signature; ::_thesis: for X, Y being V8() ManySortedSet of the carrier of S
for A being MSSubAlgebra of FreeMSA X
for B being MSSubAlgebra of FreeMSA Y st the Sorts of A = the Sorts of B holds
MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)
let X, Y be V8() ManySortedSet of the carrier of S; ::_thesis: for A being MSSubAlgebra of FreeMSA X
for B being MSSubAlgebra of FreeMSA Y st the Sorts of A = the Sorts of B holds
MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)
let A be MSSubAlgebra of FreeMSA X; ::_thesis: for B being MSSubAlgebra of FreeMSA Y st the Sorts of A = the Sorts of B holds
MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)
let B be MSSubAlgebra of FreeMSA Y; ::_thesis: ( the Sorts of A = the Sorts of B implies MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) )
assume A1: the Sorts of A = the Sorts of B ; ::_thesis: MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)
reconsider SB = the Sorts of B as MSSubset of (FreeMSA Y) by MSUALG_2:def_9;
reconsider SA = the Sorts of A as MSSubset of (FreeMSA X) by MSUALG_2:def_9;
A2: SA is opers_closed by MSUALG_2:def_9;
A3: SB is opers_closed by MSUALG_2:def_9;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier'_of_S_holds_
the_Charact_of_A_._x_=_the_Charact_of_B_._x
let x be set ; ::_thesis: ( x in the carrier' of S implies the Charact of A . x = the Charact of B . x )
A4: ( SA c= the Sorts of (FreeMSA X) & the Sorts of (FreeMSA X) is MSSubset of (FreeMSA X) ) by PBOOLE:def_18;
assume  x in the carrier' of S ; ::_thesis: the Charact of A . x = the Charact of B . x
then reconsider o = x as OperSymbol of S ;
A5: SA is_closed_on o by A2, MSUALG_2:def_6;
A6: the Charact of A . o = (Opers ((FreeMSA X),SA)) . o by MSUALG_2:def_9
.= o /. SA by MSUALG_2:def_8
.= (Den (o,(FreeMSA X))) | (((SA #) * the Arity of S) . o) by A5, MSUALG_2:def_7 ;
 Args (o,(FreeMSA X)) = (( the Sorts of (FreeMSA X) #) * the Arity of S) . o by MSUALG_1:def_4;
then  dom (Den (o,(FreeMSA X))) = (( the Sorts of (FreeMSA X) #) * the Arity of S) . o by FUNCT_2:def_1;
then A7: dom ( the Charact of A . o) = ((SA #) * the Arity of S) . o by A6, A4, MSUALG_2:2, RELAT_1:62;
A8: ( SB c= the Sorts of (FreeMSA Y) & the Sorts of (FreeMSA Y) is MSSubset of (FreeMSA Y) ) by PBOOLE:def_18;
then A9: ((SB #) * the Arity of S) . o c= (( the Sorts of (FreeMSA Y) #) * the Arity of S) . o by MSUALG_2:2;
A10: SB is_closed_on o by A3, MSUALG_2:def_6;
A11: the Charact of B . o = (Opers ((FreeMSA Y),SB)) . o by MSUALG_2:def_9
.= o /. SB by MSUALG_2:def_8
.= (Den (o,(FreeMSA Y))) | (((SB #) * the Arity of S) . o) by A10, MSUALG_2:def_7 ;
 Args (o,(FreeMSA Y)) = (( the Sorts of (FreeMSA Y) #) * the Arity of S) . o by MSUALG_1:def_4;
then  dom (Den (o,(FreeMSA Y))) = (( the Sorts of (FreeMSA Y) #) * the Arity of S) . o by FUNCT_2:def_1;
then A12: dom ( the Charact of B . o) = ((SB #) * the Arity of S) . o by A11, A8, MSUALG_2:2, RELAT_1:62;
A13: ((SA #) * the Arity of S) . o c= (( the Sorts of (FreeMSA X) #) * the Arity of S) . o by A4, MSUALG_2:2;
now__::_thesis:_for_x_being_set_st_x_in_((SA_#)_*_the_Arity_of_S)_._o_holds_
(_the_Charact_of_A_._o)_._x_=_(_the_Charact_of_B_._o)_._x
let x be set ; ::_thesis: ( x in ((SA #) * the Arity of S) . o implies ( the Charact of A . o) . x = ( the Charact of B . o) . x )
assume A14: x in ((SA #) * the Arity of S) . o ; ::_thesis: ( the Charact of A . o) . x = ( the Charact of B . o) . x
then reconsider p1 = x as Element of Args (o,(FreeMSA X)) by A13, MSUALG_1:def_4;
reconsider p2 = x as Element of Args (o,(FreeMSA Y)) by A1, A9, A14, MSUALG_1:def_4;
thus ( the Charact of A . o) . x = (Den (o,(FreeMSA X))) . p1 by A6, A7, A14, FUNCT_1:47
.= [o, the carrier of S] -tree p1 by INSTALG1:3
.= (Den (o,(FreeMSA Y))) . p2 by INSTALG1:3
.= ( the Charact of B . o) . x by A1, A11, A12, A14, FUNCT_1:47 ; ::_thesis: verum
end;
hence  the Charact of A . x = the Charact of B . x by A1, A7, A12, FUNCT_1:2; ::_thesis: verum
end;
hence  MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) by A1, PBOOLE:3; ::_thesis: verum
end;

theorem Th27: :: MSAFREE3:27
for S being non void Signature
for X being V9() ManySortedSet of the carrier of S
for Y being ManySortedSet of the carrier of S
for t being Element of (Free (S,X)) holds S variables_in t c= X
proof
let S be non void Signature; ::_thesis: for X being V9() ManySortedSet of the carrier of S
for Y being ManySortedSet of the carrier of S
for t being Element of (Free (S,X)) holds S variables_in t c= X
let X be V9() ManySortedSet of the carrier of S; ::_thesis: for Y being ManySortedSet of the carrier of S
for t being Element of (Free (S,X)) holds S variables_in t c= X
let Y be ManySortedSet of the carrier of S; ::_thesis: for t being Element of (Free (S,X)) holds S variables_in t c= X
let t be Element of (Free (S,X)); ::_thesis: S variables_in t c= X
set Z = X \/ ( the carrier of S --> {0});
reconsider t = t as Term of S,(X \/ ( the carrier of S --> {0})) by Th8;
 t in Union the Sorts of (Free (S,X)) ;
then A1: t in Union (S -Terms (X,(X \/ ( the carrier of S --> {0})))) by Th24;
 dom (S -Terms (X,(X \/ ( the carrier of S --> {0})))) = the carrier of S by PARTFUN1:def_2;
then  ex s being set st
( s in the carrier of S & t in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . s ) by A1, CARD_5:2;
then  variables_in t c= X by Th17;
hence  S variables_in t c= X ; ::_thesis: verum
end;

theorem Th28: :: MSAFREE3:28
for S being non void Signature
for X being V8() ManySortedSet of the carrier of S
for t being Term of S,X holds variables_in t c= X
proof
let S be non void Signature; ::_thesis: for X being V8() ManySortedSet of the carrier of S
for t being Term of S,X holds variables_in t c= X
let X be V8() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,X holds variables_in t c= X
defpred S1[ DecoratedTree] means S variables_in $1 c= X;
let t be Term of S,X; ::_thesis: variables_in t c= X
A1: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st ( for t being Term of S,X st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]
proof
let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,X) st ( for t being Term of S,X st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]
let p be ArgumentSeq of Sym (o,X); ::_thesis: ( ( for t being Term of S,X st t in rng p holds
S1[t] ) implies S1[[o, the carrier of S] -tree p] )
assume A2: for t being Term of S,X st t in rng p holds
S variables_in t c= X ; ::_thesis: S1[[o, the carrier of S] -tree p]
thus  S variables_in ([o, the carrier of S] -tree p) c= X ::_thesis: verum
proof
let s be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s in the carrier of S or (S variables_in ([o, the carrier of S] -tree p)) . s c= X . s )
assume A3: s in the carrier of S ; ::_thesis: (S variables_in ([o, the carrier of S] -tree p)) . s c= X . s
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (S variables_in ([o, the carrier of S] -tree p)) . s or x in X . s )
assume  x in (S variables_in ([o, the carrier of S] -tree p)) . s ; ::_thesis: x in X . s
then consider t being DecoratedTree such that
A4: t in rng p and
A5: x in (S variables_in t) . s by A3, Th11;
consider i being set  such that
A6: i in dom p and
A7: t = p . i by A4, FUNCT_1:def_3;
reconsider i = i as Nat by A6;
reconsider t = p . i as Term of S,X by A6, MSATERM:22;
 S variables_in t c= X by A2, A4, A7;
then  (S variables_in t) . s c= X . s by A3, PBOOLE:def_2;
hence  x in X . s by A5, A7; ::_thesis: verum
end;
end;
A8: for s being SortSymbol of S
for v being Element of X . s holds S1[ root-tree [v,s]]
proof
let s be SortSymbol of S; ::_thesis: for v being Element of X . s holds S1[ root-tree [v,s]]
let x be Element of X . s; ::_thesis: S1[ root-tree [x,s]]
thus  S variables_in (root-tree [x,s]) c= X ::_thesis: verum
proof
let y be set ; :: according to PBOOLE:def_2 ::_thesis: ( not y in the carrier of S or (S variables_in (root-tree [x,s])) . y c= X . y )
assume  y in the carrier of S ; ::_thesis: (S variables_in (root-tree [x,s])) . y c= X . y
A9: ( y <> s implies (S variables_in (root-tree [x,s])) . y = {} ) by Th10;
 (S variables_in (root-tree [x,s])) . s = {x} by Th10;
hence  (S variables_in (root-tree [x,s])) . y c= X . y by A9, XBOOLE_1:2; ::_thesis: verum
end;
end;
 for t being Term of S,X holds S1[t] from MSATERM:sch_1(A8, A1);
hence  variables_in t c= X ; ::_thesis: verum
end;

theorem Th29: :: MSAFREE3:29
for S being non void Signature
for X, Y being V8() ManySortedSet of the carrier of S
for t1 being Term of S,X
for t2 being Term of S,Y st t1 = t2 holds
the_sort_of t1 = the_sort_of t2
proof
let S be non void Signature; ::_thesis: for X, Y being V8() ManySortedSet of the carrier of S
for t1 being Term of S,X
for t2 being Term of S,Y st t1 = t2 holds
the_sort_of t1 = the_sort_of t2
let X, Y be V8() ManySortedSet of the carrier of S; ::_thesis: for t1 being Term of S,X
for t2 being Term of S,Y st t1 = t2 holds
the_sort_of t1 = the_sort_of t2
let t1 be Term of S,X; ::_thesis: for t2 being Term of S,Y st t1 = t2 holds
the_sort_of t1 = the_sort_of t2
let t2 be Term of S,Y; ::_thesis: ( t1 = t2 implies the_sort_of t1 = the_sort_of t2 )
assume A1: t1 = t2 ; ::_thesis: the_sort_of t1 = the_sort_of t2
percases ( ex s being SortSymbol of S ex v being Element of X . s st t1 . {} = [v,s] or t1 . {} in [: the carrier' of S,{ the carrier of S}:] ) by MSATERM:2;
suppose ex s being SortSymbol of S ex v being Element of X . s st t1 . {} = [v,s] ; ::_thesis: the_sort_of t1 = the_sort_of t2
then consider s being SortSymbol of S, x being Element of X . s such that
A2: t1 . {} = [x,s] ;
 s in the carrier of S ;
then  s <> the carrier of S ;
then  not s in { the carrier of S} by TARSKI:def_1;
then  not [x,s] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87;
then consider s9 being SortSymbol of S, y being Element of Y . s9 such that
A3: t2 . {} = [y,s9] by A1, A2, MSATERM:2;
 t1 = root-tree [x,s] by A2, MSATERM:5;
then A4: the_sort_of t1 = s by MSATERM:14;
 t2 = root-tree [y,s9] by A3, MSATERM:5;
then  the_sort_of t2 = s9 by MSATERM:14;
hence  the_sort_of t1 = the_sort_of t2 by A1, A2, A3, A4, XTUPLE_0:1; ::_thesis: verum
end;
suppose t1 . {} in [: the carrier' of S,{ the carrier of S}:] ; ::_thesis: the_sort_of t1 = the_sort_of t2
then consider o, z being set  such that
A5: o in the carrier' of S and
A6: z in { the carrier of S} and
A7: t1 . {} = [o,z] by ZFMISC_1:def_2;
reconsider o = o as OperSymbol of S by A5;
A8: z = the carrier of S by A6, TARSKI:def_1;
then  the_sort_of t1 = the_result_sort_of o by A7, MSATERM:17;
hence  the_sort_of t1 = the_sort_of t2 by A1, A7, A8, MSATERM:17; ::_thesis: verum
end;
end;
end;

theorem Th30: :: MSAFREE3:30
for S being non void Signature
for X, Y being V8() ManySortedSet of the carrier of S
for t being Term of S,Y st variables_in t c= X holds
t is Term of S,X
proof
let S be non void Signature; ::_thesis: for X, Y being V8() ManySortedSet of the carrier of S
for t being Term of S,Y st variables_in t c= X holds
t is Term of S,X
let X, Y be V8() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,Y st variables_in t c= X holds
t is Term of S,X
defpred S1[ DecoratedTree] means ( Y variables_in $1 c= X implies $1 is Term of S,X );
let t be Term of S,Y; ::_thesis: ( variables_in t c= X implies t is Term of S,X )
A1: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,Y) st ( for t being Term of S,Y st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]
proof
let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,Y) st ( for t being Term of S,Y st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]
let p be ArgumentSeq of Sym (o,Y); ::_thesis: ( ( for t being Term of S,Y st t in rng p holds
S1[t] ) implies S1[[o, the carrier of S] -tree p] )
assume that
A2: for t being Term of S,Y st t in rng p & Y variables_in t c= X holds
t is Term of S,X and
A3: Y variables_in ([o, the carrier of S] -tree p) c= X ; ::_thesis: [o, the carrier of S] -tree p is Term of S,X
A4: now__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_
ex_t9_being_Term_of_S,X_st_
(_t9_=_p_._i_&_the_sort_of_t9_=_(the_arity_of_o)_._i_)
let i be Nat; ::_thesis: ( i in dom p implies ex t9 being Term of S,X st
( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i ) )
assume A5: i in dom p ; ::_thesis: ex t9 being Term of S,X st
( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i )
then reconsider t = p . i as Term of S,Y by MSATERM:22;
A6: t in rng p by A5, FUNCT_1:def_3;
 Y variables_in t c= X
proof
let y be set ; :: according to PBOOLE:def_2 ::_thesis: ( not y in the carrier of S or (Y variables_in t) . y c= X . y )
assume  y in the carrier of S ; ::_thesis: (Y variables_in t) . y c= X . y
then reconsider s = y as SortSymbol of S ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Y variables_in t) . y or x in X . y )
assume  x in (Y variables_in t) . y ; ::_thesis: x in X . y
then A7: x in (Y variables_in ([o, the carrier of S] -tree p)) . s by A6, Th13;
 (Y variables_in ([o, the carrier of S] -tree p)) . s c= X . s by A3, PBOOLE:def_2;
hence  x in X . y by A7; ::_thesis: verum
end;
then reconsider t9 = t as Term of S,X by A2, A6;
take t9 = t9; ::_thesis: ( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i )
thus  t9 = p . i ; ::_thesis: the_sort_of t9 = (the_arity_of o) . i
 the_sort_of t = (the_arity_of o) . i by A5, MSATERM:23;
hence  the_sort_of t9 = (the_arity_of o) . i by Th29; ::_thesis: verum
end;
 len p = len (the_arity_of o) by MSATERM:22;
then reconsider p = p as ArgumentSeq of Sym (o,X) by A4, MSATERM:24;
 (Sym (o,X)) -tree p is Term of S,X ;
hence  [o, the carrier of S] -tree p is Term of S,X by MSAFREE:def_9; ::_thesis: verum
end;
assume  variables_in t c= X ; ::_thesis: t is Term of S,X
then A8: Y variables_in t c= X by Th15;
A9: for s being SortSymbol of S
for x being Element of Y . s holds S1[ root-tree [x,s]]
proof
let s be SortSymbol of S; ::_thesis: for x being Element of Y . s holds S1[ root-tree [x,s]]
let x be Element of Y . s; ::_thesis: S1[ root-tree [x,s]]
assume  Y variables_in (root-tree [x,s]) c= X ; ::_thesis: root-tree [x,s] is Term of S,X
then A10: (Y variables_in (root-tree [x,s])) . s c= X . s by PBOOLE:def_2;
 (Y variables_in (root-tree [x,s])) . s = {x} by Th12;
then  x in X . s by A10, ZFMISC_1:31;
hence  root-tree [x,s] is Term of S,X by MSATERM:4; ::_thesis: verum
end;
 for t being Term of S,Y holds S1[t] from MSATERM:sch_1(A9, A1);
hence  t is Term of S,X by A8; ::_thesis: verum
end;

theorem :: MSAFREE3:31
for S being non void Signature
for X being V8() ManySortedSet of the carrier of S holds Free (S,X) = FreeMSA X
proof
let S be non void Signature; ::_thesis: for X being V8() ManySortedSet of the carrier of S holds Free (S,X) = FreeMSA X
let X be V8() ManySortedSet of the carrier of S; ::_thesis: Free (S,X) = FreeMSA X
set Y = X \/ ( the carrier of S --> {0});
A1: the Sorts of (Free (S,X)) = S -Terms (X,(X \/ ( the carrier of S --> {0}))) by Th24;
A2: FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def_14;
A3: the Sorts of (Free (S,X)) = the Sorts of (FreeMSA X)
proof
let s be Element of S; :: according to PBOOLE:def_21 ::_thesis: the Sorts of (Free (S,X)) . s = the Sorts of (FreeMSA X) . s
reconsider s9 = s as SortSymbol of S ;
thus  the Sorts of (Free (S,X)) . s c= the Sorts of (FreeMSA X) . s :: according to XBOOLE_0:def_10 ::_thesis: the Sorts of (FreeMSA X) . s c= the Sorts of (Free (S,X)) . s
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Sorts of (Free (S,X)) . s or x in the Sorts of (FreeMSA X) . s )
assume A4: x in the Sorts of (Free (S,X)) . s ; ::_thesis: x in the Sorts of (FreeMSA X) . s
then reconsider t = x as Term of S,(X \/ ( the carrier of S --> {0})) by A1, Th16;
 variables_in t c= X by A1, A4, Th17;
then reconsider t9 = t as Term of S,X by Th30;
 the_sort_of t = s by A1, A4, Th17;
then  the_sort_of t9 = s by Th29;
then  x in FreeSort (X,s9) by MSATERM:def_5;
hence  x in the Sorts of (FreeMSA X) . s by A2, MSAFREE:def_11; ::_thesis: verum
end;
reconsider s9 = s as SortSymbol of S ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Sorts of (FreeMSA X) . s or x in the Sorts of (Free (S,X)) . s )
assume  x in the Sorts of (FreeMSA X) . s ; ::_thesis: x in the Sorts of (Free (S,X)) . s
then A5: x in FreeSort (X,s9) by A2, MSAFREE:def_11;
 FreeSort (X,s9) c= S -Terms X by MSATERM:12;
then reconsider t = x as Term of S,X by A5;
 X c= X \/ ( the carrier of S --> {0}) by PBOOLE:14;
then reconsider t9 = t as Term of S,(X \/ ( the carrier of S --> {0})) by MSATERM:26;
 variables_in t = S variables_in t ;
then A6: variables_in t9 c= X by Th28;
 the_sort_of t = s by A5, MSATERM:def_5;
then  the_sort_of t9 = s by Th29;
then  t in  {  q where q is Term of S,(X \/ ( the carrier of S --> {0})) : ( the_sort_of q = s9 & variables_in q c= X )  }  by A6;
hence  x in the Sorts of (Free (S,X)) . s by A1, Def5; ::_thesis: verum
end;
 ( FreeMSA X is MSSubAlgebra of FreeMSA X & ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st
( Free (S,X) = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) ) by Def1, MSUALG_2:5;
hence  Free (S,X) = FreeMSA X by A3, Th26; ::_thesis: verum
end;

theorem Th32: :: MSAFREE3:32
for S being non void Signature
for Y being V8() ManySortedSet of the carrier of S
for t being Term of S,Y
for p being Element of dom t holds variables_in (t | p) c= variables_in t
proof
let S be non void Signature; ::_thesis: for Y being V8() ManySortedSet of the carrier of S
for t being Term of S,Y
for p being Element of dom t holds variables_in (t | p) c= variables_in t
let Y be V8() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,Y
for p being Element of dom t holds variables_in (t | p) c= variables_in t
let t be Term of S,Y; ::_thesis: for p being Element of dom t holds variables_in (t | p) c= variables_in t
let p be Element of dom t; ::_thesis: variables_in (t | p) c= variables_in t
reconsider q = t | p as Term of S,Y ;
let s be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s in the carrier of S or (variables_in (t | p)) . s c= (variables_in t) . s )
assume A1: s in the carrier of S ; ::_thesis: (variables_in (t | p)) . s c= (variables_in t) . s
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (variables_in (t | p)) . s or x in (variables_in t) . s )
assume  x in (variables_in (t | p)) . s ; ::_thesis: x in (variables_in t) . s
then  x in  {  (a `1) where a is Element of rng q : a `2 = s  }  by A1, Def2;
then consider a being Element of rng (t | p) such that
A2: ( x = a `1 & a `2 = s ) ;
 ( rng (t | p) c= rng t & a in rng (t | p) ) by TREES_2:32;
then  x in  {  (b `1) where b is Element of rng t : b `2 = s  }  by A2;
hence  x in (variables_in t) . s by A1, Def2; ::_thesis: verum
end;

theorem Th33: :: MSAFREE3:33
for S being non void Signature
for X being V9() ManySortedSet of the carrier of S
for t being Element of (Free (S,X))
for p being Element of dom t holds t | p is Element of (Free (S,X))
proof
let S be non void Signature; ::_thesis: for X being V9() ManySortedSet of the carrier of S
for t being Element of (Free (S,X))
for p being Element of dom t holds t | p is Element of (Free (S,X))
let X be V9() ManySortedSet of the carrier of S; ::_thesis: for t being Element of (Free (S,X))
for p being Element of dom t holds t | p is Element of (Free (S,X))
let t be Element of (Free (S,X)); ::_thesis: for p being Element of dom t holds t | p is Element of (Free (S,X))
let p be Element of dom t; ::_thesis: t | p is Element of (Free (S,X))
set Y = X \/ ( the carrier of S --> {0});
reconsider t = t as Term of S,(X \/ ( the carrier of S --> {0})) by Th8;
reconsider p = p as Element of dom t ;
A1: variables_in (t | p) c= variables_in t by Th32;
A2: ( the Sorts of (Free (S,X)) = S -Terms (X,(X \/ ( the carrier of S --> {0}))) & dom (S -Terms (X,(X \/ ( the carrier of S --> {0})))) = the carrier of S ) by Th24, PARTFUN1:def_2;
then  ex x being set st
( x in the carrier of S & t in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . x ) by CARD_5:2;
then  variables_in t c= X by Th17;
then  variables_in (t | p) c= X by A1, PBOOLE:13;
then  t | p in  {  q where q is Term of S,(X \/ ( the carrier of S --> {0})) : ( the_sort_of q = the_sort_of (t | p) & variables_in q c= X )  }  ;
then  t | p in (S -Terms (X,(X \/ ( the carrier of S --> {0})))) . (the_sort_of (t | p)) by Def5;
hence  t | p is Element of (Free (S,X)) by A2, CARD_5:2; ::_thesis: verum
end;

theorem Th34: :: MSAFREE3:34
for S being non void Signature
for X being V8() ManySortedSet of the carrier of S
for t being Term of S,X
for a being Element of rng t holds a = [(a `1),(a `2)]
proof
let S be non void Signature; ::_thesis: for X being V8() ManySortedSet of the carrier of S
for t being Term of S,X
for a being Element of rng t holds a = [(a `1),(a `2)]
let X be V8() ManySortedSet of the carrier of S; ::_thesis: for t being Term of S,X
for a being Element of rng t holds a = [(a `1),(a `2)]
let t be Term of S,X; ::_thesis: for a being Element of rng t holds a = [(a `1),(a `2)]
let a be Element of rng t; ::_thesis: a = [(a `1),(a `2)]
consider x being set  such that
A1: x in dom t and
A2: a = t . x by FUNCT_1:def_3;
reconsider x = x as Element of dom t by A1;
 a = (t | x) . {} by A2, TREES_9:35;
then  ( ex s being SortSymbol of S ex v being Element of X . s st a = [v,s] or a in [: the carrier' of S,{ the carrier of S}:] ) by MSATERM:2;
hence  a = [(a `1),(a `2)] by MCART_1:21; ::_thesis: verum
end;

theorem :: MSAFREE3:35
for x being set
for S being non void Signature
for X being V9() ManySortedSet of the carrier of S
for t being Element of (Free (S,X))
for s being SortSymbol of S holds
( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )
proof
let x be set ; ::_thesis: for S being non void Signature
for X being V9() ManySortedSet of the carrier of S
for t being Element of (Free (S,X))
for s being SortSymbol of S holds
( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )
let S be non void Signature; ::_thesis: for X being V9() ManySortedSet of the carrier of S
for t being Element of (Free (S,X))
for s being SortSymbol of S holds
( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )
let X be V9() ManySortedSet of the carrier of S; ::_thesis: for t being Element of (Free (S,X))
for s being SortSymbol of S holds
( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )
let t be Element of (Free (S,X)); ::_thesis: for s being SortSymbol of S holds
( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )
let s be SortSymbol of S; ::_thesis: ( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )
set Y = X \/ ( the carrier of S --> {0});
hereby  ::_thesis: ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) )
assume  x in (S variables_in t) . s ; ::_thesis: [x,s] in rng t
then  x in  {  (a `1) where a is Element of rng t : a `2 = s  }  by Def2;
then consider a being Element of rng t such that
A1: ( x = a `1 & a `2 = s ) ;
 ( t is Term of S,(X \/ ( the carrier of S --> {0})) & a in rng t ) by Th8;
hence  [x,s] in rng t by A1, Th34; ::_thesis: verum
end;
assume A2: [x,s] in rng t ; ::_thesis: ( x in (S variables_in t) . s & x in X . s )
then consider z being set  such that
A3: z in dom t and
A4: [x,s] = t . z by FUNCT_1:def_3;
reconsider z = z as Element of dom t by A3;
reconsider q = t | z as Element of (Free (S,X)) by Th33;
A5: [x,s] = q . {} by A4, TREES_9:35;
 ( [x,s] `1 = x & [x,s] `2 = s ) ;
then A6: x in  {  (a `1) where a is Element of rng t : a `2 = s  }  by A2;
A7: q is Term of S,(X \/ ( the carrier of S --> {0})) by Th8;
 s in the carrier of S ;
then  s <> the carrier of S ;
then  not s in { the carrier of S} by TARSKI:def_1;
then  not [x,s] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87;
then consider s9 being SortSymbol of S, v being Element of (X \/ ( the carrier of S --> {0})) . s9 such that
A8: [x,s] = [v,s9] by A5, A7, MSATERM:2;
 S variables_in q c= X by Th27;
then A9: (S variables_in q) . s9 c= X . s9 by PBOOLE:def_2;
 q = root-tree [v,s9] by A5, A7, A8, MSATERM:5;
then  (S variables_in q) . s9 = {v} by Th10;
then A10: v in X . s9 by A9, ZFMISC_1:31;
 x = v by A8, XTUPLE_0:1;
hence  ( x in (S variables_in t) . s & x in X . s ) by A8, A10, A6, Def2, XTUPLE_0:1; ::_thesis: verum
end;

theorem :: MSAFREE3:36
for S being non void Signature
for X being ManySortedSet of the carrier of S st ( for s being SortSymbol of S st X . s = {} holds
ex o being OperSymbol of S st
( the_result_sort_of o = s & the_arity_of o = {} ) ) holds
Free (S,X) is non-empty
proof
let C be non void Signature; ::_thesis: for X being ManySortedSet of the carrier of C st ( for s being SortSymbol of C st X . s = {} holds
ex o being OperSymbol of C st
( the_result_sort_of o = s & the_arity_of o = {} ) ) holds
Free (C,X) is non-empty
let X be ManySortedSet of the carrier of C; ::_thesis: ( ( for s being SortSymbol of C st X . s = {} holds
ex o being OperSymbol of C st
( the_result_sort_of o = s & the_arity_of o = {} ) ) implies Free (C,X) is non-empty )
assume A1: for s being SortSymbol of C st X . s = {} holds
ex o being OperSymbol of C st
( the_result_sort_of o = s & the_arity_of o = {} ) ; ::_thesis: Free (C,X) is non-empty
now__::_thesis:_not_{}_in_rng_the_Sorts_of_(Free_(C,X))
assume  {} in rng the Sorts of (Free (C,X)) ; ::_thesis: contradiction
then consider s being set  such that
A2: s in dom the Sorts of (Free (C,X)) and
A3: {} = the Sorts of (Free (C,X)) . s by FUNCT_1:def_3;
reconsider s = s as SortSymbol of C by A2;
set x = the Element of X . s;
percases ( X . s = {} or X . s <> {} ) ;
suppose X . s = {} ; ::_thesis: contradiction
then  ex m being OperSymbol of C st
( the_result_sort_of m = s & the_arity_of m = {} ) by A1;
hence  contradiction by A3, Th5; ::_thesis: verum
end;
suppose X . s <> {} ; ::_thesis: contradiction
then  root-tree [ the Element of X . s,s] in the Sorts of (Free (C,X)) . s by Th4;
hence  contradiction by A3; ::_thesis: verum
end;
end;
end;
then  the Sorts of (Free (C,X)) is V8() by RELAT_1:def_9;
hence  Free (C,X) is non-empty by MSUALG_1:def_3; ::_thesis: verum
end;

theorem Th37: :: MSAFREE3:37
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for B being MSSubAlgebra of A
for o being OperSymbol of S holds Args (o,B) c= Args (o,A)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra over S
for B being MSSubAlgebra of A
for o being OperSymbol of S holds Args (o,B) c= Args (o,A)
let A be MSAlgebra over S; ::_thesis: for B being MSSubAlgebra of A
for o being OperSymbol of S holds Args (o,B) c= Args (o,A)
let B be MSSubAlgebra of A; ::_thesis: for o being OperSymbol of S holds Args (o,B) c= Args (o,A)
reconsider SB = the Sorts of B as MSSubset of A by MSUALG_2:def_9;
let o be OperSymbol of S; ::_thesis: Args (o,B) c= Args (o,A)
reconsider SA = the Sorts of A as MSSubset of A by PBOOLE:def_18;
A1: Args (o,B) = ((SB #) * the Arity of S) . o by MSUALG_1:def_4;
 ( SB c= SA & Args (o,A) = ((SA #) * the Arity of S) . o ) by MSUALG_1:def_4, PBOOLE:def_18;
hence  Args (o,B) c= Args (o,A) by A1, MSUALG_2:2; ::_thesis: verum
end;

theorem Th38: :: MSAFREE3:38
for S being non void Signature
for A being feasible MSAlgebra over S
for B being MSSubAlgebra of A holds B is feasible
proof
let S be non void Signature; ::_thesis: for A being feasible MSAlgebra over S
for B being MSSubAlgebra of A holds B is feasible
let A be feasible MSAlgebra over S; ::_thesis: for B being MSSubAlgebra of A holds B is feasible
let B be MSSubAlgebra of A; ::_thesis: B is feasible
reconsider SB = the Sorts of B as MSSubset of A by MSUALG_2:def_9;
let o be OperSymbol of S; :: according to MSUALG_6:def_1 ::_thesis: ( Args (o,B) = {} or not Result (o,B) = {} )
set a = the Element of Args (o,B);
assume  Args (o,B) <> {} ; ::_thesis: not Result (o,B) = {}
then A1: the Element of Args (o,B) in Args (o,B) ;
A2: Args (o,B) c= Args (o,A) by Th37;
then  Result (o,A) <> {} by A1, MSUALG_6:def_1;
then  dom (Den (o,A)) = Args (o,A) by FUNCT_2:def_1;
then  the Element of Args (o,B) in dom ((Den (o,A)) | (Args (o,B))) by A1, A2, RELAT_1:57;
then A3: ( Result (o,B) = (SB * the ResultSort of S) . o & ((Den (o,A)) | (Args (o,B))) . the Element of Args (o,B) in rng ((Den (o,A)) | (Args (o,B))) ) by FUNCT_1:def_3, MSUALG_1:def_5;
 SB is opers_closed by MSUALG_2:def_9;
then  SB is_closed_on o by MSUALG_2:def_6;
then  rng ((Den (o,A)) | (((SB #) * the Arity of S) . o)) c= (SB * the ResultSort of S) . o by MSUALG_2:def_5;
hence  not Result (o,B) = {} by A3, MSUALG_1:def_4; ::_thesis: verum
end;

registration
let S be non void Signature;
let A be feasible MSAlgebra over S;
cluster  ->  feasible for MSSubAlgebra of A;
coherence
 for b1 being MSSubAlgebra of A holds b1 is feasible by Th38;
end;

theorem Th39: :: MSAFREE3:39
for S being non void Signature
for X being ManySortedSet of the carrier of S holds
( Free (S,X) is feasible & Free (S,X) is free )
proof
let S be non void Signature; ::_thesis: for X being ManySortedSet of the carrier of S holds
( Free (S,X) is feasible & Free (S,X) is free )
let X be ManySortedSet of the carrier of S; ::_thesis: ( Free (S,X) is feasible & Free (S,X) is free )
set Y = X \/ ( the carrier of S --> {0});
consider A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) such that
A1: Free (S,X) = GenMSAlg A and
A2: A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X by Def1;
thus  Free (S,X) is feasible by A1; ::_thesis: Free (S,X) is free
 A is ManySortedSubset of FreeGen (X \/ ( the carrier of S --> {0})) by A2, EQUATION:8;
then  A c= FreeGen (X \/ ( the carrier of S --> {0})) by PBOOLE:def_18;
hence  Free (S,X) is free by A1, EQUATION:28; ::_thesis: verum
end;

registration
let S be non void Signature;
let X be ManySortedSet of the carrier of S;
cluster Free (S,X) ->  strict free feasible ;
coherence
 ( Free (S,X) is feasible & Free (S,X) is free ) by Th39;
end;