:: MSAFREE1 semantic presentation begin theorem Th1: :: MSAFREE1:1 for f, g being Function st g in product f holds rng g c= Union f proof let f, g be Function; ::_thesis: ( g in product f implies rng g c= Union f ) assume A1: g in product f ; ::_thesis: rng g c= Union f let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in Union f ) assume y in rng g ; ::_thesis: y in Union f then consider x being set such that A2: x in dom g and A3: y = g . x by FUNCT_1:def_3; A4: dom g = dom f by A1, CARD_3:9; then y in f . x by A1, A2, A3, CARD_3:9; hence y in Union f by A4, A2, CARD_5:2; ::_thesis: verum end; scheme :: MSAFREE1:sch 1 DTConstrUniq{ F1() -> non empty DTConstrStr , F2() -> non empty set , F3( set ) -> Element of F2(), F4( set , set , set ) -> Element of F2(), F5() -> Function of (TS F1()),F2(), F6() -> Function of (TS F1()),F2() } : F5() = F6() provided A1: for t being Symbol of F1() st t in Terminals F1() holds F5() . (root-tree t) = F3(t) and A2: for nt being Symbol of F1() for ts being Element of (TS F1()) * st nt ==> roots ts holds for x being Element of F2() * st x = F5() * ts holds F5() . (nt -tree ts) = F4(nt,ts,x) and A3: for t being Symbol of F1() st t in Terminals F1() holds F6() . (root-tree t) = F3(t) and A4: for nt being Symbol of F1() for ts being Element of (TS F1()) * st nt ==> roots ts holds for x being Element of F2() * st x = F6() * ts holds F6() . (nt -tree ts) = F4(nt,ts,x) proof defpred S1[ set ] means F5() . \$1 = F6() . \$1; A5: for nt being Symbol of F1() for ts being FinSequence of TS F1() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds S1[t] ) holds S1[nt -tree ts] proof let nt be Symbol of F1(); ::_thesis: for ts being FinSequence of TS F1() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds S1[t] ) holds S1[nt -tree ts] let ts be FinSequence of TS F1(); ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds S1[t] ) implies S1[nt -tree ts] ) assume that A6: nt ==> roots ts and A7: for t being DecoratedTree of the carrier of F1() st t in rng ts holds F5() . t = F6() . t ; ::_thesis: S1[nt -tree ts] A8: rng ts c= TS F1() by FINSEQ_1:def_4; then A9: rng ts c= dom F5() by FUNCT_2:def_1; then A10: dom (F5() * ts) = dom ts by RELAT_1:27; rng ts c= dom F6() by A8, FUNCT_2:def_1; then A11: dom (F6() * ts) = dom ts by RELAT_1:27; A12: now__::_thesis:_for_x_being_set_st_x_in_dom_ts_holds_ (F5()_*_ts)_._x_=_(F6()_*_ts)_._x let x be set ; ::_thesis: ( x in dom ts implies (F5() * ts) . x = (F6() * ts) . x ) assume A13: x in dom ts ; ::_thesis: (F5() * ts) . x = (F6() * ts) . x then reconsider t = ts . x as Element of FinTrees the carrier of F1() by DTCONSTR:2; t in rng ts by A13, FUNCT_1:def_3; then A14: F5() . t = F6() . t by A7; thus (F5() * ts) . x = F5() . t by A10, A13, FUNCT_1:12 .= (F6() * ts) . x by A11, A13, A14, FUNCT_1:12 ; ::_thesis: verum end; dom (F5() * ts) = dom ts by A9, RELAT_1:27 .= Seg (len ts) by FINSEQ_1:def_3 ; then reconsider ntv1 = F5() * ts as FinSequence by FINSEQ_1:def_2; rng ntv1 c= F2() by RELAT_1:def_19; then ntv1 is FinSequence of F2() by FINSEQ_1:def_4; then reconsider ntv1 = ntv1 as Element of F2() * by FINSEQ_1:def_11; reconsider tss = ts as Element of (TS F1()) * by FINSEQ_1:def_11; thus F5() . (nt -tree ts) = F4(nt,tss,ntv1) by A2, A6 .= F6() . (nt -tree ts) by A4, A6, A10, A11, A12, FUNCT_1:2 ; ::_thesis: verum end; A15: for s being Symbol of F1() st s in Terminals F1() holds S1[ root-tree s] proof let s be Symbol of F1(); ::_thesis: ( s in Terminals F1() implies S1[ root-tree s] ) assume A16: s in Terminals F1() ; ::_thesis: S1[ root-tree s] hence F5() . (root-tree s) = F3(s) by A1 .= F6() . (root-tree s) by A3, A16 ; ::_thesis: verum end; for t being DecoratedTree of the carrier of F1() st t in TS F1() holds S1[t] from DTCONSTR:sch_7(A15, A5); then for x being set st x in TS F1() holds F5() . x = F6() . x ; hence F5() = F6() by FUNCT_2:12; ::_thesis: verum end; theorem Th2: :: MSAFREE1:2 for S being non empty non void ManySortedSign for X being ManySortedSet of the carrier of S for o, b being set st [o,b] in REL X holds ( o in [: the carrier' of S,{ the carrier of S}:] & b in ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * ) proof let S be non empty non void ManySortedSign ; ::_thesis: for X being ManySortedSet of the carrier of S for o, b being set st [o,b] in REL X holds ( o in [: the carrier' of S,{ the carrier of S}:] & b in ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * ) let X be ManySortedSet of the carrier of S; ::_thesis: for o, b being set st [o,b] in REL X holds ( o in [: the carrier' of S,{ the carrier of S}:] & b in ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * ) let o, b be set ; ::_thesis: ( [o,b] in REL X implies ( o in [: the carrier' of S,{ the carrier of S}:] & b in ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * ) ) assume A1: [o,b] in REL X ; ::_thesis: ( o in [: the carrier' of S,{ the carrier of S}:] & b in ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * ) then reconsider o9 = o as Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by ZFMISC_1:87; reconsider b9 = b as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by A1, ZFMISC_1:87; A2: [o9,b9] in REL X by A1; hence o in [: the carrier' of S,{ the carrier of S}:] by MSAFREE:def_7; ::_thesis: b in ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * thus b in ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by A2; ::_thesis: verum end; theorem :: MSAFREE1:3 for S being non empty non void ManySortedSign for X being ManySortedSet of the carrier of S for o being OperSymbol of S for b being FinSequence st [[o, the carrier of S],b] in REL X holds ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds ( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for X being ManySortedSet of the carrier of S for o being OperSymbol of S for b being FinSequence st [[o, the carrier of S],b] in REL X holds ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds ( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) let X be ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S for b being FinSequence st [[o, the carrier of S],b] in REL X holds ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds ( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) let o be OperSymbol of S; ::_thesis: for b being FinSequence st [[o, the carrier of S],b] in REL X holds ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds ( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) let b be FinSequence; ::_thesis: ( [[o, the carrier of S],b] in REL X implies ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds ( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) assume A1: [[o, the carrier of S],b] in REL X ; ::_thesis: ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds ( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) then reconsider b9 = b as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by Th2; len b9 = len (the_arity_of o) by A1, MSAFREE:5; hence len b = len (the_arity_of o) ; ::_thesis: for x being set st x in dom b holds ( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) for x being set st x in dom b9 holds ( ( b9 . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b9 . x holds the_result_sort_of o1 = (the_arity_of o) . x ) & ( b9 . x in Union (coprod X) implies b9 . x in coprod (((the_arity_of o) . x),X) ) ) by A1, MSAFREE:5; hence for x being set st x in dom b holds ( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ; ::_thesis: verum end; registration let I be non empty set ; let M be ManySortedSet of I; cluster rng M -> non empty ; coherence not rng M is empty ; end; registration let I be set ; cluster Relation-like V3() I -defined Function-like total -> disjoint_valued for set ; coherence for b1 being ManySortedSet of I st b1 is V3() holds b1 is disjoint_valued proof let M be ManySortedSet of I; ::_thesis: ( M is V3() implies M is disjoint_valued ) assume A1: M is V3() ; ::_thesis: M is disjoint_valued let x, y be set ; :: according to PROB_2:def_2 ::_thesis: ( x = y or M . x misses M . y ) assume x <> y ; ::_thesis: M . x misses M . y percases ( ( x in dom M & y in dom M ) or not x in dom M or not y in dom M ) ; suppose ( x in dom M & y in dom M ) ; ::_thesis: M . x misses M . y M . x is empty by A1; hence M . x misses M . y by XBOOLE_1:65; ::_thesis: verum end; suppose ( not x in dom M or not y in dom M ) ; ::_thesis: M . x misses M . y then ( M . x = {} or M . y = {} ) by FUNCT_1:def_2; hence M . x misses M . y by XBOOLE_1:65; ::_thesis: verum end; end; end; end; registration let I be set ; cluster Relation-like I -defined Function-like total disjoint_valued for set ; existence ex b1 being ManySortedSet of I st b1 is disjoint_valued proof set M = the V3() ManySortedSet of I; take the V3() ManySortedSet of I ; ::_thesis: the V3() ManySortedSet of I is disjoint_valued thus the V3() ManySortedSet of I is disjoint_valued ; ::_thesis: verum end; end; definition let I be non empty set ; let X be disjoint_valued ManySortedSet of I; let D be V2() ManySortedSet of I; let F be ManySortedFunction of X,D; func Flatten F -> Function of (Union X),(Union D) means :Def1: :: MSAFREE1:def 1 for i being Element of I for x being set st x in X . i holds it . x = (F . i) . x; existence ex b1 being Function of (Union X),(Union D) st for i being Element of I for x being set st x in X . i holds b1 . x = (F . i) . x proof defpred S1[ set , set ] means for i being Element of I st \$1 in X . i holds \$2 = (F . i) . \$1; A1: for x being set st x in Union X holds ex y being set st ( y in Union D & S1[x,y] ) proof let e be set ; ::_thesis: ( e in Union X implies ex y being set st ( y in Union D & S1[e,y] ) ) assume e in Union X ; ::_thesis: ex y being set st ( y in Union D & S1[e,y] ) then consider i being set such that A2: i in dom X and A3: e in X . i by CARD_5:2; reconsider i = i as Element of I by A2, PARTFUN1:def_2; take u = (F . i) . e; ::_thesis: ( u in Union D & S1[e,u] ) i in I ; then A4: i in dom D by PARTFUN1:def_2; (F . i) . e in D . i by A3, FUNCT_2:5; hence u in Union D by A4, CARD_5:2; ::_thesis: S1[e,u] let i9 be Element of I; ::_thesis: ( e in X . i9 implies u = (F . i9) . e ) assume e in X . i9 ; ::_thesis: u = (F . i9) . e then X . i9 meets X . i by A3, XBOOLE_0:3; hence u = (F . i9) . e by PROB_2:def_2; ::_thesis: verum end; consider f being Function of (Union X),(Union D) such that A5: for e being set st e in Union X holds S1[e,f . e] from FUNCT_2:sch_1(A1); take f ; ::_thesis: for i being Element of I for x being set st x in X . i holds f . x = (F . i) . x let i be Element of I; ::_thesis: for x being set st x in X . i holds f . x = (F . i) . x let x be set ; ::_thesis: ( x in X . i implies f . x = (F . i) . x ) assume A6: x in X . i ; ::_thesis: f . x = (F . i) . x i in I ; then i in dom X by PARTFUN1:def_2; then x in Union X by A6, CARD_5:2; hence f . x = (F . i) . x by A5, A6; ::_thesis: verum end; correctness uniqueness for b1, b2 being Function of (Union X),(Union D) st ( for i being Element of I for x being set st x in X . i holds b1 . x = (F . i) . x ) & ( for i being Element of I for x being set st x in X . i holds b2 . x = (F . i) . x ) holds b1 = b2; proof let F1, F2 be Function of (Union X),(Union D); ::_thesis: ( ( for i being Element of I for x being set st x in X . i holds F1 . x = (F . i) . x ) & ( for i being Element of I for x being set st x in X . i holds F2 . x = (F . i) . x ) implies F1 = F2 ) assume that A7: for i being Element of I for x being set st x in X . i holds F1 . x = (F . i) . x and A8: for i being Element of I for x being set st x in X . i holds F2 . x = (F . i) . x ; ::_thesis: F1 = F2 now__::_thesis:_for_x_being_set_st_x_in_Union_X_holds_ F1_._x_=_F2_._x let x be set ; ::_thesis: ( x in Union X implies F1 . x = F2 . x ) assume x in Union X ; ::_thesis: F1 . x = F2 . x then consider i being set such that A9: i in dom X and A10: x in X . i by CARD_5:2; reconsider i = i as Element of I by A9, PARTFUN1:def_2; thus F1 . x = (F . i) . x by A7, A10 .= F2 . x by A8, A10 ; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def1 defines Flatten MSAFREE1:def_1_:_ for I being non empty set for X being disjoint_valued ManySortedSet of I for D being V2() ManySortedSet of I for F being ManySortedFunction of X,D for b5 being Function of (Union X),(Union D) holds ( b5 = Flatten F iff for i being Element of I for x being set st x in X . i holds b5 . x = (F . i) . x ); theorem Th4: :: MSAFREE1:4 for I being non empty set for X being disjoint_valued ManySortedSet of I for D being V2() ManySortedSet of I for F1, F2 being ManySortedFunction of X,D st Flatten F1 = Flatten F2 holds F1 = F2 proof let I be non empty set ; ::_thesis: for X being disjoint_valued ManySortedSet of I for D being V2() ManySortedSet of I for F1, F2 being ManySortedFunction of X,D st Flatten F1 = Flatten F2 holds F1 = F2 let X be disjoint_valued ManySortedSet of I; ::_thesis: for D being V2() ManySortedSet of I for F1, F2 being ManySortedFunction of X,D st Flatten F1 = Flatten F2 holds F1 = F2 let D be V2() ManySortedSet of I; ::_thesis: for F1, F2 being ManySortedFunction of X,D st Flatten F1 = Flatten F2 holds F1 = F2 let F1, F2 be ManySortedFunction of X,D; ::_thesis: ( Flatten F1 = Flatten F2 implies F1 = F2 ) assume A1: Flatten F1 = Flatten F2 ; ::_thesis: F1 = F2 now__::_thesis:_for_i_being_set_st_i_in_I_holds_ F1_._i_=_F2_._i let i be set ; ::_thesis: ( i in I implies F1 . i = F2 . i ) assume A2: i in I ; ::_thesis: F1 . i = F2 . i then reconsider Di = D . i as non empty set ; reconsider f1 = F1 . i, f2 = F2 . i as Function of (X . i),Di by A2, PBOOLE:def_15; now__::_thesis:_for_x_being_set_st_x_in_X_._i_holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in X . i implies f1 . x = f2 . x ) assume A3: x in X . i ; ::_thesis: f1 . x = f2 . x hence f1 . x = (Flatten F1) . x by A2, Def1 .= f2 . x by A1, A2, A3, Def1 ; ::_thesis: verum end; hence F1 . i = F2 . i by FUNCT_2:12; ::_thesis: verum end; hence F1 = F2 by PBOOLE:3; ::_thesis: verum end; definition let S be non empty ManySortedSign ; let A be MSAlgebra over S; attrA is disjoint_valued means :Def2: :: MSAFREE1:def 2 the Sorts of A is disjoint_valued ; end; :: deftheorem Def2 defines disjoint_valued MSAFREE1:def_2_:_ for S being non empty ManySortedSign for A being MSAlgebra over S holds ( A is disjoint_valued iff the Sorts of A is disjoint_valued ); definition let S be non empty ManySortedSign ; func SingleAlg S -> strict MSAlgebra over S means :Def3: :: MSAFREE1:def 3 for i being set st i in the carrier of S holds the Sorts of it . i = {i}; existence ex b1 being strict MSAlgebra over S st for i being set st i in the carrier of S holds the Sorts of b1 . i = {i} proof deffunc H1( set ) -> set = {\$1}; consider f being ManySortedSet of the carrier of S such that A1: for i being set st i in the carrier of S holds f . i = H1(i) from PBOOLE:sch_4(); set Ch = the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S; take MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #) ; ::_thesis: for i being set st i in the carrier of S holds the Sorts of MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #) . i = {i} thus for i being set st i in the carrier of S holds the Sorts of MSAlgebra(# f, the ManySortedFunction of (f #) * the Arity of S,f * the ResultSort of S #) . i = {i} by A1; ::_thesis: verum end; uniqueness for b1, b2 being strict MSAlgebra over S st ( for i being set st i in the carrier of S holds the Sorts of b1 . i = {i} ) & ( for i being set st i in the carrier of S holds the Sorts of b2 . i = {i} ) holds b1 = b2 proof let A1, A2 be strict MSAlgebra over S; ::_thesis: ( ( for i being set st i in the carrier of S holds the Sorts of A1 . i = {i} ) & ( for i being set st i in the carrier of S holds the Sorts of A2 . i = {i} ) implies A1 = A2 ) assume that A2: for i being set st i in the carrier of S holds the Sorts of A1 . i = {i} and A3: for i being set st i in the carrier of S holds the Sorts of A2 . i = {i} ; ::_thesis: A1 = A2 set B = the Sorts of A1; now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ the_Sorts_of_A1_._i_=_the_Sorts_of_A2_._i let i be set ; ::_thesis: ( i in the carrier of S implies the Sorts of A1 . i = the Sorts of A2 . i ) assume A4: i in the carrier of S ; ::_thesis: the Sorts of A1 . i = the Sorts of A2 . i hence the Sorts of A1 . i = {i} by A2 .= the Sorts of A2 . i by A3, A4 ; ::_thesis: verum end; then A5: the Sorts of A1 = the Sorts of A2 by PBOOLE:3; A6: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1; now__::_thesis:_for_i_being_set_st_i_in_the_carrier'_of_S_holds_ the_Charact_of_A1_._i_=_the_Charact_of_A2_._i let i be set ; ::_thesis: ( i in the carrier' of S implies the Charact of A1 . i = the Charact of A2 . i ) set A = ( the Sorts of A1 * the ResultSort of S) . i; assume A7: i in the carrier' of S ; ::_thesis: the Charact of A1 . i = the Charact of A2 . i then A8: ( the Sorts of A1 * the ResultSort of S) . i = the Sorts of A1 . ( the ResultSort of S . i) by A6, FUNCT_1:13 .= {( the ResultSort of S . i)} by A2, A7, FUNCT_2:5 ; then reconsider A = ( the Sorts of A1 * the ResultSort of S) . i as non empty set ; reconsider f1 = the Charact of A1 . i, f2 = the Charact of A2 . i as Function of ((( the Sorts of A1 #) * the Arity of S) . i),A by A5, A7, PBOOLE:def_15; now__::_thesis:_for_x_being_set_st_x_in_((_the_Sorts_of_A1_#)_*_the_Arity_of_S)_._i_holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in (( the Sorts of A1 #) * the Arity of S) . i implies f1 . x = f2 . x ) assume A9: x in (( the Sorts of A1 #) * the Arity of S) . i ; ::_thesis: f1 . x = f2 . x then f1 . x in A by FUNCT_2:5; then A10: f1 . x = the ResultSort of S . i by A8, TARSKI:def_1; f2 . x in A by A9, FUNCT_2:5; hence f1 . x = f2 . x by A8, A10, TARSKI:def_1; ::_thesis: verum end; hence the Charact of A1 . i = the Charact of A2 . i by FUNCT_2:12; ::_thesis: verum end; hence A1 = A2 by A5, PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def3 defines SingleAlg MSAFREE1:def_3_:_ for S being non empty ManySortedSign for b2 being strict MSAlgebra over S holds ( b2 = SingleAlg S iff for i being set st i in the carrier of S holds the Sorts of b2 . i = {i} ); Lm1: for S being non empty ManySortedSign holds ( SingleAlg S is non-empty & SingleAlg S is disjoint_valued ) proof let S be non empty ManySortedSign ; ::_thesis: ( SingleAlg S is non-empty & SingleAlg S is disjoint_valued ) set F = the Sorts of (SingleAlg S); hereby :: according to MSUALG_1:def_3,PBOOLE:def_13 ::_thesis: SingleAlg S is disjoint_valued let x be set ; ::_thesis: ( x in the carrier of S implies not the Sorts of (SingleAlg S) . x is empty ) assume x in the carrier of S ; ::_thesis: not the Sorts of (SingleAlg S) . x is empty then the Sorts of (SingleAlg S) . x = {x} by Def3; hence not the Sorts of (SingleAlg S) . x is empty ; ::_thesis: verum end; let x, y be set ; :: according to PROB_2:def_2,MSAFREE1:def_2 ::_thesis: ( x = y or the Sorts of (SingleAlg S) . x misses the Sorts of (SingleAlg S) . y ) assume A1: x <> y ; ::_thesis: the Sorts of (SingleAlg S) . x misses the Sorts of (SingleAlg S) . y percases ( ( x in dom the Sorts of (SingleAlg S) & y in dom the Sorts of (SingleAlg S) ) or not x in dom the Sorts of (SingleAlg S) or not y in dom the Sorts of (SingleAlg S) ) ; supposeA2: ( x in dom the Sorts of (SingleAlg S) & y in dom the Sorts of (SingleAlg S) ) ; ::_thesis: the Sorts of (SingleAlg S) . x misses the Sorts of (SingleAlg S) . y dom the Sorts of (SingleAlg S) = the carrier of S by PARTFUN1:def_2; then A3: ( the Sorts of (SingleAlg S) . x = {x} & the Sorts of (SingleAlg S) . y = {y} ) by A2, Def3; assume the Sorts of (SingleAlg S) . x meets the Sorts of (SingleAlg S) . y ; ::_thesis: contradiction hence contradiction by A1, A3, ZFMISC_1:11; ::_thesis: verum end; suppose ( not x in dom the Sorts of (SingleAlg S) or not y in dom the Sorts of (SingleAlg S) ) ; ::_thesis: the Sorts of (SingleAlg S) . x misses the Sorts of (SingleAlg S) . y then ( the Sorts of (SingleAlg S) . x = {} or the Sorts of (SingleAlg S) . y = {} ) by FUNCT_1:def_2; hence the Sorts of (SingleAlg S) . x misses the Sorts of (SingleAlg S) . y by XBOOLE_1:65; ::_thesis: verum end; end; end; registration let S be non empty ManySortedSign ; cluster non-empty disjoint_valued for MSAlgebra over S; existence ex b1 being MSAlgebra over S st ( b1 is non-empty & b1 is disjoint_valued ) proof ( SingleAlg S is non-empty & SingleAlg S is disjoint_valued ) by Lm1; hence ex b1 being MSAlgebra over S st ( b1 is non-empty & b1 is disjoint_valued ) ; ::_thesis: verum end; end; registration let S be non empty ManySortedSign ; cluster SingleAlg S -> strict non-empty disjoint_valued ; coherence ( SingleAlg S is non-empty & SingleAlg S is disjoint_valued ) by Lm1; end; registration let S be non empty ManySortedSign ; let A be disjoint_valued MSAlgebra over S; cluster the Sorts of A -> disjoint_valued ; coherence the Sorts of A is disjoint_valued by Def2; end; theorem Th5: :: MSAFREE1:5 for S being non empty non void ManySortedSign for o being OperSymbol of S for A1 being non-empty disjoint_valued MSAlgebra over S for A2 being non-empty MSAlgebra over S for f being ManySortedFunction of A1,A2 for a being Element of Args (o,A1) holds (Flatten f) * a = f # a proof let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S for A1 being non-empty disjoint_valued MSAlgebra over S for A2 being non-empty MSAlgebra over S for f being ManySortedFunction of A1,A2 for a being Element of Args (o,A1) holds (Flatten f) * a = f # a let o be OperSymbol of S; ::_thesis: for A1 being non-empty disjoint_valued MSAlgebra over S for A2 being non-empty MSAlgebra over S for f being ManySortedFunction of A1,A2 for a being Element of Args (o,A1) holds (Flatten f) * a = f # a let A1 be non-empty disjoint_valued MSAlgebra over S; ::_thesis: for A2 being non-empty MSAlgebra over S for f being ManySortedFunction of A1,A2 for a being Element of Args (o,A1) holds (Flatten f) * a = f # a let A2 be non-empty MSAlgebra over S; ::_thesis: for f being ManySortedFunction of A1,A2 for a being Element of Args (o,A1) holds (Flatten f) * a = f # a let f be ManySortedFunction of A1,A2; ::_thesis: for a being Element of Args (o,A1) holds (Flatten f) * a = f # a let a be Element of Args (o,A1); ::_thesis: (Flatten f) * a = f # a A1: dom the Arity of S = the carrier' of S by FUNCT_2:def_1; set s = the_arity_of o; a in (( the Sorts of A1 #) * the Arity of S) . o ; then a in ( the Sorts of A1 #) . ( the Arity of S . o) by A1, FUNCT_1:13; then A2: a in product ( the Sorts of A1 * (the_arity_of o)) by FINSEQ_2:def_5; then rng a c= Union ( the Sorts of A1 * (the_arity_of o)) by Th1; then ( union (rng ( the Sorts of A1 * (the_arity_of o))) c= union (rng the Sorts of A1) & rng a c= union (rng ( the Sorts of A1 * (the_arity_of o))) ) by CARD_3:def_4, RELAT_1:26, ZFMISC_1:77; then rng a c= union (rng the Sorts of A1) by XBOOLE_1:1; then rng a c= Union the Sorts of A1 by CARD_3:def_4; then rng a c= dom (Flatten f) by FUNCT_2:def_1; then A3: dom ((Flatten f) * a) = dom a by RELAT_1:27; A4: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4; dom the Sorts of A1 = the carrier of S by PARTFUN1:def_2; then A5: dom ( the Sorts of A1 * (the_arity_of o)) = dom (the_arity_of o) by A4, RELAT_1:27; A6: dom a = dom ( the Sorts of A1 * (the_arity_of o)) by A2, CARD_3:9; A7: now__::_thesis:_for_x_being_set_st_x_in_dom_(_the_Sorts_of_A2_*_(the_arity_of_o))_holds_ ((Flatten_f)_*_a)_._x_in_(_the_Sorts_of_A2_*_(the_arity_of_o))_._x let x be set ; ::_thesis: ( x in dom ( the Sorts of A2 * (the_arity_of o)) implies ((Flatten f) * a) . x in ( the Sorts of A2 * (the_arity_of o)) . x ) assume A8: x in dom ( the Sorts of A2 * (the_arity_of o)) ; ::_thesis: ((Flatten f) * a) . x in ( the Sorts of A2 * (the_arity_of o)) . x A9: dom ( the Sorts of A2 * (the_arity_of o)) c= dom (the_arity_of o) by RELAT_1:25; then A10: the Sorts of A2 . ((the_arity_of o) . x) = ( the Sorts of A2 * (the_arity_of o)) . x by A8, FUNCT_1:13; (the_arity_of o) . x in rng (the_arity_of o) by A9, A8, FUNCT_1:def_3; then reconsider z = (the_arity_of o) . x as SortSymbol of S by A4; the Sorts of A1 . ((the_arity_of o) . x) = ( the Sorts of A1 * (the_arity_of o)) . x by A9, A8, FUNCT_1:13; then A11: a . x in the Sorts of A1 . z by A2, A5, A9, A8, CARD_3:9; ((Flatten f) * a) . x = (Flatten f) . (a . x) by A6, A5, A9, A8, FUNCT_1:13 .= (f . z) . (a . x) by A11, Def1 ; hence ((Flatten f) * a) . x in ( the Sorts of A2 * (the_arity_of o)) . x by A10, A11, FUNCT_2:5; ::_thesis: verum end; dom the Sorts of A2 = the carrier of S by PARTFUN1:def_2; then dom (the_arity_of o) = dom ( the Sorts of A2 * (the_arity_of o)) by A4, RELAT_1:27; then (Flatten f) * a in product ( the Sorts of A2 * (the_arity_of o)) by A3, A6, A5, A7, CARD_3:9; then (Flatten f) * a in ( the Sorts of A2 #) . ( the Arity of S . o) by FINSEQ_2:def_5; then reconsider x = (Flatten f) * a as Element of Args (o,A2) by A1, FUNCT_1:13; now__::_thesis:_for_n_being_Nat_st_n_in_dom_a_holds_ x_._n_=_(f_._((the_arity_of_o)_/._n))_._(a_._n) let n be Nat; ::_thesis: ( n in dom a implies x . n = (f . ((the_arity_of o) /. n)) . (a . n) ) assume A12: n in dom a ; ::_thesis: x . n = (f . ((the_arity_of o) /. n)) . (a . n) then ( (the_arity_of o) /. n = (the_arity_of o) . n & a . n in ( the Sorts of A1 * (the_arity_of o)) . n ) by A2, A6, A5, CARD_3:9, PARTFUN1:def_6; then A13: a . n in the Sorts of A1 . ((the_arity_of o) /. n) by A6, A5, A12, FUNCT_1:13; thus x . n = (Flatten f) . (a . n) by A12, FUNCT_1:13 .= (f . ((the_arity_of o) /. n)) . (a . n) by A13, Def1 ; ::_thesis: verum end; hence (Flatten f) * a = f # a by MSUALG_3:def_6; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let X be V2() ManySortedSet of the carrier of S; cluster FreeSort X -> disjoint_valued ; coherence FreeSort X is disjoint_valued proof let x, y be set ; :: according to PROB_2:def_2 ::_thesis: ( x = y or (FreeSort X) . x misses (FreeSort X) . y ) set F = FreeSort X; percases ( ( x in dom (FreeSort X) & y in dom (FreeSort X) ) or not x in dom (FreeSort X) or not y in dom (FreeSort X) ) ; suppose ( x in dom (FreeSort X) & y in dom (FreeSort X) ) ; ::_thesis: ( x = y or (FreeSort X) . x misses (FreeSort X) . y ) then reconsider s1 = x, s2 = y as SortSymbol of S by PARTFUN1:def_2; assume x <> y ; ::_thesis: (FreeSort X) . x misses (FreeSort X) . y then (FreeSort X) . s1 misses (FreeSort X) . s2 by MSAFREE:12; hence (FreeSort X) . x misses (FreeSort X) . y ; ::_thesis: verum end; supposeA1: ( not x in dom (FreeSort X) or not y in dom (FreeSort X) ) ; ::_thesis: ( x = y or (FreeSort X) . x misses (FreeSort X) . y ) assume x <> y ; ::_thesis: (FreeSort X) . x misses (FreeSort X) . y ( (FreeSort X) . x = {} or (FreeSort X) . y = {} ) by A1, FUNCT_1:def_2; hence (FreeSort X) . x misses (FreeSort X) . y by XBOOLE_1:65; ::_thesis: verum end; end; end; end; scheme :: MSAFREE1:sch 2 FreeSortUniq{ F1() -> non empty non void ManySortedSign , F2() -> V2() ManySortedSet of the carrier of F1(), F3() -> V2() ManySortedSet of the carrier of F1(), F4( set ) -> Element of Union F3(), F5( set , set , set ) -> Element of Union F3(), F6() -> ManySortedFunction of FreeSort F2(),F3(), F7() -> ManySortedFunction of FreeSort F2(),F3() } : F6() = F7() provided A1: for o being OperSymbol of F1() for ts being Element of Args (o,(FreeMSA F2())) for x being Element of (Union F3()) * st x = (Flatten F6()) * ts holds (F6() . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = F5(o,ts,x) and A2: for s being SortSymbol of F1() for y being set st y in FreeGen (s,F2()) holds (F6() . s) . y = F4(y) and A3: for o being OperSymbol of F1() for ts being Element of Args (o,(FreeMSA F2())) for x being Element of (Union F3()) * st x = (Flatten F7()) * ts holds (F7() . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = F5(o,ts,x) and A4: for s being SortSymbol of F1() for y being set st y in FreeGen (s,F2()) holds (F7() . s) . y = F4(y) proof reconsider D = Union F3() as non empty set ; TS (DTConMSA F2()) = union (rng (FreeSort F2())) by MSAFREE:11 .= Union (FreeSort F2()) by CARD_3:def_4 ; then reconsider f1 = Flatten F6(), f2 = Flatten F7() as Function of (TS (DTConMSA F2())),D ; deffunc H1( Element of (DTConMSA F2()), Element of (TS (DTConMSA F2())) * , Element of (Union F3()) * ) -> Element of Union F3() = F5((\$1 `1),\$2,\$3); consider H being Function of [: the carrier of (DTConMSA F2()),((TS (DTConMSA F2())) *),((Union F3()) *):],(Union F3()) such that A5: for nt being Element of (DTConMSA F2()) for ts being Element of (TS (DTConMSA F2())) * for x being Element of (Union F3()) * holds H . (nt,ts,x) = H1(nt,ts,x) from MULTOP_1:sch_4(); reconsider H = H as Function of [: the carrier of (DTConMSA F2()),((TS (DTConMSA F2())) *),(D *):],D ; deffunc H2( Element of (DTConMSA F2()), Element of (TS (DTConMSA F2())) * , Element of D * ) -> Element of D = H . (\$1,\$2,\$3); A6: DTConMSA F2() = DTConstrStr(# ([: the carrier' of F1(),{ the carrier of F1()}:] \/ (Union (coprod F2()))),(REL F2()) #) by MSAFREE:def_8; A7: now__::_thesis:_for_f_being_ManySortedFunction_of_FreeSort_F2(),F3()_st_(_for_o_being_OperSymbol_of_F1() for_ts_being_Element_of_Args_(o,(FreeMSA_F2())) for_x_being_Element_of_D_*_st_x_=_(Flatten_f)_*_ts_holds_ (f_._(the_result_sort_of_o))_._((Den_(o,(FreeMSA_F2())))_._ts)_=_F5(o,ts,x)_)_holds_ for_nt_being_Element_of_(DTConMSA_F2()) for_ts_being_Element_of_(TS_(DTConMSA_F2()))_*_st_nt_==>_roots_ts_holds_ for_x_being_Element_of_D_*_st_x_=_(Flatten_f)_*_ts_holds_ (Flatten_f)_._(nt_-tree_ts)_=_H_._(nt,ts,x) let f be ManySortedFunction of FreeSort F2(),F3(); ::_thesis: ( ( for o being OperSymbol of F1() for ts being Element of Args (o,(FreeMSA F2())) for x being Element of D * st x = (Flatten f) * ts holds (f . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = F5(o,ts,x) ) implies for nt being Element of (DTConMSA F2()) for ts being Element of (TS (DTConMSA F2())) * st nt ==> roots ts holds for x being Element of D * st x = (Flatten f) * ts holds (Flatten f) . (nt -tree ts) = H . (nt,ts,x) ) assume A8: for o being OperSymbol of F1() for ts being Element of Args (o,(FreeMSA F2())) for x being Element of D * st x = (Flatten f) * ts holds (f . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = F5(o,ts,x) ; ::_thesis: for nt being Element of (DTConMSA F2()) for ts being Element of (TS (DTConMSA F2())) * st nt ==> roots ts holds for x being Element of D * st x = (Flatten f) * ts holds (Flatten f) . (nt -tree ts) = H . (nt,ts,x) let nt be Element of (DTConMSA F2()); ::_thesis: for ts being Element of (TS (DTConMSA F2())) * st nt ==> roots ts holds for x being Element of D * st x = (Flatten f) * ts holds (Flatten f) . (nt -tree ts) = H . (nt,ts,x) let ts be Element of (TS (DTConMSA F2())) * ; ::_thesis: ( nt ==> roots ts implies for x being Element of D * st x = (Flatten f) * ts holds (Flatten f) . (nt -tree ts) = H . (nt,ts,x) ) assume A9: nt ==> roots ts ; ::_thesis: for x being Element of D * st x = (Flatten f) * ts holds (Flatten f) . (nt -tree ts) = H . (nt,ts,x) then [nt,(roots ts)] in REL F2() by A6, LANG1:def_1; then consider o being OperSymbol of F1(), x2 being Element of { the carrier of F1()} such that A10: nt = [o,x2] by Th2, DOMAIN_1:1; let x be Element of D * ; ::_thesis: ( x = (Flatten f) * ts implies (Flatten f) . (nt -tree ts) = H . (nt,ts,x) ) assume A11: x = (Flatten f) * ts ; ::_thesis: (Flatten f) . (nt -tree ts) = H . (nt,ts,x) A12: FreeMSA F2() = MSAlgebra(# (FreeSort F2()),(FreeOper F2()) #) by MSAFREE:def_14; reconsider tss = ts as FinSequence of TS (DTConMSA F2()) by FINSEQ_1:def_11; reconsider xx = x as Element of (Union F3()) * ; A13: x2 = the carrier of F1() by TARSKI:def_1; then A14: nt = Sym (o,F2()) by A10, MSAFREE:def_9; then A15: tss in (((FreeSort F2()) #) * the Arity of F1()) . o by A9, MSAFREE:10; ((FreeSort F2()) * the ResultSort of F1()) . o = (FreeSort F2()) . (the_result_sort_of o) by FUNCT_2:15; then A16: (DenOp (o,F2())) . ts in (FreeSort F2()) . (the_result_sort_of o) by A15, FUNCT_2:5; (Flatten f) . ([o, the carrier of F1()] -tree ts) = (Flatten f) . ((DenOp (o,F2())) . tss) by A9, A10, A13, A14, MSAFREE:def_12 .= (f . (the_result_sort_of o)) . ((DenOp (o,F2())) . ts) by A16, Def1 .= (f . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) by A12, MSAFREE:def_13 .= F5(o,ts,x) by A8, A12, A15, A11 .= F5((nt `1),ts,x) by A10, MCART_1:7 ; hence (Flatten f) . (nt -tree ts) = H1(nt,ts,xx) by A10, A13 .= H . (nt,ts,x) by A5 ; ::_thesis: verum end; then A17: for nt being Symbol of (DTConMSA F2()) for ts being Element of (TS (DTConMSA F2())) * st nt ==> roots ts holds for x being Element of D * st x = f1 * ts holds f1 . (nt -tree ts) = H2(nt,ts,x) by A1; deffunc H3( Element of (DTConMSA F2())) -> Element of Union F3() = F4((root-tree \$1)); A18: Terminals (DTConMSA F2()) = Union (coprod F2()) by MSAFREE:6; consider G being Function of the carrier of (DTConMSA F2()),(Union F3()) such that A19: for t being Element of (DTConMSA F2()) holds G . t = H3(t) from FUNCT_2:sch_4(); reconsider G = G as Function of the carrier of (DTConMSA F2()),D ; deffunc H4( Element of (DTConMSA F2())) -> Element of D = G . \$1; A20: dom F2() = the carrier of F1() by PARTFUN1:def_2; A21: now__::_thesis:_for_f_being_ManySortedFunction_of_FreeSort_F2(),F3()_st_(_for_s_being_SortSymbol_of_F1() for_y_being_set_st_y_in_FreeGen_(s,F2())_holds_ (f_._s)_._y_=_F4(y)_)_holds_ for_t_being_Element_of_(DTConMSA_F2())_st_t_in_Terminals_(DTConMSA_F2())_holds_ (Flatten_f)_._(root-tree_t)_=_G_._t let f be ManySortedFunction of FreeSort F2(),F3(); ::_thesis: ( ( for s being SortSymbol of F1() for y being set st y in FreeGen (s,F2()) holds (f . s) . y = F4(y) ) implies for t being Element of (DTConMSA F2()) st t in Terminals (DTConMSA F2()) holds (Flatten f) . (root-tree t) = G . t ) assume A22: for s being SortSymbol of F1() for y being set st y in FreeGen (s,F2()) holds (f . s) . y = F4(y) ; ::_thesis: for t being Element of (DTConMSA F2()) st t in Terminals (DTConMSA F2()) holds (Flatten f) . (root-tree t) = G . t let t be Element of (DTConMSA F2()); ::_thesis: ( t in Terminals (DTConMSA F2()) implies (Flatten f) . (root-tree t) = G . t ) assume A23: t in Terminals (DTConMSA F2()) ; ::_thesis: (Flatten f) . (root-tree t) = G . t then reconsider s = t `2 as SortSymbol of F1() by A18, A20, CARD_3:22; t `1 in F2() . (t `2) by A18, A23, CARD_3:22; then A24: root-tree [(t `1),s] in FreeGen (s,F2()) by MSAFREE:def_15; A25: t = [(t `1),(t `2)] by A18, A23, CARD_3:22; hence (Flatten f) . (root-tree t) = (f . s) . (root-tree [(t `1),s]) by A24, Def1 .= F4((root-tree t)) by A22, A25, A24 .= G . t by A19 ; ::_thesis: verum end; then A26: for t being Symbol of (DTConMSA F2()) st t in Terminals (DTConMSA F2()) holds f2 . (root-tree t) = H4(t) by A4; A27: for nt being Symbol of (DTConMSA F2()) for ts being Element of (TS (DTConMSA F2())) * st nt ==> roots ts holds for x being Element of D * st x = f2 * ts holds f2 . (nt -tree ts) = H2(nt,ts,x) by A3, A7; A28: for t being Element of (DTConMSA F2()) st t in Terminals (DTConMSA F2()) holds f1 . (root-tree t) = H4(t) by A2, A21; f1 = f2 from MSAFREE1:sch_1(A28, A17, A26, A27); hence F6() = F7() by Th4; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let X be V2() ManySortedSet of the carrier of S; cluster FreeMSA X -> non-empty ; coherence FreeMSA X is non-empty ; end; registration let S be non empty non void ManySortedSign ; let o be OperSymbol of S; let A be non-empty MSAlgebra over S; cluster Args (o,A) -> non empty ; coherence not Args (o,A) is empty ; cluster Result (o,A) -> non empty ; coherence not Result (o,A) is empty ; end; registration let S be non empty non void ManySortedSign ; let X be V2() ManySortedSet of the carrier of S; cluster the Sorts of (FreeMSA X) -> disjoint_valued ; coherence the Sorts of (FreeMSA X) is disjoint_valued proof FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def_14; hence the Sorts of (FreeMSA X) is disjoint_valued ; ::_thesis: verum end; end; registration let S be non empty non void ManySortedSign ; let X be V2() ManySortedSet of the carrier of S; cluster FreeMSA X -> disjoint_valued ; coherence FreeMSA X is disjoint_valued proof thus the Sorts of (FreeMSA X) is disjoint_valued ; :: according to MSAFREE1:def_2 ::_thesis: verum end; end; scheme :: MSAFREE1:sch 3 ExtFreeGen{ F1() -> non empty non void ManySortedSign , F2() -> V2() ManySortedSet of the carrier of F1(), F3() -> non-empty MSAlgebra over F1(), P1[ set , set , set ], F4() -> ManySortedFunction of (FreeMSA F2()),F3(), F5() -> ManySortedFunction of (FreeMSA F2()),F3() } : F4() = F5() provided A1: F4() is_homomorphism FreeMSA F2(),F3() and A2: for s being SortSymbol of F1() for x, y being set st y in FreeGen (s,F2()) holds ( (F4() . s) . y = x iff P1[s,x,y] ) and A3: F5() is_homomorphism FreeMSA F2(),F3() and A4: for s being SortSymbol of F1() for x, y being set st y in FreeGen (s,F2()) holds ( (F5() . s) . y = x iff P1[s,x,y] ) proof defpred S1[ set , set ] means for s being SortSymbol of F1() st \$1 in FreeGen (s,F2()) holds P1[s,\$2,\$1]; A5: FreeMSA F2() = MSAlgebra(# (FreeSort F2()),(FreeOper F2()) #) by MSAFREE:def_14; then reconsider f1 = F4(), f2 = F5() as ManySortedFunction of FreeSort F2(), the Sorts of F3() ; A6: for x being set st x in Union (FreeGen F2()) holds ex y being set st ( y in Union the Sorts of F3() & S1[x,y] ) proof let e be set ; ::_thesis: ( e in Union (FreeGen F2()) implies ex y being set st ( y in Union the Sorts of F3() & S1[e,y] ) ) A7: dom the Sorts of F3() = the carrier of F1() by PARTFUN1:def_2; assume e in Union (FreeGen F2()) ; ::_thesis: ex y being set st ( y in Union the Sorts of F3() & S1[e,y] ) then consider s being set such that A8: s in dom (FreeGen F2()) and A9: e in (FreeGen F2()) . s by CARD_5:2; reconsider s = s as SortSymbol of F1() by A8, PARTFUN1:def_2; A10: e in FreeGen (s,F2()) by A9, MSAFREE:def_16; take u = (F4() . s) . e; ::_thesis: ( u in Union the Sorts of F3() & S1[e,u] ) f1 . s is Function of ((FreeSort F2()) . s),( the Sorts of F3() . s) ; then u in the Sorts of F3() . s by A10, FUNCT_2:5; hence u in Union the Sorts of F3() by A7, CARD_5:2; ::_thesis: S1[e,u] let s9 be SortSymbol of F1(); ::_thesis: ( e in FreeGen (s9,F2()) implies P1[s9,u,e] ) assume A11: e in FreeGen (s9,F2()) ; ::_thesis: P1[s9,u,e] then ((FreeSort F2()) . s9) /\ ((FreeSort F2()) . s) <> {} by A10, XBOOLE_0:def_4; then (FreeSort F2()) . s9 meets (FreeSort F2()) . s by XBOOLE_0:def_7; then s = s9 by MSAFREE:12; hence P1[s9,u,e] by A2, A11; ::_thesis: verum end; consider G being Function of (Union (FreeGen F2())),(Union the Sorts of F3()) such that A12: for e being set st e in Union (FreeGen F2()) holds S1[e,G . e] from FUNCT_2:sch_1(A6); deffunc H1( set ) -> Element of Union the Sorts of F3() = G /. \$1; defpred S2[ set , set ] means for o being OperSymbol of F1() for a being Element of Args (o,F3()) st \$1 = [o,a] holds \$2 = (Den (o,F3())) . a; consider R being set such that A13: R = { [o,a] where o is Element of the carrier' of F1(), a is Element of Args (o,F3()) : verum } ; A14: for s being SortSymbol of F1() for y being set st y in FreeGen (s,F2()) holds (f1 . s) . y = H1(y) proof let s be SortSymbol of F1(); ::_thesis: for y being set st y in FreeGen (s,F2()) holds (f1 . s) . y = H1(y) let y be set ; ::_thesis: ( y in FreeGen (s,F2()) implies (f1 . s) . y = H1(y) ) A15: dom (FreeGen F2()) = the carrier of F1() by PARTFUN1:def_2; assume A16: y in FreeGen (s,F2()) ; ::_thesis: (f1 . s) . y = H1(y) then y in (FreeGen F2()) . s by MSAFREE:def_16; then A17: y in Union (FreeGen F2()) by A15, CARD_5:2; then P1[s,G . y,y] by A12, A16; hence (f1 . s) . y = G . y by A2, A16 .= G /. y by A17, FUNCT_2:def_13 ; ::_thesis: verum end; A18: for x being set st x in R holds ex y being set st ( y in Union the Sorts of F3() & S2[x,y] ) proof let e be set ; ::_thesis: ( e in R implies ex y being set st ( y in Union the Sorts of F3() & S2[e,y] ) ) assume e in R ; ::_thesis: ex y being set st ( y in Union the Sorts of F3() & S2[e,y] ) then consider o being OperSymbol of F1(), a being Element of Args (o,F3()) such that A19: e = [o,a] by A13; reconsider u = (Den (o,F3())) . a as set ; take u ; ::_thesis: ( u in Union the Sorts of F3() & S2[e,u] ) u in union (rng the Sorts of F3()) by TARSKI:def_4; hence u in Union the Sorts of F3() by CARD_3:def_4; ::_thesis: S2[e,u] let o9 be OperSymbol of F1(); ::_thesis: for a being Element of Args (o9,F3()) st e = [o9,a] holds u = (Den (o9,F3())) . a let x9 be Element of Args (o9,F3()); ::_thesis: ( e = [o9,x9] implies u = (Den (o9,F3())) . x9 ) assume A20: e = [o9,x9] ; ::_thesis: u = (Den (o9,F3())) . x9 then o = o9 by A19, XTUPLE_0:1; hence u = (Den (o9,F3())) . x9 by A19, A20, XTUPLE_0:1; ::_thesis: verum end; consider H being Function of R,(Union the Sorts of F3()) such that A21: for e being set st e in R holds S2[e,H . e] from FUNCT_2:sch_1(A18); A22: for s being SortSymbol of F1() for y being set st y in FreeGen (s,F2()) holds (f2 . s) . y = H1(y) proof let s be SortSymbol of F1(); ::_thesis: for y being set st y in FreeGen (s,F2()) holds (f2 . s) . y = H1(y) let y be set ; ::_thesis: ( y in FreeGen (s,F2()) implies (f2 . s) . y = H1(y) ) A23: dom (FreeGen F2()) = the carrier of F1() by PARTFUN1:def_2; assume A24: y in FreeGen (s,F2()) ; ::_thesis: (f2 . s) . y = H1(y) then y in (FreeGen F2()) . s by MSAFREE:def_16; then A25: y in Union (FreeGen F2()) by A23, CARD_5:2; then P1[s,G . y,y] by A12, A24; hence (f2 . s) . y = G . y by A4, A24 .= G /. y by A25, FUNCT_2:def_13 ; ::_thesis: verum end; deffunc H2( set , set , set ) -> Element of Union the Sorts of F3() = H /. [\$1,\$3]; A26: for o being OperSymbol of F1() for ts being Element of Args (o,(FreeMSA F2())) for x being Element of (Union the Sorts of F3()) * st x = (Flatten f2) * ts holds (f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x) proof let o be OperSymbol of F1(); ::_thesis: for ts being Element of Args (o,(FreeMSA F2())) for x being Element of (Union the Sorts of F3()) * st x = (Flatten f2) * ts holds (f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x) let ts be Element of Args (o,(FreeMSA F2())); ::_thesis: for x being Element of (Union the Sorts of F3()) * st x = (Flatten f2) * ts holds (f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x) let x be Element of (Union the Sorts of F3()) * ; ::_thesis: ( x = (Flatten f2) * ts implies (f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x) ) assume A27: x = (Flatten f2) * ts ; ::_thesis: (f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x) A28: (Flatten f2) * ts = F5() # ts by A5, Th5; then reconsider a = x as Element of Args (o,F3()) by A27; A29: [o,a] in R by A13; thus (f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = (Den (o,F3())) . a by A3, A28, A27, MSUALG_3:def_7 .= H . [o,x] by A21, A29 .= H /. [o,x] by A29, FUNCT_2:def_13 ; ::_thesis: verum end; A30: for o being OperSymbol of F1() for ts being Element of Args (o,(FreeMSA F2())) for x being Element of (Union the Sorts of F3()) * st x = (Flatten f1) * ts holds (f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x) proof let o be OperSymbol of F1(); ::_thesis: for ts being Element of Args (o,(FreeMSA F2())) for x being Element of (Union the Sorts of F3()) * st x = (Flatten f1) * ts holds (f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x) let ts be Element of Args (o,(FreeMSA F2())); ::_thesis: for x being Element of (Union the Sorts of F3()) * st x = (Flatten f1) * ts holds (f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x) let x be Element of (Union the Sorts of F3()) * ; ::_thesis: ( x = (Flatten f1) * ts implies (f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x) ) assume A31: x = (Flatten f1) * ts ; ::_thesis: (f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x) A32: (Flatten f1) * ts = F4() # ts by A5, Th5; then reconsider a = x as Element of Args (o,F3()) by A31; A33: [o,a] in R by A13; thus (f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = (Den (o,F3())) . a by A1, A32, A31, MSUALG_3:def_7 .= H . [o,x] by A21, A33 .= H /. [o,x] by A33, FUNCT_2:def_13 ; ::_thesis: verum end; f1 = f2 from MSAFREE1:sch_2(A30, A14, A26, A22); hence F4() = F5() ; ::_thesis: verum end;