:: EQUATION semantic presentation begin theorem Th1: :: EQUATION:1 for A being set for B, C being non empty set for f being Function of A,B for g being Function of B,C st rng (g * f) = C holds rng g = C proof let A be set ; ::_thesis: for B, C being non empty set for f being Function of A,B for g being Function of B,C st rng (g * f) = C holds rng g = C let B, C be non empty set ; ::_thesis: for f being Function of A,B for g being Function of B,C st rng (g * f) = C holds rng g = C let f be Function of A,B; ::_thesis: for g being Function of B,C st rng (g * f) = C holds rng g = C let g be Function of B,C; ::_thesis: ( rng (g * f) = C implies rng g = C ) assume A1: rng (g * f) = C ; ::_thesis: rng g = C thus rng g c= C ; :: according to XBOOLE_0:def_10 ::_thesis: C c= rng g let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in C or q in rng g ) assume q in C ; ::_thesis: q in rng g then consider x being set such that A2: x in dom (g * f) and A3: q = (g * f) . x by A1, FUNCT_1:def_3; A4: dom f = A by FUNCT_2:def_1; then A5: f . x in rng f by A2, FUNCT_1:def_3; dom (g * f) = A by FUNCT_2:def_1; then A6: rng f c= dom g by A4, FUNCT_1:15; q = g . (f . x) by A2, A3, FUNCT_1:12; hence q in rng g by A6, A5, FUNCT_1:def_3; ::_thesis: verum end; theorem :: EQUATION:2 for I being set for A being ManySortedSet of I for B, C being V2() ManySortedSet of I for f being ManySortedFunction of A,B for g being ManySortedFunction of B,C st g ** f is "onto" holds g is "onto" proof let I be set ; ::_thesis: for A being ManySortedSet of I for B, C being V2() ManySortedSet of I for f being ManySortedFunction of A,B for g being ManySortedFunction of B,C st g ** f is "onto" holds g is "onto" let A be ManySortedSet of I; ::_thesis: for B, C being V2() ManySortedSet of I for f being ManySortedFunction of A,B for g being ManySortedFunction of B,C st g ** f is "onto" holds g is "onto" let B, C be V2() ManySortedSet of I; ::_thesis: for f being ManySortedFunction of A,B for g being ManySortedFunction of B,C st g ** f is "onto" holds g is "onto" let f be ManySortedFunction of A,B; ::_thesis: for g being ManySortedFunction of B,C st g ** f is "onto" holds g is "onto" let g be ManySortedFunction of B,C; ::_thesis: ( g ** f is "onto" implies g is "onto" ) assume A1: g ** f is "onto" ; ::_thesis: g is "onto" let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in I or proj2 (g . i) = C . i ) assume A2: i in I ; ::_thesis: proj2 (g . i) = C . i then A3: ( f . i is Function of (A . i),(B . i) & g . i is Function of (B . i),(C . i) ) by PBOOLE:def_15; rng ((g . i) * (f . i)) = rng ((g ** f) . i) by A2, MSUALG_3:2 .= C . i by A1, A2, MSUALG_3:def_3 ; hence proj2 (g . i) = C . i by A2, A3, Th1; ::_thesis: verum end; theorem Th3: :: EQUATION:3 for A, B being non empty set for C, y being set for f being Function st f in Funcs (A,(Funcs (B,C))) & y in B holds ( dom ((commute f) . y) = A & rng ((commute f) . y) c= C ) proof let A, B be non empty set ; ::_thesis: for C, y being set for f being Function st f in Funcs (A,(Funcs (B,C))) & y in B holds ( dom ((commute f) . y) = A & rng ((commute f) . y) c= C ) let C, y be set ; ::_thesis: for f being Function st f in Funcs (A,(Funcs (B,C))) & y in B holds ( dom ((commute f) . y) = A & rng ((commute f) . y) c= C ) let f be Function; ::_thesis: ( f in Funcs (A,(Funcs (B,C))) & y in B implies ( dom ((commute f) . y) = A & rng ((commute f) . y) c= C ) ) assume that A1: f in Funcs (A,(Funcs (B,C))) and A2: y in B ; ::_thesis: ( dom ((commute f) . y) = A & rng ((commute f) . y) c= C ) set cf = commute f; commute f in Funcs (B,(Funcs (A,C))) by A1, FUNCT_6:55; then A3: ex g being Function st ( g = commute f & dom g = B & rng g c= Funcs (A,C) ) by FUNCT_2:def_2; then (commute f) . y in rng (commute f) by A2, FUNCT_1:def_3; then ex t being Function st ( t = (commute f) . y & dom t = A & rng t c= C ) by A3, FUNCT_2:def_2; hence ( dom ((commute f) . y) = A & rng ((commute f) . y) c= C ) ; ::_thesis: verum end; theorem :: EQUATION:4 for I being set for A, B being ManySortedSet of I st A is_transformable_to B holds for f being ManySortedFunction of I st doms f = A & rngs f c= B holds f is ManySortedFunction of A,B proof let I be set ; ::_thesis: for A, B being ManySortedSet of I st A is_transformable_to B holds for f being ManySortedFunction of I st doms f = A & rngs f c= B holds f is ManySortedFunction of A,B let A, B be ManySortedSet of I; ::_thesis: ( A is_transformable_to B implies for f being ManySortedFunction of I st doms f = A & rngs f c= B holds f is ManySortedFunction of A,B ) assume for i being set st i in I & B . i = {} holds A . i = {} ; :: according to PZFMISC1:def_3 ::_thesis: for f being ManySortedFunction of I st doms f = A & rngs f c= B holds f is ManySortedFunction of A,B let f be ManySortedFunction of I; ::_thesis: ( doms f = A & rngs f c= B implies f is ManySortedFunction of A,B ) assume that A1: doms f = A and A2: rngs f c= B ; ::_thesis: f is ManySortedFunction of A,B let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in I or f . i is Element of bool [:(A . i),(B . i):] ) assume A3: i in I ; ::_thesis: f . i is Element of bool [:(A . i),(B . i):] then reconsider J = I as non empty set ; reconsider s = i as Element of J by A3; A4: dom (f . s) = A . s by A1, MSSUBFAM:14; rng (f . s) = (rngs f) . s by MSSUBFAM:13; then rng (f . s) c= B . s by A2, PBOOLE:def_2; hence f . i is Element of bool [:(A . i),(B . i):] by A4, FUNCT_2:2; ::_thesis: verum end; theorem Th5: :: EQUATION:5 for I being set for A, B being ManySortedSet of I for F being ManySortedFunction of A,B for C, E being ManySortedSubset of A for D being ManySortedSubset of C st E = D holds (F || C) || D = F || E proof let I be set ; ::_thesis: for A, B being ManySortedSet of I for F being ManySortedFunction of A,B for C, E being ManySortedSubset of A for D being ManySortedSubset of C st E = D holds (F || C) || D = F || E let A, B be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B for C, E being ManySortedSubset of A for D being ManySortedSubset of C st E = D holds (F || C) || D = F || E let F be ManySortedFunction of A,B; ::_thesis: for C, E being ManySortedSubset of A for D being ManySortedSubset of C st E = D holds (F || C) || D = F || E let C, E be ManySortedSubset of A; ::_thesis: for D being ManySortedSubset of C st E = D holds (F || C) || D = F || E let D be ManySortedSubset of C; ::_thesis: ( E = D implies (F || C) || D = F || E ) assume A1: E = D ; ::_thesis: (F || C) || D = F || E now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ((F_||_C)_||_D)_._i_=_(F_||_E)_._i let i be set ; ::_thesis: ( i in I implies ((F || C) || D) . i = (F || E) . i ) assume A2: i in I ; ::_thesis: ((F || C) || D) . i = (F || E) . i A3: F . i is Function of (A . i),(B . i) by A2, PBOOLE:def_15; D c= C by PBOOLE:def_18; then A4: D . i c= C . i by A2, PBOOLE:def_2; A5: (F || C) . i is Function of (C . i),(B . i) by A2, PBOOLE:def_15; then reconsider fc = (F . i) | (C . i) as Function of (C . i),(B . i) by A2, A3, MSAFREE:def_1; thus ((F || C) || D) . i = ((F || C) . i) | (D . i) by A2, A5, MSAFREE:def_1 .= fc | (D . i) by A2, A3, MSAFREE:def_1 .= (F . i) | (D . i) by A4, RELAT_1:74 .= (F || E) . i by A1, A2, A3, MSAFREE:def_1 ; ::_thesis: verum end; hence (F || C) || D = F || E by PBOOLE:3; ::_thesis: verum end; theorem Th6: :: EQUATION:6 for I being set for B being V2() ManySortedSet of I for C being ManySortedSet of I for A being ManySortedSubset of C for F being ManySortedFunction of A,B ex G being ManySortedFunction of C,B st G || A = F proof let I be set ; ::_thesis: for B being V2() ManySortedSet of I for C being ManySortedSet of I for A being ManySortedSubset of C for F being ManySortedFunction of A,B ex G being ManySortedFunction of C,B st G || A = F let B be V2() ManySortedSet of I; ::_thesis: for C being ManySortedSet of I for A being ManySortedSubset of C for F being ManySortedFunction of A,B ex G being ManySortedFunction of C,B st G || A = F let C be ManySortedSet of I; ::_thesis: for A being ManySortedSubset of C for F being ManySortedFunction of A,B ex G being ManySortedFunction of C,B st G || A = F let A be ManySortedSubset of C; ::_thesis: for F being ManySortedFunction of A,B ex G being ManySortedFunction of C,B st G || A = F let F be ManySortedFunction of A,B; ::_thesis: ex G being ManySortedFunction of C,B st G || A = F defpred S1[ set , set , set ] means ex f being Function of (A . \$3),(B . \$3) st ( f = F . \$3 & ( \$2 in A . \$3 implies \$1 = f . \$2 ) ); A1: for i being set st i in I holds for x being set st x in C . i holds ex y being set st ( y in B . i & S1[y,x,i] ) proof let i be set ; ::_thesis: ( i in I implies for x being set st x in C . i holds ex y being set st ( y in B . i & S1[y,x,i] ) ) assume A2: i in I ; ::_thesis: for x being set st x in C . i holds ex y being set st ( y in B . i & S1[y,x,i] ) then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; let x be set ; ::_thesis: ( x in C . i implies ex y being set st ( y in B . i & S1[y,x,i] ) ) assume x in C . i ; ::_thesis: ex y being set st ( y in B . i & S1[y,x,i] ) percases ( x in A . i or not x in A . i ) ; supposeA3: x in A . i ; ::_thesis: ex y being set st ( y in B . i & S1[y,x,i] ) take f . x ; ::_thesis: ( f . x in B . i & S1[f . x,x,i] ) thus f . x in B . i by A2, A3, FUNCT_2:5; ::_thesis: S1[f . x,x,i] take f ; ::_thesis: ( f = F . i & ( x in A . i implies f . x = f . x ) ) thus ( f = F . i & ( x in A . i implies f . x = f . x ) ) ; ::_thesis: verum end; supposeA4: not x in A . i ; ::_thesis: ex y being set st ( y in B . i & S1[y,x,i] ) consider y being set such that A5: y in B . i by A2, XBOOLE_0:def_1; take y ; ::_thesis: ( y in B . i & S1[y,x,i] ) thus y in B . i by A5; ::_thesis: S1[y,x,i] take f ; ::_thesis: ( f = F . i & ( x in A . i implies y = f . x ) ) thus ( f = F . i & ( x in A . i implies y = f . x ) ) by A4; ::_thesis: verum end; end; end; consider G being ManySortedFunction of C,B such that A6: for i being set st i in I holds ex g being Function of (C . i),(B . i) st ( g = G . i & ( for x being set st x in C . i holds S1[g . x,x,i] ) ) from MSSUBFAM:sch_1(A1); take G ; ::_thesis: G || A = F now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (G_||_A)_._i_=_F_._i let i be set ; ::_thesis: ( i in I implies (G || A) . i = F . i ) assume A7: i in I ; ::_thesis: (G || A) . i = F . i then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; A8: dom f = A . i by A7, FUNCT_2:def_1; consider g being Function of (C . i),(B . i) such that A9: g = G . i and A10: for x being set st x in C . i holds S1[g . x,x,i] by A6, A7; A c= C by PBOOLE:def_18; then A11: A . i c= C . i by A7, PBOOLE:def_2; A12: for x being set st x in A . i holds f . x = (g | (A . i)) . x proof let x be set ; ::_thesis: ( x in A . i implies f . x = (g | (A . i)) . x ) assume A13: x in A . i ; ::_thesis: f . x = (g | (A . i)) . x then ex h being Function of (A . i),(B . i) st ( h = F . i & ( x in A . i implies g . x = h . x ) ) by A10, A11; hence f . x = (g | (A . i)) . x by A13, FUNCT_1:49; ::_thesis: verum end; dom g = C . i by A7, FUNCT_2:def_1; then A14: dom (g | (A . i)) = A . i by A11, RELAT_1:62; thus (G || A) . i = g | (A . i) by A7, A9, MSAFREE:def_1 .= F . i by A8, A14, A12, FUNCT_1:2 ; ::_thesis: verum end; hence G || A = F by PBOOLE:3; ::_thesis: verum end; definition let I be set ; let A be ManySortedSet of I; let F be ManySortedFunction of I; funcF "" A -> ManySortedSet of I means :Def1: :: EQUATION:def 1 for i being set st i in I holds it . i = (F . i) " (A . i); existence ex b1 being ManySortedSet of I st for i being set st i in I holds b1 . i = (F . i) " (A . i) proof deffunc H1( set ) -> set = (F . \$1) " (A . \$1); ex f being ManySortedSet of I st for i being set st i in I holds f . i = H1(i) from PBOOLE:sch_4(); hence ex b1 being ManySortedSet of I st for i being set st i in I holds b1 . i = (F . i) " (A . i) ; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds b1 . i = (F . i) " (A . i) ) & ( for i being set st i in I holds b2 . i = (F . i) " (A . i) ) holds b1 = b2 proof let X, Y be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds X . i = (F . i) " (A . i) ) & ( for i being set st i in I holds Y . i = (F . i) " (A . i) ) implies X = Y ) assume that A1: for i being set st i in I holds X . i = (F . i) " (A . i) and A2: for i being set st i in I holds Y . i = (F . i) " (A . i) ; ::_thesis: X = Y now__::_thesis:_for_i_being_set_st_i_in_I_holds_ X_._i_=_Y_._i let i be set ; ::_thesis: ( i in I implies X . i = Y . i ) assume A3: i in I ; ::_thesis: X . i = Y . i hence X . i = (F . i) " (A . i) by A1 .= Y . i by A2, A3 ; ::_thesis: verum end; hence X = Y by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def1 defines "" EQUATION:def_1_:_ for I being set for A being ManySortedSet of I for F being ManySortedFunction of I for b4 being ManySortedSet of I holds ( b4 = F "" A iff for i being set st i in I holds b4 . i = (F . i) " (A . i) ); theorem :: EQUATION:7 for I being set for A, B, C being ManySortedSet of I for F being ManySortedFunction of A,B holds F .:.: C is ManySortedSubset of B proof let I be set ; ::_thesis: for A, B, C being ManySortedSet of I for F being ManySortedFunction of A,B holds F .:.: C is ManySortedSubset of B let A, B, C be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B holds F .:.: C is ManySortedSubset of B let F be ManySortedFunction of A,B; ::_thesis: F .:.: C is ManySortedSubset of B let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in I or (F .:.: C) . i c= B . i ) assume A1: i in I ; ::_thesis: (F .:.: C) . i c= B . i then reconsider J = I as non empty set ; reconsider j = i as Element of J by A1; reconsider A1 = A, B1 = B as ManySortedSet of J ; reconsider F1 = F as ManySortedFunction of A1,B1 ; (F1 . j) .: (C . j) c= B . j ; hence (F .:.: C) . i c= B . i by PBOOLE:def_20; ::_thesis: verum end; theorem :: EQUATION:8 for I being set for A, B, C being ManySortedSet of I for F being ManySortedFunction of A,B holds F "" C is ManySortedSubset of A proof let I be set ; ::_thesis: for A, B, C being ManySortedSet of I for F being ManySortedFunction of A,B holds F "" C is ManySortedSubset of A let A, B, C be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B holds F "" C is ManySortedSubset of A let F be ManySortedFunction of A,B; ::_thesis: F "" C is ManySortedSubset of A let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in I or (F "" C) . i c= A . i ) assume A1: i in I ; ::_thesis: (F "" C) . i c= A . i then reconsider J = I as non empty set ; reconsider j = i as Element of J by A1; reconsider A1 = A, B1 = B as ManySortedSet of J ; reconsider F1 = F as ManySortedFunction of A1,B1 ; (F1 . j) " (C . j) c= A . j ; hence (F "" C) . i c= A . i by Def1; ::_thesis: verum end; theorem :: EQUATION:9 for I being set for A, B being ManySortedSet of I for F being ManySortedFunction of A,B st F is "onto" holds F .:.: A = B proof let I be set ; ::_thesis: for A, B being ManySortedSet of I for F being ManySortedFunction of A,B st F is "onto" holds F .:.: A = B let A, B be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B st F is "onto" holds F .:.: A = B let F be ManySortedFunction of A,B; ::_thesis: ( F is "onto" implies F .:.: A = B ) assume A1: F is "onto" ; ::_thesis: F .:.: A = B now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (F_.:.:_A)_._i_=_B_._i let i be set ; ::_thesis: ( i in I implies (F .:.: A) . b1 = B . b1 ) assume A2: i in I ; ::_thesis: (F .:.: A) . b1 = B . b1 then A3: F . i is Function of (A . i),(B . i) by PBOOLE:def_15; percases not ( B . i = {} & not A . i = {} & not ( B . i = {} & not A . i = {} ) ) ; suppose ( B . i = {} implies A . i = {} ) ; ::_thesis: (F .:.: A) . b1 = B . b1 thus (F .:.: A) . i = (F . i) .: (A . i) by A2, PBOOLE:def_20 .= rng (F . i) by A3, RELSET_1:22 .= B . i by A1, A2, MSUALG_3:def_3 ; ::_thesis: verum end; supposeA4: ( B . i = {} & not A . i = {} ) ; ::_thesis: (F .:.: A) . b1 = B . b1 then A5: F . i = {} by A3; thus (F .:.: A) . i = (F . i) .: (A . i) by A2, PBOOLE:def_20 .= B . i by A4, A5 ; ::_thesis: verum end; end; end; hence F .:.: A = B by PBOOLE:3; ::_thesis: verum end; theorem :: EQUATION:10 for I being set for A, B being ManySortedSet of I for F being ManySortedFunction of A,B st A is_transformable_to B holds F "" B = A proof let I be set ; ::_thesis: for A, B being ManySortedSet of I for F being ManySortedFunction of A,B st A is_transformable_to B holds F "" B = A let A, B be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B st A is_transformable_to B holds F "" B = A let F be ManySortedFunction of A,B; ::_thesis: ( A is_transformable_to B implies F "" B = A ) assume A1: A is_transformable_to B ; ::_thesis: F "" B = A now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (F_""_B)_._i_=_A_._i let i be set ; ::_thesis: ( i in I implies (F "" B) . i = A . i ) assume A2: i in I ; ::_thesis: (F "" B) . i = A . i then A3: F . i is Function of (A . i),(B . i) by PBOOLE:def_15; A4: ( B . i = {} implies A . i = {} ) by A1, A2, PZFMISC1:def_3; thus (F "" B) . i = (F . i) " (B . i) by A2, Def1 .= A . i by A4, A3, FUNCT_2:40 ; ::_thesis: verum end; hence F "" B = A by PBOOLE:3; ::_thesis: verum end; theorem :: EQUATION:11 for I being set for A being ManySortedSet of I for F being ManySortedFunction of I st A c= rngs 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 A c= rngs F holds F .:.: (F "" A) = A let A be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of I st A c= rngs F holds F .:.: (F "" A) = A let F be ManySortedFunction of I; ::_thesis: ( A c= rngs F implies F .:.: (F "" A) = A ) assume A1: A c= rngs F ; ::_thesis: F .:.: (F "" A) = A 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 A2: i in I ; ::_thesis: (F .:.: (F "" A)) . i = A . i then A . i c= (rngs F) . i by A1, PBOOLE:def_2; then A3: A . i c= rng (F . i) by A2, MSSUBFAM:13; thus (F .:.: (F "" A)) . i = (F . i) .: ((F "" A) . i) by A2, PBOOLE:def_20 .= (F . i) .: ((F . i) " (A . i)) by A2, Def1 .= A . i by A3, FUNCT_1:77 ; ::_thesis: verum end; hence F .:.: (F "" A) = A by PBOOLE:3; ::_thesis: verum end; theorem :: EQUATION:12 for I being set for f being ManySortedFunction of I for X being ManySortedSet of I holds f .:.: X c= rngs f proof let I be set ; ::_thesis: for f being ManySortedFunction of I for X being ManySortedSet of I holds f .:.: X c= rngs f let f be ManySortedFunction of I; ::_thesis: for X being ManySortedSet of I holds f .:.: X c= rngs f let X be ManySortedSet of I; ::_thesis: f .:.: X c= rngs f let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (f .:.: X) . i c= (rngs f) . i ) assume A1: i in I ; ::_thesis: (f .:.: X) . i c= (rngs f) . i then (f .:.: X) . i = (f . i) .: (X . i) by PBOOLE:def_20; then (f .:.: X) . i c= rng (f . i) by RELAT_1:111; hence (f .:.: X) . i c= (rngs f) . i by A1, MSSUBFAM:13; ::_thesis: verum end; theorem Th13: :: EQUATION:13 for I being set for f being ManySortedFunction of I holds f .:.: (doms f) = rngs f proof let I be set ; ::_thesis: for f being ManySortedFunction of I holds f .:.: (doms f) = rngs f let f be ManySortedFunction of I; ::_thesis: f .:.: (doms f) = rngs f now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (f_.:.:_(doms_f))_._i_=_(rngs_f)_._i let i be set ; ::_thesis: ( i in I implies (f .:.: (doms f)) . i = (rngs f) . i ) assume A1: i in I ; ::_thesis: (f .:.: (doms f)) . i = (rngs f) . i hence (f .:.: (doms f)) . i = (f . i) .: ((doms f) . i) by PBOOLE:def_20 .= (f . i) .: (dom (f . i)) by A1, MSSUBFAM:14 .= rng (f . i) by RELAT_1:113 .= (rngs f) . i by A1, MSSUBFAM:13 ; ::_thesis: verum end; hence f .:.: (doms f) = rngs f by PBOOLE:3; ::_thesis: verum end; theorem Th14: :: EQUATION:14 for I being set for f being ManySortedFunction of I holds f "" (rngs f) = doms f proof let I be set ; ::_thesis: for f being ManySortedFunction of I holds f "" (rngs f) = doms f let f be ManySortedFunction of I; ::_thesis: f "" (rngs f) = doms f now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (f_""_(rngs_f))_._i_=_(doms_f)_._i let i be set ; ::_thesis: ( i in I implies (f "" (rngs f)) . i = (doms f) . i ) assume A1: i in I ; ::_thesis: (f "" (rngs f)) . i = (doms f) . i hence (f "" (rngs f)) . i = (f . i) " ((rngs f) . i) by Def1 .= (f . i) " (rng (f . i)) by A1, MSSUBFAM:13 .= dom (f . i) by RELAT_1:134 .= (doms f) . i by A1, MSSUBFAM:14 ; ::_thesis: verum end; hence f "" (rngs f) = doms f by PBOOLE:3; ::_thesis: verum end; theorem :: EQUATION:15 for I being set for A being ManySortedSet of I holds (id A) .:.: A = A proof let I be set ; ::_thesis: for A being ManySortedSet of I holds (id A) .:.: A = A let A be ManySortedSet of I; ::_thesis: (id A) .:.: A = A A1: rngs (id A) = A by EXTENS_1:9; doms (id A) = A by MSSUBFAM:17; hence (id A) .:.: A = A by A1, Th13; ::_thesis: verum end; theorem :: EQUATION:16 for I being set for A being ManySortedSet of I holds (id A) "" A = A proof let I be set ; ::_thesis: for A being ManySortedSet of I holds (id A) "" A = A let A be ManySortedSet of I; ::_thesis: (id A) "" A = A A1: rngs (id A) = A by EXTENS_1:9; doms (id A) = A by MSSUBFAM:17; hence (id A) "" A = A by A1, Th14; ::_thesis: verum end; begin theorem Th17: :: EQUATION:17 for S being non empty non void ManySortedSign for A being MSAlgebra over S holds A is MSSubAlgebra of MSAlgebra(# the Sorts of A, the Charact of A #) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra over S holds A is MSSubAlgebra of MSAlgebra(# the Sorts of A, the Charact of A #) let A be MSAlgebra over S; ::_thesis: A is MSSubAlgebra of MSAlgebra(# the Sorts of A, the Charact of A #) set IT = MSAlgebra(# the Sorts of A, the Charact of A #); A1: MSAlgebra(# the Sorts of A, the Charact of A #) is MSSubAlgebra of MSAlgebra(# the Sorts of A, the Charact of A #) by MSUALG_2:5; hence the Sorts of A is MSSubset of MSAlgebra(# the Sorts of A, the Charact of A #) by MSUALG_2:def_9; :: according to MSUALG_2:def_9 ::_thesis: for b1 being ManySortedSubset of the Sorts of MSAlgebra(# the Sorts of A, the Charact of A #) holds ( not b1 = the Sorts of A or ( b1 is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of A, the Charact of A #),b1) ) ) let C be MSSubset of MSAlgebra(# the Sorts of A, the Charact of A #); ::_thesis: ( not C = the Sorts of A or ( C is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of A, the Charact of A #),C) ) ) assume A2: C = the Sorts of A ; ::_thesis: ( C is opers_closed & the Charact of A = Opers (MSAlgebra(# the Sorts of A, the Charact of A #),C) ) hence C is opers_closed by A1, MSUALG_2:def_9; ::_thesis: the Charact of A = Opers (MSAlgebra(# the Sorts of A, the Charact of A #),C) thus the Charact of A = Opers (MSAlgebra(# the Sorts of A, the Charact of A #),C) by A1, A2, MSUALG_2:def_9; ::_thesis: verum end; theorem Th18: :: EQUATION:18 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for A being MSSubAlgebra of U0 for o being OperSymbol of S for x being set st x in Args (o,A) holds x in Args (o,U0) proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for A being MSSubAlgebra of U0 for o being OperSymbol of S for x being set st x in Args (o,A) holds x in Args (o,U0) let U0 be MSAlgebra over S; ::_thesis: for A being MSSubAlgebra of U0 for o being OperSymbol of S for x being set st x in Args (o,A) holds x in Args (o,U0) let A be MSSubAlgebra of U0; ::_thesis: for o being OperSymbol of S for x being set st x in Args (o,A) holds x in Args (o,U0) let o be OperSymbol of S; ::_thesis: for x being set st x in Args (o,A) holds x in Args (o,U0) let x be set ; ::_thesis: ( x in Args (o,A) implies x in Args (o,U0) ) assume A1: x in Args (o,A) ; ::_thesis: x in Args (o,U0) reconsider B0 = the Sorts of A as MSSubset of U0 by MSUALG_2:def_9; MSAlgebra(# the Sorts of U0, the Charact of U0 #) = MSAlgebra(# the Sorts of U0, the Charact of U0 #) ; then U0 is MSSubAlgebra of U0 by MSUALG_2:5; then reconsider B1 = the Sorts of U0 as MSSubset of U0 by MSUALG_2:def_9; B0 c= B1 by PBOOLE:def_18; then ((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o by MSUALG_2:2; hence x in Args (o,U0) by A1; ::_thesis: verum end; theorem Th19: :: EQUATION:19 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for A being MSSubAlgebra of U0 for o being OperSymbol of S for x being set st x in Args (o,A) holds (Den (o,A)) . x = (Den (o,U0)) . x proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for A being MSSubAlgebra of U0 for o being OperSymbol of S for x being set st x in Args (o,A) holds (Den (o,A)) . x = (Den (o,U0)) . x let U0 be MSAlgebra over S; ::_thesis: for A being MSSubAlgebra of U0 for o being OperSymbol of S for x being set st x in Args (o,A) holds (Den (o,A)) . x = (Den (o,U0)) . x let A be MSSubAlgebra of U0; ::_thesis: for o being OperSymbol of S for x being set st x in Args (o,A) holds (Den (o,A)) . x = (Den (o,U0)) . x let o be OperSymbol of S; ::_thesis: for x being set st x in Args (o,A) holds (Den (o,A)) . x = (Den (o,U0)) . x let x be set ; ::_thesis: ( x in Args (o,A) implies (Den (o,A)) . x = (Den (o,U0)) . x ) assume A1: x in Args (o,A) ; ::_thesis: (Den (o,A)) . x = (Den (o,U0)) . x reconsider B = the Sorts of A as MSSubset of U0 by MSUALG_2:def_9; B is opers_closed by MSUALG_2:def_9; then A2: B is_closed_on o by MSUALG_2:def_6; thus (Den (o,A)) . x = ((Opers (U0,B)) . o) . x by MSUALG_2:def_9 .= (o /. B) . x by MSUALG_2:def_8 .= ((Den (o,U0)) | (((B #) * the Arity of S) . o)) . x by A2, MSUALG_2:def_7 .= (Den (o,U0)) . x by A1, FUNCT_1:49 ; ::_thesis: verum end; theorem Th20: :: EQUATION:20 for I being set for S being non empty non void ManySortedSign for F being MSAlgebra-Family of I,S for B being MSSubAlgebra of product F for o being OperSymbol of S for x being set st x in Args (o,B) holds ( (Den (o,B)) . x is Function & (Den (o,(product F))) . x is Function ) proof let I be set ; ::_thesis: for S being non empty non void ManySortedSign for F being MSAlgebra-Family of I,S for B being MSSubAlgebra of product F for o being OperSymbol of S for x being set st x in Args (o,B) holds ( (Den (o,B)) . x is Function & (Den (o,(product F))) . x is Function ) let S be non empty non void ManySortedSign ; ::_thesis: for F being MSAlgebra-Family of I,S for B being MSSubAlgebra of product F for o being OperSymbol of S for x being set st x in Args (o,B) holds ( (Den (o,B)) . x is Function & (Den (o,(product F))) . x is Function ) let F be MSAlgebra-Family of I,S; ::_thesis: for B being MSSubAlgebra of product F for o being OperSymbol of S for x being set st x in Args (o,B) holds ( (Den (o,B)) . x is Function & (Den (o,(product F))) . x is Function ) let B be MSSubAlgebra of product F; ::_thesis: for o being OperSymbol of S for x being set st x in Args (o,B) holds ( (Den (o,B)) . x is Function & (Den (o,(product F))) . x is Function ) let o be OperSymbol of S; ::_thesis: for x being set st x in Args (o,B) holds ( (Den (o,B)) . x is Function & (Den (o,(product F))) . x is Function ) let x be set ; ::_thesis: ( x in Args (o,B) implies ( (Den (o,B)) . x is Function & (Den (o,(product F))) . x is Function ) ) set r = the_result_sort_of o; assume A1: x in Args (o,B) ; ::_thesis: ( (Den (o,B)) . x is Function & (Den (o,(product F))) . x is Function ) then x in Args (o,(product F)) by Th18; then (Den (o,(product F))) . x in product (Carrier (F,(the_result_sort_of o))) by PRALG_3:19; then (Den (o,B)) . x in product (Carrier (F,(the_result_sort_of o))) by A1, Th19; then reconsider p = (Den (o,B)) . x as Element of (SORTS F) . (the_result_sort_of o) by PRALG_2:def_10; A2: p is Function ; hence (Den (o,B)) . x is Function ; ::_thesis: (Den (o,(product F))) . x is Function thus (Den (o,(product F))) . x is Function by A1, A2, Th19; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let A be MSAlgebra over S; let B be MSSubAlgebra of A; func SuperAlgebraSet B -> set means :Def2: :: EQUATION:def 2 for x being set holds ( x in it iff ex C being strict MSSubAlgebra of A st ( x = C & B is MSSubAlgebra of C ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ex C being strict MSSubAlgebra of A st ( x = C & B is MSSubAlgebra of C ) ) proof defpred S1[ set ] means ex C being strict MSSubAlgebra of A st ( \$1 = C & B is MSSubAlgebra of C ); consider IT being set such that A1: for x being set holds ( x in IT iff ( x in MSSub A & S1[x] ) ) from XBOOLE_0:sch_1(); take IT ; ::_thesis: for x being set holds ( x in IT iff ex C being strict MSSubAlgebra of A st ( x = C & B is MSSubAlgebra of C ) ) let x be set ; ::_thesis: ( x in IT iff ex C being strict MSSubAlgebra of A st ( x = C & B is MSSubAlgebra of C ) ) thus ( x in IT implies ex C being strict MSSubAlgebra of A st ( x = C & B is MSSubAlgebra of C ) ) by A1; ::_thesis: ( ex C being strict MSSubAlgebra of A st ( x = C & B is MSSubAlgebra of C ) implies x in IT ) given C being strict MSSubAlgebra of A such that A2: x = C and A3: B is MSSubAlgebra of C ; ::_thesis: x in IT x in MSSub A by A2, MSUALG_2:def_19; hence x in IT by A1, A2, A3; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ex C being strict MSSubAlgebra of A st ( x = C & B is MSSubAlgebra of C ) ) ) & ( for x being set holds ( x in b2 iff ex C being strict MSSubAlgebra of A st ( x = C & B is MSSubAlgebra of C ) ) ) holds b1 = b2 proof defpred S1[ set ] means ex C being strict MSSubAlgebra of A st ( \$1 = C & B is MSSubAlgebra of C ); for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); hence for b1, b2 being set st ( for x being set holds ( x in b1 iff ex C being strict MSSubAlgebra of A st ( x = C & B is MSSubAlgebra of C ) ) ) & ( for x being set holds ( x in b2 iff ex C being strict MSSubAlgebra of A st ( x = C & B is MSSubAlgebra of C ) ) ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def2 defines SuperAlgebraSet EQUATION:def_2_:_ for S being non empty non void ManySortedSign for A being MSAlgebra over S for B being MSSubAlgebra of A for b4 being set holds ( b4 = SuperAlgebraSet B iff for x being set holds ( x in b4 iff ex C being strict MSSubAlgebra of A st ( x = C & B is MSSubAlgebra of C ) ) ); registration let S be non empty non void ManySortedSign ; let A be MSAlgebra over S; let B be MSSubAlgebra of A; cluster SuperAlgebraSet B -> non empty ; coherence not SuperAlgebraSet B is empty proof MSAlgebra(# the Sorts of B, the Charact of B #) is MSSubAlgebra of B by MSUALG_2:37; then A1: MSAlgebra(# the Sorts of B, the Charact of B #) is MSSubAlgebra of A by MSUALG_2:6; B is MSSubAlgebra of MSAlgebra(# the Sorts of B, the Charact of B #) by Th17; hence not SuperAlgebraSet B is empty by A1, Def2; ::_thesis: verum end; end; registration let S be non empty non void ManySortedSign ; cluster strict non-empty free for MSAlgebra over S; existence ex b1 being MSAlgebra over S st ( b1 is strict & b1 is non-empty & b1 is free ) proof set X = the V2() ManySortedSet of the carrier of S; take FreeMSA the V2() ManySortedSet of the carrier of S ; ::_thesis: ( FreeMSA the V2() ManySortedSet of the carrier of S is strict & FreeMSA the V2() ManySortedSet of the carrier of S is non-empty & FreeMSA the V2() ManySortedSet of the carrier of S is free ) thus ( FreeMSA the V2() ManySortedSet of the carrier of S is strict & FreeMSA the V2() ManySortedSet of the carrier of S is non-empty & FreeMSA the V2() ManySortedSet of the carrier of S is free ) ; ::_thesis: verum end; end; registration let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; let X be V2() V29() MSSubset of A; cluster GenMSAlg X -> finitely-generated ; coherence GenMSAlg X is finitely-generated proof percases ( not S is void or S is void ) ; :: according to MSAFREE2:def_10 case not S is void ; ::_thesis: for b1 being ManySortedSign holds ( not b1 = S or for b2 being MSAlgebra over b1 holds ( not b2 = GenMSAlg X or ex b3 being GeneratorSet of b2 st b3 is finite-yielding ) ) let S9 be non empty non void ManySortedSign ; ::_thesis: ( not S9 = S or for b1 being MSAlgebra over S9 holds ( not b1 = GenMSAlg X or ex b2 being GeneratorSet of b1 st b2 is finite-yielding ) ) assume A1: S9 = S ; ::_thesis: for b1 being MSAlgebra over S9 holds ( not b1 = GenMSAlg X or ex b2 being GeneratorSet of b1 st b2 is finite-yielding ) let H be MSAlgebra over S9; ::_thesis: ( not H = GenMSAlg X or ex b1 being GeneratorSet of H st b1 is finite-yielding ) assume A2: H = GenMSAlg X ; ::_thesis: ex b1 being GeneratorSet of H st b1 is finite-yielding then reconsider T = X as MSSubset of H by A1, MSUALG_2:def_17; GenMSAlg T = H by A1, A2, EXTENS_1:18; then reconsider T = T as GeneratorSet of H by A1, A2, MSAFREE:3; take T ; ::_thesis: T is finite-yielding thus T is finite-yielding ; ::_thesis: verum end; case S is void ; ::_thesis: the Sorts of (GenMSAlg X) is finite-yielding hence the Sorts of (GenMSAlg X) is finite-yielding ; ::_thesis: verum end; end; end; end; registration let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; cluster strict non-empty finitely-generated for MSSubAlgebra of A; existence ex b1 being MSSubAlgebra of A st ( b1 is strict & b1 is non-empty & b1 is finitely-generated ) proof set G = the V2() V29() ManySortedSubset of the Sorts of A; take GenMSAlg the V2() V29() ManySortedSubset of the Sorts of A ; ::_thesis: ( GenMSAlg the V2() V29() ManySortedSubset of the Sorts of A is strict & GenMSAlg the V2() V29() ManySortedSubset of the Sorts of A is non-empty & GenMSAlg the V2() V29() ManySortedSubset of the Sorts of A is finitely-generated ) thus ( GenMSAlg the V2() V29() ManySortedSubset of the Sorts of A is strict & GenMSAlg the V2() V29() ManySortedSubset of the Sorts of A is non-empty & GenMSAlg the V2() V29() ManySortedSubset of the Sorts of A is finitely-generated ) ; ::_thesis: verum end; end; registration let S be non empty non void ManySortedSign ; let A be feasible MSAlgebra over S; cluster feasible for MSSubAlgebra of A; existence ex b1 being MSSubAlgebra of A st b1 is feasible proof MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of A, the Charact of A #) ; then reconsider B = A as MSSubAlgebra of A by MSUALG_2:5; take B ; ::_thesis: B is feasible thus B is feasible ; ::_thesis: verum end; end; theorem Th21: :: EQUATION:21 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S for A being MSAlgebra over S for C being MSSubAlgebra of A for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds for h being ManySortedFunction of A,U0 for g being ManySortedFunction of C,U0 st g = h || D holds for o being OperSymbol of S for x being Element of Args (o,A) for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds h # x = g # y proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S for A being MSAlgebra over S for C being MSSubAlgebra of A for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds for h being ManySortedFunction of A,U0 for g being ManySortedFunction of C,U0 st g = h || D holds for o being OperSymbol of S for x being Element of Args (o,A) for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds h # x = g # y let U0 be non-empty MSAlgebra over S; ::_thesis: for A being MSAlgebra over S for C being MSSubAlgebra of A for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds for h being ManySortedFunction of A,U0 for g being ManySortedFunction of C,U0 st g = h || D holds for o being OperSymbol of S for x being Element of Args (o,A) for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds h # x = g # y let A be MSAlgebra over S; ::_thesis: for C being MSSubAlgebra of A for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds for h being ManySortedFunction of A,U0 for g being ManySortedFunction of C,U0 st g = h || D holds for o being OperSymbol of S for x being Element of Args (o,A) for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds h # x = g # y let C be MSSubAlgebra of A; ::_thesis: for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds for h being ManySortedFunction of A,U0 for g being ManySortedFunction of C,U0 st g = h || D holds for o being OperSymbol of S for x being Element of Args (o,A) for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds h # x = g # y let D be ManySortedSubset of the Sorts of A; ::_thesis: ( D = the Sorts of C implies for h being ManySortedFunction of A,U0 for g being ManySortedFunction of C,U0 st g = h || D holds for o being OperSymbol of S for x being Element of Args (o,A) for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds h # x = g # y ) assume A1: D = the Sorts of C ; ::_thesis: for h being ManySortedFunction of A,U0 for g being ManySortedFunction of C,U0 st g = h || D holds for o being OperSymbol of S for x being Element of Args (o,A) for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds h # x = g # y let h be ManySortedFunction of A,U0; ::_thesis: for g being ManySortedFunction of C,U0 st g = h || D holds for o being OperSymbol of S for x being Element of Args (o,A) for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds h # x = g # y let g be ManySortedFunction of C,U0; ::_thesis: ( g = h || D implies for o being OperSymbol of S for x being Element of Args (o,A) for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds h # x = g # y ) assume A2: g = h || D ; ::_thesis: for o being OperSymbol of S for x being Element of Args (o,A) for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds h # x = g # y let o be OperSymbol of S; ::_thesis: for x being Element of Args (o,A) for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds h # x = g # y let x be Element of Args (o,A); ::_thesis: for y being Element of Args (o,C) st Args (o,C) <> {} & x = y holds h # x = g # y let y be Element of Args (o,C); ::_thesis: ( Args (o,C) <> {} & x = y implies h # x = g # y ) assume that A3: Args (o,C) <> {} and A4: x = y ; ::_thesis: h # x = g # y set hx = h # x; set gy = g # y; set ar = the_arity_of o; A5: y in Args (o,A) by A3, Th18; then reconsider xx = x, yy = y as Function by MSUALG_6:1; A6: dom yy = dom (the_arity_of o) by A3, MSUALG_3:6; A7: dom xx = dom (the_arity_of o) by A5, MSUALG_3:6; A8: now__::_thesis:_for_n_being_set_st_n_in_dom_(the_arity_of_o)_holds_ (h_#_x)_._n_=_(g_#_y)_._n let n be set ; ::_thesis: ( n in dom (the_arity_of o) implies (h # x) . n = (g # y) . n ) assume A9: n in dom (the_arity_of o) ; ::_thesis: (h # x) . n = (g # y) . n then reconsider n9 = n as Nat ; reconsider hn = h . ((the_arity_of o) . n) as Function of ( the Sorts of A . ((the_arity_of o) . n)),( the Sorts of U0 . ((the_arity_of o) . n)) by A9, PARTFUN1:4, PBOOLE:def_15; (the_arity_of o) . n in the carrier of S by A9, PARTFUN1:4; then A10: g . ((the_arity_of o) . n9) = hn | (D . ((the_arity_of o) . n)) by A2, MSAFREE:def_1; dom ( the Sorts of C * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def_2; then xx . n in ( the Sorts of C * (the_arity_of o)) . n by A3, A4, A9, MSUALG_3:6; then A11: xx . n in D . ((the_arity_of o) . n) by A1, A9, FUNCT_1:13; thus (h # x) . n = (h # x) . n9 .= (h . ((the_arity_of o) /. n)) . (xx . n) by A5, A7, A9, MSUALG_3:24 .= (h . ((the_arity_of o) . n)) . (xx . n) by A9, PARTFUN1:def_6 .= (g . ((the_arity_of o) . n)) . (xx . n) by A10, A11, FUNCT_1:49 .= (g . ((the_arity_of o) /. n)) . (yy . n) by A4, A9, PARTFUN1:def_6 .= (g # y) . n9 by A3, A6, A9, MSUALG_3:24 .= (g # y) . n ; ::_thesis: verum end; ( dom (h # x) = dom (the_arity_of o) & dom (g # y) = dom (the_arity_of o) ) by MSUALG_3:6; hence h # x = g # y by A8, FUNCT_1:2; ::_thesis: verum end; theorem Th22: :: EQUATION:22 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S for A being feasible MSAlgebra over S for C being feasible MSSubAlgebra of A for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds for h being ManySortedFunction of A,U0 st h is_homomorphism A,U0 holds for g being ManySortedFunction of C,U0 st g = h || D holds g is_homomorphism C,U0 proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S for A being feasible MSAlgebra over S for C being feasible MSSubAlgebra of A for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds for h being ManySortedFunction of A,U0 st h is_homomorphism A,U0 holds for g being ManySortedFunction of C,U0 st g = h || D holds g is_homomorphism C,U0 let U0 be non-empty MSAlgebra over S; ::_thesis: for A being feasible MSAlgebra over S for C being feasible MSSubAlgebra of A for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds for h being ManySortedFunction of A,U0 st h is_homomorphism A,U0 holds for g being ManySortedFunction of C,U0 st g = h || D holds g is_homomorphism C,U0 let A be feasible MSAlgebra over S; ::_thesis: for C being feasible MSSubAlgebra of A for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds for h being ManySortedFunction of A,U0 st h is_homomorphism A,U0 holds for g being ManySortedFunction of C,U0 st g = h || D holds g is_homomorphism C,U0 let C be feasible MSSubAlgebra of A; ::_thesis: for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds for h being ManySortedFunction of A,U0 st h is_homomorphism A,U0 holds for g being ManySortedFunction of C,U0 st g = h || D holds g is_homomorphism C,U0 let D be ManySortedSubset of the Sorts of A; ::_thesis: ( D = the Sorts of C implies for h being ManySortedFunction of A,U0 st h is_homomorphism A,U0 holds for g being ManySortedFunction of C,U0 st g = h || D holds g is_homomorphism C,U0 ) assume A1: D = the Sorts of C ; ::_thesis: for h being ManySortedFunction of A,U0 st h is_homomorphism A,U0 holds for g being ManySortedFunction of C,U0 st g = h || D holds g is_homomorphism C,U0 let h be ManySortedFunction of A,U0; ::_thesis: ( h is_homomorphism A,U0 implies for g being ManySortedFunction of C,U0 st g = h || D holds g is_homomorphism C,U0 ) assume A2: h is_homomorphism A,U0 ; ::_thesis: for g being ManySortedFunction of C,U0 st g = h || D holds g is_homomorphism C,U0 let g be ManySortedFunction of C,U0; ::_thesis: ( g = h || D implies g is_homomorphism C,U0 ) assume A3: g = h || D ; ::_thesis: g is_homomorphism C,U0 let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,C) = {} or for b1 being Element of Args (o,C) holds (g . (the_result_sort_of o)) . ((Den (o,C)) . b1) = (Den (o,U0)) . (g # b1) ) assume A4: Args (o,C) <> {} ; ::_thesis: for b1 being Element of Args (o,C) holds (g . (the_result_sort_of o)) . ((Den (o,C)) . b1) = (Den (o,U0)) . (g # b1) let x be Element of Args (o,C); ::_thesis: (g . (the_result_sort_of o)) . ((Den (o,C)) . x) = (Den (o,U0)) . (g # x) reconsider y = x as Element of Args (o,A) by A4, Th18; set r = the_result_sort_of o; A5: x in Args (o,A) by A4, Th18; Result (o,C) <> {} by A4, MSUALG_6:def_1; then (Den (o,C)) . x in Result (o,C) by A4, FUNCT_2:5; then A6: (Den (o,C)) . x in the Sorts of C . ( the ResultSort of S . o) by FUNCT_2:15; (Den (o,A)) . x = (Den (o,C)) . x by A4, Th19; hence (g . (the_result_sort_of o)) . ((Den (o,C)) . x) = (h . (the_result_sort_of o)) . ((Den (o,A)) . x) by A1, A3, A6, INSTALG1:39 .= (Den (o,U0)) . (h # y) by A2, A5, MSUALG_3:def_7 .= (Den (o,U0)) . (g # x) by A1, A3, A4, Th21 ; ::_thesis: verum end; theorem :: EQUATION:23 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S for B being strict non-empty MSAlgebra over S for G being GeneratorSet of U0 for H being V2() GeneratorSet of B for f being ManySortedFunction of U0,B st H c= f .:.: G & f is_homomorphism U0,B holds f is_epimorphism U0,B proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S for B being strict non-empty MSAlgebra over S for G being GeneratorSet of U0 for H being V2() GeneratorSet of B for f being ManySortedFunction of U0,B st H c= f .:.: G & f is_homomorphism U0,B holds f is_epimorphism U0,B let U0 be non-empty MSAlgebra over S; ::_thesis: for B being strict non-empty MSAlgebra over S for G being GeneratorSet of U0 for H being V2() GeneratorSet of B for f being ManySortedFunction of U0,B st H c= f .:.: G & f is_homomorphism U0,B holds f is_epimorphism U0,B let B be strict non-empty MSAlgebra over S; ::_thesis: for G being GeneratorSet of U0 for H being V2() GeneratorSet of B for f being ManySortedFunction of U0,B st H c= f .:.: G & f is_homomorphism U0,B holds f is_epimorphism U0,B let G be GeneratorSet of U0; ::_thesis: for H being V2() GeneratorSet of B for f being ManySortedFunction of U0,B st H c= f .:.: G & f is_homomorphism U0,B holds f is_epimorphism U0,B let H be V2() GeneratorSet of B; ::_thesis: for f being ManySortedFunction of U0,B st H c= f .:.: G & f is_homomorphism U0,B holds f is_epimorphism U0,B let f be ManySortedFunction of U0,B; ::_thesis: ( H c= f .:.: G & f is_homomorphism U0,B implies f is_epimorphism U0,B ) assume that A1: H c= f .:.: G and A2: f is_homomorphism U0,B ; ::_thesis: f is_epimorphism U0,B reconsider I = the Sorts of (Image f) as V2() MSSubset of B by MSUALG_2:def_9; f .:.: G c= f .:.: the Sorts of U0 by EXTENS_1:2; then H c= f .:.: the Sorts of U0 by A1, PBOOLE:13; then H c= the Sorts of (Image f) by A2, MSUALG_3:def_12; then H is ManySortedSubset of the Sorts of (Image f) by PBOOLE:def_18; then A3: GenMSAlg H is MSSubAlgebra of GenMSAlg I by EXTENS_1:17; reconsider I1 = the Sorts of (Image f) as V2() MSSubset of (Image f) by PBOOLE:def_18; ( I is GeneratorSet of Image f & GenMSAlg I = GenMSAlg I1 ) by EXTENS_1:18, MSAFREE2:6; then GenMSAlg I = Image f by MSAFREE:3; then B is MSSubAlgebra of Image f by A3, MSAFREE:3; then Image f = B by MSUALG_2:7; hence f is_epimorphism U0,B by A2, MSUALG_3:19; ::_thesis: verum end; theorem Th24: :: EQUATION:24 for S being non empty non void ManySortedSign for U0, U1 being non-empty MSAlgebra over S for W being strict non-empty free MSAlgebra over S for F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 holds for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds ex H being ManySortedFunction of W,U0 st ( H is_homomorphism W,U0 & G = F ** H ) proof let S be non empty non void ManySortedSign ; ::_thesis: for U0, U1 being non-empty MSAlgebra over S for W being strict non-empty free MSAlgebra over S for F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 holds for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds ex H being ManySortedFunction of W,U0 st ( H is_homomorphism W,U0 & G = F ** H ) let U0, U1 be non-empty MSAlgebra over S; ::_thesis: for W being strict non-empty free MSAlgebra over S for F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 holds for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds ex H being ManySortedFunction of W,U0 st ( H is_homomorphism W,U0 & G = F ** H ) let W be strict non-empty free MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 holds for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds ex H being ManySortedFunction of W,U0 st ( H is_homomorphism W,U0 & G = F ** H ) let F be ManySortedFunction of U0,U1; ::_thesis: ( F is_epimorphism U0,U1 implies for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds ex H being ManySortedFunction of W,U0 st ( H is_homomorphism W,U0 & G = F ** H ) ) assume A1: F is_epimorphism U0,U1 ; ::_thesis: for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds ex H being ManySortedFunction of W,U0 st ( H is_homomorphism W,U0 & G = F ** H ) set sU0 = the Sorts of U0; set sU1 = the Sorts of U1; set I = the carrier of S; let G be ManySortedFunction of W,U1; ::_thesis: ( G is_homomorphism W,U1 implies ex H being ManySortedFunction of W,U0 st ( H is_homomorphism W,U0 & G = F ** H ) ) assume A2: G is_homomorphism W,U1 ; ::_thesis: ex H being ManySortedFunction of W,U0 st ( H is_homomorphism W,U0 & G = F ** H ) consider Gen being GeneratorSet of W such that A3: Gen is free by MSAFREE:def_6; defpred S1[ set , set , set ] means ex f being Function of ( the Sorts of U0 . \$3),( the Sorts of U1 . \$3) ex g being Function of (Gen . \$3),( the Sorts of U1 . \$3) st ( f = F . \$3 & g = (G || Gen) . \$3 & \$1 in f " {(g . \$2)} ); A4: for i being set st i in the carrier of S holds for x being set st x in Gen . i holds ex y being set st ( y in the Sorts of U0 . i & S1[y,x,i] ) proof let i be set ; ::_thesis: ( i in the carrier of S implies for x being set st x in Gen . i holds ex y being set st ( y in the Sorts of U0 . i & S1[y,x,i] ) ) assume A5: i in the carrier of S ; ::_thesis: for x being set st x in Gen . i holds ex y being set st ( y in the Sorts of U0 . i & S1[y,x,i] ) reconsider g = (G || Gen) . i as Function of (Gen . i),( the Sorts of U1 . i) by A5, PBOOLE:def_15; reconsider f = F . i as Function of ( the Sorts of U0 . i),( the Sorts of U1 . i) by A5, PBOOLE:def_15; let x be set ; ::_thesis: ( x in Gen . i implies ex y being set st ( y in the Sorts of U0 . i & S1[y,x,i] ) ) assume x in Gen . i ; ::_thesis: ex y being set st ( y in the Sorts of U0 . i & S1[y,x,i] ) then A6: g . x in the Sorts of U1 . i by A5, FUNCT_2:5; F is "onto" by A1, MSUALG_3:def_8; then rng (F . i) = the Sorts of U1 . i by A5, MSUALG_3:def_3; then f " {(g . x)} <> {} by A6, FUNCT_2:41; then consider y being set such that A7: y in f " {(g . x)} by XBOOLE_0:def_1; take y ; ::_thesis: ( y in the Sorts of U0 . i & S1[y,x,i] ) thus y in the Sorts of U0 . i by A7; ::_thesis: S1[y,x,i] thus S1[y,x,i] by A7; ::_thesis: verum end; consider H being ManySortedFunction of Gen, the Sorts of U0 such that A8: for i being set st i in the carrier of S holds ex h being Function of (Gen . i),( the Sorts of U0 . i) st ( h = H . i & ( for x being set st x in Gen . i holds S1[h . x,x,i] ) ) from MSSUBFAM:sch_1(A4); consider H1 being ManySortedFunction of W,U0 such that A9: H1 is_homomorphism W,U0 and A10: H1 || Gen = H by A3, MSAFREE:def_5; now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ (G_||_Gen)_._i_=_(F_**_H)_._i let i be set ; ::_thesis: ( i in the carrier of S implies (G || Gen) . i = (F ** H) . i ) assume A11: i in the carrier of S ; ::_thesis: (G || Gen) . i = (F ** H) . i then reconsider f9 = F . i as Function of ( the Sorts of U0 . i),( the Sorts of U1 . i) by PBOOLE:def_15; reconsider g9 = (G || Gen) . i as Function of (Gen . i),( the Sorts of U1 . i) by A11, PBOOLE:def_15; consider h being Function of (Gen . i),( the Sorts of U0 . i) such that A12: h = H . i and A13: for x being set st x in Gen . i holds ex f being Function of ( the Sorts of U0 . i),( the Sorts of U1 . i) ex g being Function of (Gen . i),( the Sorts of U1 . i) st ( f = F . i & g = (G || Gen) . i & h . x in f " {(g . x)} ) by A8, A11; A14: now__::_thesis:_for_x_being_set_st_x_in_Gen_._i_holds_ (f9_*_h)_._x_=_g9_._x let x be set ; ::_thesis: ( x in Gen . i implies (f9 * h) . x = g9 . x ) assume A15: x in Gen . i ; ::_thesis: (f9 * h) . x = g9 . x then consider f being Function of ( the Sorts of U0 . i),( the Sorts of U1 . i), g being Function of (Gen . i),( the Sorts of U1 . i) such that A16: ( f = F . i & g = (G || Gen) . i ) and A17: h . x in f " {(g . x)} by A13; f . (h . x) in {(g . x)} by A11, A17, FUNCT_2:38; then f . (h . x) = g . x by TARSKI:def_1; hence (f9 * h) . x = g9 . x by A15, A16, A17, FUNCT_2:15; ::_thesis: verum end; ( Gen . i = dom g9 & Gen . i = dom (f9 * h) ) by A11, FUNCT_2:def_1; then g9 = f9 * h by A14, FUNCT_1:2; hence (G || Gen) . i = (F ** H) . i by A11, A12, MSUALG_3:2; ::_thesis: verum end; then G || Gen = F ** (H1 || Gen) by A10, PBOOLE:3; then A18: G || Gen = (F ** H1) || Gen by EXTENS_1:4; take H1 ; ::_thesis: ( H1 is_homomorphism W,U0 & G = F ** H1 ) thus H1 is_homomorphism W,U0 by A9; ::_thesis: G = F ** H1 F is_homomorphism U0,U1 by A1, MSUALG_3:def_8; then F ** H1 is_homomorphism W,U1 by A9, MSUALG_3:10; hence G = F ** H1 by A2, A18, EXTENS_1:19; ::_thesis: verum end; theorem Th25: :: EQUATION:25 for S being non empty non void ManySortedSign for I being non empty finite set for A being non-empty MSAlgebra over S for F being MSAlgebra-Family of I,S st ( for i being Element of I ex C being strict non-empty finitely-generated MSSubAlgebra of A st C = F . i ) holds ex B being strict non-empty finitely-generated MSSubAlgebra of A st for i being Element of I holds F . i is MSSubAlgebra of B proof let S be non empty non void ManySortedSign ; ::_thesis: for I being non empty finite set for A being non-empty MSAlgebra over S for F being MSAlgebra-Family of I,S st ( for i being Element of I ex C being strict non-empty finitely-generated MSSubAlgebra of A st C = F . i ) holds ex B being strict non-empty finitely-generated MSSubAlgebra of A st for i being Element of I holds F . i is MSSubAlgebra of B let I be non empty finite set ; ::_thesis: for A being non-empty MSAlgebra over S for F being MSAlgebra-Family of I,S st ( for i being Element of I ex C being strict non-empty finitely-generated MSSubAlgebra of A st C = F . i ) holds ex B being strict non-empty finitely-generated MSSubAlgebra of A st for i being Element of I holds F . i is MSSubAlgebra of B let A be non-empty MSAlgebra over S; ::_thesis: for F being MSAlgebra-Family of I,S st ( for i being Element of I ex C being strict non-empty finitely-generated MSSubAlgebra of A st C = F . i ) holds ex B being strict non-empty finitely-generated MSSubAlgebra of A st for i being Element of I holds F . i is MSSubAlgebra of B let F be MSAlgebra-Family of I,S; ::_thesis: ( ( for i being Element of I ex C being strict non-empty finitely-generated MSSubAlgebra of A st C = F . i ) implies ex B being strict non-empty finitely-generated MSSubAlgebra of A st for i being Element of I holds F . i is MSSubAlgebra of B ) assume A1: for i being Element of I ex C being strict non-empty finitely-generated MSSubAlgebra of A st C = F . i ; ::_thesis: ex B being strict non-empty finitely-generated MSSubAlgebra of A st for i being Element of I holds F . i is MSSubAlgebra of B set Z = { C where C is Element of MSSub A : ex i being Element of I ex D being strict non-empty finitely-generated MSSubAlgebra of A st ( C = F . i & C = D ) } ; set J = the carrier of S; set m = the Element of I; consider W being strict non-empty finitely-generated MSSubAlgebra of A such that A2: W = F . the Element of I by A1; W is Element of MSSub A by MSUALG_2:def_19; then W in { C where C is Element of MSSub A : ex i being Element of I ex D being strict non-empty finitely-generated MSSubAlgebra of A st ( C = F . i & C = D ) } by A2; then reconsider Z = { C where C is Element of MSSub A : ex i being Element of I ex D being strict non-empty finitely-generated MSSubAlgebra of A st ( C = F . i & C = D ) } as non empty set ; defpred S1[ set , set ] means ex Q being strict non-empty MSSubAlgebra of A ex G being GeneratorSet of Q st ( \$1 = Q & \$2 = G & G is V2() & G is V29() ); A3: for a being Element of Z ex b being Element of Bool the Sorts of A st S1[a,b] proof let a be Element of Z; ::_thesis: ex b being Element of Bool the Sorts of A st S1[a,b] a in Z ; then consider C being Element of MSSub A such that A4: a = C and A5: ex i being Element of I ex D being strict non-empty finitely-generated MSSubAlgebra of A st ( C = F . i & C = D ) ; consider i being Element of I, D being strict non-empty finitely-generated MSSubAlgebra of A such that C = F . i and A6: C = D by A5; consider G being GeneratorSet of D such that A7: G is V29() by MSAFREE2:def_10; consider S being V2() V29() ManySortedSubset of the Sorts of D such that A8: G c= S by A7, MSUALG_9:7; the Sorts of D is MSSubset of A by MSUALG_2:def_9; then ( S c= the Sorts of D & the Sorts of D c= the Sorts of A ) by PBOOLE:def_18; then S c= the Sorts of A by PBOOLE:13; then S is ManySortedSubset of the Sorts of A by PBOOLE:def_18; then reconsider b = S as Element of Bool the Sorts of A by CLOSURE2:def_1; reconsider S = S as GeneratorSet of D by A8, MSSCYC_1:21; take b ; ::_thesis: S1[a,b] take D ; ::_thesis: ex G being GeneratorSet of D st ( a = D & b = G & G is V2() & G is V29() ) take S ; ::_thesis: ( a = D & b = S & S is V2() & S is V29() ) thus a = D by A4, A6; ::_thesis: ( b = S & S is V2() & S is V29() ) thus ( b = S & S is V2() & S is V29() ) ; ::_thesis: verum end; consider f being Function of Z,(Bool the Sorts of A) such that A9: for B being Element of Z holds S1[B,f . B] from FUNCT_2:sch_3(A3); deffunc H1( set ) -> set = union { a where a is Element of bool ( the Sorts of A . \$1) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . \$1 ) } ; consider SOR being ManySortedSet of the carrier of S such that A10: for j being set st j in the carrier of S holds SOR . j = H1(j) from PBOOLE:sch_4(); SOR is ManySortedSubset of the Sorts of A proof let j be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not j in the carrier of S or SOR . j c= the Sorts of A . j ) assume A11: j in the carrier of S ; ::_thesis: SOR . j c= the Sorts of A . j let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in SOR . j or q in the Sorts of A . j ) set UU = { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } ; assume q in SOR . j ; ::_thesis: q in the Sorts of A . j then q in union { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } by A10, A11; then consider w being set such that A12: q in w and A13: w in { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } by TARSKI:def_4; consider a being Element of bool ( the Sorts of A . j) such that A14: w = a and ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) by A13; thus q in the Sorts of A . j by A12, A14; ::_thesis: verum end; then reconsider SOR = SOR as MSSubset of A ; SOR is V2() proof set i = the Element of I; consider C being strict non-empty finitely-generated MSSubAlgebra of A such that A15: C = F . the Element of I by A1; C is Element of MSSub A by MSUALG_2:def_19; then A16: F . the Element of I in Z by A15; then A17: ex Q being strict non-empty MSSubAlgebra of A ex G being GeneratorSet of Q st ( F . the Element of I = Q & f . (F . the Element of I) = G & G is V2() & G is V29() ) by A9; then reconsider G1 = f . (F . the Element of I) as V29() Element of Bool the Sorts of A by A16, FUNCT_2:5; let j be set ; :: according to PBOOLE:def_13 ::_thesis: ( not j in the carrier of S or not SOR . j is empty ) assume A18: j in the carrier of S ; ::_thesis: not SOR . j is empty consider q being set such that A19: q in G1 . j by A18, A17, XBOOLE_0:def_1; set UU = { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } ; G1 c= the Sorts of A by PBOOLE:def_18; then G1 . j c= the Sorts of A . j by A18, PBOOLE:def_2; then G1 . j in { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } ; then q in union { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } by A19, TARSKI:def_4; hence not SOR . j is empty by A10, A18; ::_thesis: verum end; then reconsider SOR = SOR as V2() MSSubset of A ; A20: now__::_thesis:_for_j_being_set_st_j_in_the_carrier_of_S_holds_ not__{__a_where_a_is_Element_of_bool_(_the_Sorts_of_A_._j)_:_ex_i_being_Element_of_I_ex_K_being_ManySortedSet_of_the_carrier_of_S_st_ (_K_=_f_._(F_._i)_&_a_=_K_._j_)__}__is_empty set i = the Element of I; let j be set ; ::_thesis: ( j in the carrier of S implies not { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } is empty ) assume A21: j in the carrier of S ; ::_thesis: not { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } is empty set UU = { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } ; consider C being strict non-empty finitely-generated MSSubAlgebra of A such that A22: C = F . the Element of I by A1; C is Element of MSSub A by MSUALG_2:def_19; then A23: F . the Element of I in Z by A22; then ex Q being strict non-empty MSSubAlgebra of A ex G being GeneratorSet of Q st ( F . the Element of I = Q & f . (F . the Element of I) = G & G is V2() & G is V29() ) by A9; then reconsider G1 = f . (F . the Element of I) as V29() Element of Bool the Sorts of A by A23, FUNCT_2:5; G1 c= the Sorts of A by PBOOLE:def_18; then G1 . j c= the Sorts of A . j by A21, PBOOLE:def_2; then G1 . j in { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } ; hence not { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } is empty ; ::_thesis: verum end; SOR is V29() proof let j be set ; :: according to FINSET_1:def_5 ::_thesis: ( not j in the carrier of S or SOR . j is finite ) assume A24: j in the carrier of S ; ::_thesis: SOR . j is finite set UU = { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } ; reconsider VV = { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } as non empty set by A20, A24; A25: now__::_thesis:_ex_p_being_FinSequence_st_rng_p_=_VV defpred S2[ set , set ] means ex L being ManySortedSet of the carrier of S st ( f . (F . \$1) = L & \$2 = L . j ); consider r being FinSequence such that A26: rng r = I by FINSEQ_1:52; A27: for a being Element of I ex b being Element of VV st S2[a,b] proof let a be Element of I; ::_thesis: ex b being Element of VV st S2[a,b] consider W being strict non-empty finitely-generated MSSubAlgebra of A such that A28: W = F . a by A1; W is Element of MSSub A by MSUALG_2:def_19; then A29: W in Z by A28; then ex Q being strict non-empty MSSubAlgebra of A ex G being GeneratorSet of Q st ( W = Q & f . W = G & G is V2() & G is V29() ) by A9; then reconsider G1 = f . (F . a) as V29() Element of Bool the Sorts of A by A28, A29, FUNCT_2:5; G1 c= the Sorts of A by PBOOLE:def_18; then G1 . j c= the Sorts of A . j by A24, PBOOLE:def_2; then G1 . j in { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } ; then reconsider b = G1 . j as Element of VV ; take b ; ::_thesis: S2[a,b] take G1 ; ::_thesis: ( f . (F . a) = G1 & b = G1 . j ) thus ( f . (F . a) = G1 & b = G1 . j ) ; ::_thesis: verum end; consider h being Function of I,VV such that A30: for i being Element of I holds S2[i,h . i] from FUNCT_2:sch_3(A27); A31: rng r = dom h by A26, FUNCT_2:def_1; then reconsider p = h * r as FinSequence by FINSEQ_1:16; A32: VV c= rng p proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in VV or q in rng p ) assume q in VV ; ::_thesis: q in rng p then consider a being Element of bool ( the Sorts of A . j) such that A33: q = a and A34: ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) ; consider i being Element of I, K being ManySortedSet of the carrier of S such that A35: ( K = f . (F . i) & a = K . j ) by A34; A36: ( rng p = rng h & dom h = I ) by A31, FUNCT_2:def_1, RELAT_1:28; ex L being ManySortedSet of the carrier of S st ( f . (F . i) = L & h . i = L . j ) by A30; hence q in rng p by A33, A35, A36, FUNCT_1:def_3; ::_thesis: verum end; take p = p; ::_thesis: rng p = VV rng p c= rng h proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in rng p or q in rng h ) assume q in rng p ; ::_thesis: q in rng h hence q in rng h by FUNCT_1:14; ::_thesis: verum end; then rng p c= VV by XBOOLE_1:1; hence rng p = VV by A32, XBOOLE_0:def_10; ::_thesis: verum end; for x being set st x in { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } holds x is finite proof let x be set ; ::_thesis: ( x in { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } implies x is finite ) assume x in { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } ; ::_thesis: x is finite then consider a being Element of bool ( the Sorts of A . j) such that A37: x = a and A38: ex w being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . w) & a = K . j ) ; consider w being Element of I, K being ManySortedSet of the carrier of S such that A39: ( K = f . (F . w) & a = K . j ) by A38; A40: ex E being strict non-empty finitely-generated MSSubAlgebra of A st E = F . w by A1; then F . w is Element of MSSub A by MSUALG_2:def_19; then F . w in Z by A40; then S1[F . w,f . (F . w)] by A9; hence x is finite by A37, A39; ::_thesis: verum end; then union { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } is finite by A25, FINSET_1:7; hence SOR . j is finite by A10, A24; ::_thesis: verum end; then reconsider SOR = SOR as V2() V29() MSSubset of A ; take GenMSAlg SOR ; ::_thesis: for i being Element of I holds F . i is MSSubAlgebra of GenMSAlg SOR let i be Element of I; ::_thesis: F . i is MSSubAlgebra of GenMSAlg SOR consider C being strict non-empty finitely-generated MSSubAlgebra of A such that A41: C = F . i by A1; C is Element of MSSub A by MSUALG_2:def_19; then F . i in Z by A41; then consider Q being strict non-empty MSSubAlgebra of A, G being GeneratorSet of Q such that A42: F . i = Q and A43: f . (F . i) = G and A44: ( G is V2() & G is V29() ) by A9; the Sorts of Q is MSSubset of A by MSUALG_2:def_9; then ( G c= the Sorts of Q & the Sorts of Q c= the Sorts of A ) by PBOOLE:def_18; then A45: G c= the Sorts of A by PBOOLE:13; then reconsider G1 = G as V2() MSSubset of A by A44, PBOOLE:def_18; A46: G1 is ManySortedSubset of SOR proof let j be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not j in the carrier of S or G1 . j c= SOR . j ) assume A47: j in the carrier of S ; ::_thesis: G1 . j c= SOR . j set UU = { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } ; G1 . j c= the Sorts of A . j by A45, A47, PBOOLE:def_2; then A48: G1 . j in { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } by A43; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in G1 . j or q in SOR . j ) assume q in G1 . j ; ::_thesis: q in SOR . j then q in union { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st ( K = f . (F . i) & a = K . j ) } by A48, TARSKI:def_4; hence q in SOR . j by A10, A47; ::_thesis: verum end; C = GenMSAlg G by A41, A42, MSAFREE:3 .= GenMSAlg G1 by EXTENS_1:18 ; hence F . i is MSSubAlgebra of GenMSAlg SOR by A41, A46, EXTENS_1:17; ::_thesis: verum end; theorem Th26: :: EQUATION:26 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S for A, B being strict non-empty finitely-generated MSSubAlgebra of U0 ex M being strict non-empty finitely-generated MSSubAlgebra of U0 st ( A is MSSubAlgebra of M & B is MSSubAlgebra of M ) proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S for A, B being strict non-empty finitely-generated MSSubAlgebra of U0 ex M being strict non-empty finitely-generated MSSubAlgebra of U0 st ( A is MSSubAlgebra of M & B is MSSubAlgebra of M ) let U0 be non-empty MSAlgebra over S; ::_thesis: for A, B being strict non-empty finitely-generated MSSubAlgebra of U0 ex M being strict non-empty finitely-generated MSSubAlgebra of U0 st ( A is MSSubAlgebra of M & B is MSSubAlgebra of M ) let A, B be strict non-empty finitely-generated MSSubAlgebra of U0; ::_thesis: ex M being strict non-empty finitely-generated MSSubAlgebra of U0 st ( A is MSSubAlgebra of M & B is MSSubAlgebra of M ) defpred S1[ set , set ] means ( ( \$1 = 0 implies \$2 = A ) & ( \$1 = 1 implies \$2 = B ) ); A1: for i being set st i in {0,1} holds ex j being set st S1[i,j] proof let i be set ; ::_thesis: ( i in {0,1} implies ex j being set st S1[i,j] ) assume A2: i in {0,1} ; ::_thesis: ex j being set st S1[i,j] percases ( i = 0 or i = 1 ) by A2, TARSKI:def_2; supposeA3: i = 0 ; ::_thesis: ex j being set st S1[i,j] take A ; ::_thesis: S1[i,A] thus S1[i,A] by A3; ::_thesis: verum end; supposeA4: i = 1 ; ::_thesis: ex j being set st S1[i,j] take B ; ::_thesis: S1[i,B] thus S1[i,B] by A4; ::_thesis: verum end; end; end; consider F being ManySortedSet of {0,1} such that A5: for i being set st i in {0,1} holds S1[i,F . i] from PBOOLE:sch_3(A1); F is MSAlgebra-Family of {0,1},S proof let i be set ; :: according to PRALG_2:def_5 ::_thesis: ( not i in {0,1} or F . i is MSAlgebra over S ) assume A6: i in {0,1} ; ::_thesis: F . i is MSAlgebra over S then A7: ( i = 1 implies F . i = B ) by A5; ( i = 0 implies F . i = A ) by A5, A6; hence F . i is MSAlgebra over S by A6, A7, TARSKI:def_2; ::_thesis: verum end; then reconsider F = F as MSAlgebra-Family of {0,1},S ; for i being Element of {0,1} ex C being strict non-empty finitely-generated MSSubAlgebra of U0 st C = F . i proof let i be Element of {0,1}; ::_thesis: ex C being strict non-empty finitely-generated MSSubAlgebra of U0 st C = F . i percases ( i = 0 or i = 1 ) by TARSKI:def_2; supposeA8: i = 0 ; ::_thesis: ex C being strict non-empty finitely-generated MSSubAlgebra of U0 st C = F . i take A ; ::_thesis: A = F . i thus A = F . i by A5, A8; ::_thesis: verum end; supposeA9: i = 1 ; ::_thesis: ex C being strict non-empty finitely-generated MSSubAlgebra of U0 st C = F . i take B ; ::_thesis: B = F . i thus B = F . i by A5, A9; ::_thesis: verum end; end; end; then consider M being strict non-empty finitely-generated MSSubAlgebra of U0 such that A10: for i being Element of {0,1} holds F . i is MSSubAlgebra of M by Th25; take M ; ::_thesis: ( A is MSSubAlgebra of M & B is MSSubAlgebra of M ) A11: 0 in {0,1} by TARSKI:def_2; then F . 0 = A by A5; hence A is MSSubAlgebra of M by A10, A11; ::_thesis: B is MSSubAlgebra of M A12: 1 in {0,1} by TARSKI:def_2; then F . 1 = B by A5; hence B is MSSubAlgebra of M by A10, A12; ::_thesis: verum end; theorem :: EQUATION:27 for SG being non empty non void ManySortedSign for AG being non-empty MSAlgebra over SG for C being set st C = { A where A is Element of MSSub AG : ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = A } holds for F being MSAlgebra-Family of C,SG st ( for c being set st c in C holds c = F . c ) holds ex PS being strict non-empty MSSubAlgebra of product F ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG proof let SG be non empty non void ManySortedSign ; ::_thesis: for AG being non-empty MSAlgebra over SG for C being set st C = { A where A is Element of MSSub AG : ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = A } holds for F being MSAlgebra-Family of C,SG st ( for c being set st c in C holds c = F . c ) holds ex PS being strict non-empty MSSubAlgebra of product F ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG let AG be non-empty MSAlgebra over SG; ::_thesis: for C being set st C = { A where A is Element of MSSub AG : ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = A } holds for F being MSAlgebra-Family of C,SG st ( for c being set st c in C holds c = F . c ) holds ex PS being strict non-empty MSSubAlgebra of product F ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG let C be set ; ::_thesis: ( C = { A where A is Element of MSSub AG : ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = A } implies for F being MSAlgebra-Family of C,SG st ( for c being set st c in C holds c = F . c ) holds ex PS being strict non-empty MSSubAlgebra of product F ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG ) assume A1: C = { A where A is Element of MSSub AG : ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = A } ; ::_thesis: for F being MSAlgebra-Family of C,SG st ( for c being set st c in C holds c = F . c ) holds ex PS being strict non-empty MSSubAlgebra of product F ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG A2: now__::_thesis:_for_A_being_strict_non-empty_finitely-generated_MSSubAlgebra_of_AG_holds_A_in_C let A be strict non-empty finitely-generated MSSubAlgebra of AG; ::_thesis: A in C A in MSSub AG by MSUALG_2:def_19; hence A in C by A1; ::_thesis: verum end; then reconsider CC = C as non empty set ; set T = the strict non-empty finitely-generated MSSubAlgebra of AG; set I = the carrier of SG; let F be MSAlgebra-Family of C,SG; ::_thesis: ( ( for c being set st c in C holds c = F . c ) implies ex PS being strict non-empty MSSubAlgebra of product F ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG ) assume A3: for c being set st c in C holds c = F . c ; ::_thesis: ex PS being strict non-empty MSSubAlgebra of product F ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG reconsider FF = F as MSAlgebra-Family of CC,SG ; set pr = product FF; defpred S1[ set , set ] means ex t being SortSymbol of SG ex f being Element of (SORTS FF) . t ex A being strict non-empty finitely-generated MSSubAlgebra of AG st ( t = \$1 & f = \$2 & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds f . A = f . B ) ); consider SOR being ManySortedSet of the carrier of SG such that A4: for i being set st i in the carrier of SG holds for e being set holds ( e in SOR . i iff ( e in (SORTS FF) . i & S1[i,e] ) ) from PBOOLE:sch_2(); SOR is MSSubset of (product FF) proof let i be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not i in the carrier of SG or SOR . i c= the Sorts of (product FF) . i ) assume A5: i in the carrier of SG ; ::_thesis: SOR . i c= the Sorts of (product FF) . i let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in SOR . i or e in the Sorts of (product FF) . i ) assume e in SOR . i ; ::_thesis: e in the Sorts of (product FF) . i hence e in the Sorts of (product FF) . i by A4, A5; ::_thesis: verum end; then reconsider SOR = SOR as MSSubset of (product FF) ; SOR is opers_closed proof let o be OperSymbol of SG; :: according to MSUALG_2:def_6 ::_thesis: SOR is_closed_on o set r = the_result_sort_of o; set ar = the_arity_of o; let q be set ; :: according to TARSKI:def_3,MSUALG_2:def_5 ::_thesis: ( not q in proj2 ((Den (o,(product FF))) | (( the Arity of SG * (SOR #)) . o)) or q in ( the ResultSort of SG * SOR) . o ) assume A6: q in rng ((Den (o,(product FF))) | (((SOR #) * the Arity of SG) . o)) ; ::_thesis: q in ( the ResultSort of SG * SOR) . o reconsider q1 = q as Element of (SORTS FF) . (the_result_sort_of o) by A6, PRALG_2:3; consider g being set such that A7: g in dom ((Den (o,(product FF))) | (((SOR #) * the Arity of SG) . o)) and A8: q = ((Den (o,(product FF))) | (((SOR #) * the Arity of SG) . o)) . g by A6, FUNCT_1:def_3; A9: q = (Den (o,(product FF))) . g by A7, A8, FUNCT_1:47; A10: g in ((SOR #) * the Arity of SG) . o by A7; g in dom (Den (o,(product FF))) by A7, RELAT_1:57; then reconsider g = g as Element of Args (o,(product FF)) ; S1[ the_result_sort_of o,q] proof take the_result_sort_of o ; ::_thesis: ex f being Element of (SORTS FF) . (the_result_sort_of o) ex A being strict non-empty finitely-generated MSSubAlgebra of AG st ( the_result_sort_of o = the_result_sort_of o & f = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds f . A = f . B ) ) take q1 ; ::_thesis: ex A being strict non-empty finitely-generated MSSubAlgebra of AG st ( the_result_sort_of o = the_result_sort_of o & q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds q1 . A = q1 . B ) ) percases ( the_arity_of o = {} or the_arity_of o <> {} ) ; supposeA11: the_arity_of o = {} ; ::_thesis: ex A being strict non-empty finitely-generated MSSubAlgebra of AG st ( the_result_sort_of o = the_result_sort_of o & q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds q1 . A = q1 . B ) ) set A = the strict non-empty finitely-generated MSSubAlgebra of AG; Args (o, the strict non-empty finitely-generated MSSubAlgebra of AG) = {{}} by A11, PRALG_2:4; then A12: {} in Args (o, the strict non-empty finitely-generated MSSubAlgebra of AG) by TARSKI:def_1; take the strict non-empty finitely-generated MSSubAlgebra of AG ; ::_thesis: ( the_result_sort_of o = the_result_sort_of o & q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B holds q1 . the strict non-empty finitely-generated MSSubAlgebra of AG = q1 . B ) ) thus the_result_sort_of o = the_result_sort_of o ; ::_thesis: ( q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B holds q1 . the strict non-empty finitely-generated MSSubAlgebra of AG = q1 . B ) ) thus q1 = q ; ::_thesis: for B being strict non-empty finitely-generated MSSubAlgebra of AG st the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B holds q1 . the strict non-empty finitely-generated MSSubAlgebra of AG = q1 . B let B be strict non-empty finitely-generated MSSubAlgebra of AG; ::_thesis: ( the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B implies q1 . the strict non-empty finitely-generated MSSubAlgebra of AG = q1 . B ) assume the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B ; ::_thesis: q1 . the strict non-empty finitely-generated MSSubAlgebra of AG = q1 . B Args (o,B) = {{}} by A11, PRALG_2:4; then A13: {} in Args (o,B) by TARSKI:def_1; B in MSSub AG by MSUALG_2:def_19; then A14: B in CC by A1; the strict non-empty finitely-generated MSSubAlgebra of AG in MSSub AG by MSUALG_2:def_19; then the strict non-empty finitely-generated MSSubAlgebra of AG in CC by A1; then reconsider iA = the strict non-empty finitely-generated MSSubAlgebra of AG, iB = B as Element of CC by A14; A15: iA = FF . iA by A3; A16: iB = FF . iB by A3; Args (o,(product FF)) = {{}} by A11, PRALG_2:4; then A17: g = {} by TARSKI:def_1; hence q1 . the strict non-empty finitely-generated MSSubAlgebra of AG = (const (o,(product FF))) . iA by A9, PRALG_3:def_1 .= const (o,(FF . iA)) by A11, PRALG_3:9 .= (Den (o,(FF . iA))) . {} by PRALG_3:def_1 .= (Den (o,AG)) . {} by A15, A12, Th19 .= (Den (o,(FF . iB))) . {} by A16, A13, Th19 .= const (o,(FF . iB)) by PRALG_3:def_1 .= (const (o,(product FF))) . iB by A11, PRALG_3:9 .= q1 . B by A9, A17, PRALG_3:def_1 ; ::_thesis: verum end; supposeA18: the_arity_of o <> {} ; ::_thesis: ex A being strict non-empty finitely-generated MSSubAlgebra of AG st ( the_result_sort_of o = the_result_sort_of o & q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds q1 . A = q1 . B ) ) then reconsider domar = dom (the_arity_of o) as non empty finite set ; defpred S2[ set , set ] means ex gn being Function ex A being strict non-empty finitely-generated MSSubAlgebra of AG st ( gn = g . \$1 & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds gn . A = gn . B ) & \$2 = A ); g in (SOR #) . ( the Arity of SG . o) by A10, FUNCT_2:15; then A19: g in product (SOR * (the_arity_of o)) by FINSEQ_2:def_5; then A20: dom (SOR * (the_arity_of o)) = dom g by CARD_3:9 .= domar by MSUALG_3:6 ; A21: for a being Element of domar ex b being Element of MSSub AG st S2[a,b] proof let n be Element of domar; ::_thesis: ex b being Element of MSSub AG st S2[n,b] g . n in (SOR * (the_arity_of o)) . n by A19, A20, CARD_3:9; then ( (the_arity_of o) . n in the carrier of SG & g . n in SOR . ((the_arity_of o) . n) ) by FUNCT_1:13, PARTFUN1:4; then consider s being SortSymbol of SG, f being Element of (SORTS FF) . s, A being strict non-empty finitely-generated MSSubAlgebra of AG such that s = (the_arity_of o) . n and A22: f = g . n and A23: for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds f . A = f . B by A4; reconsider b = A as Element of MSSub AG by MSUALG_2:def_19; take b ; ::_thesis: S2[n,b] take f ; ::_thesis: ex A being strict non-empty finitely-generated MSSubAlgebra of AG st ( f = g . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds f . A = f . B ) & b = A ) take A ; ::_thesis: ( f = g . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds f . A = f . B ) & b = A ) thus f = g . n by A22; ::_thesis: ( ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds f . A = f . B ) & b = A ) thus for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds f . A = f . B by A23; ::_thesis: b = A thus b = A ; ::_thesis: verum end; consider KK being Function of domar,(MSSub AG) such that A24: for n being Element of domar holds S2[n,KK . n] from FUNCT_2:sch_3(A21); reconsider KK = KK as ManySortedSet of domar ; KK is MSAlgebra-Family of domar,SG proof let n be set ; :: according to PRALG_2:def_5 ::_thesis: ( not n in domar or KK . n is MSAlgebra over SG ) assume n in domar ; ::_thesis: KK . n is MSAlgebra over SG then ex gn being Function ex A being strict non-empty finitely-generated MSSubAlgebra of AG st ( gn = g . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds gn . A = gn . B ) & KK . n = A ) by A24; hence KK . n is MSAlgebra over SG ; ::_thesis: verum end; then reconsider KK = KK as MSAlgebra-Family of domar,SG ; for n being Element of domar ex C being strict non-empty finitely-generated MSSubAlgebra of AG st C = KK . n proof let n be Element of domar; ::_thesis: ex C being strict non-empty finitely-generated MSSubAlgebra of AG st C = KK . n ex gn being Function ex A being strict non-empty finitely-generated MSSubAlgebra of AG st ( gn = g . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds gn . A = gn . B ) & KK . n = A ) by A24; hence ex C being strict non-empty finitely-generated MSSubAlgebra of AG st C = KK . n ; ::_thesis: verum end; then consider K being strict non-empty finitely-generated MSSubAlgebra of AG such that A25: for n being Element of domar holds KK . n is MSSubAlgebra of K by Th25; take K ; ::_thesis: ( the_result_sort_of o = the_result_sort_of o & q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st K is MSSubAlgebra of B holds q1 . K = q1 . B ) ) thus the_result_sort_of o = the_result_sort_of o ; ::_thesis: ( q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st K is MSSubAlgebra of B holds q1 . K = q1 . B ) ) thus q1 = q ; ::_thesis: for B being strict non-empty finitely-generated MSSubAlgebra of AG st K is MSSubAlgebra of B holds q1 . K = q1 . B let B be strict non-empty finitely-generated MSSubAlgebra of AG; ::_thesis: ( K is MSSubAlgebra of B implies q1 . K = q1 . B ) assume A26: K is MSSubAlgebra of B ; ::_thesis: q1 . K = q1 . B K in MSSub AG by MSUALG_2:def_19; then A27: K in CC by A1; B in MSSub AG by MSUALG_2:def_19; then B in CC by A1; then reconsider iB = B, iK = K as Element of CC by A27; A28: g in Funcs ((dom (the_arity_of o)),(Funcs (CC,(union { ( the Sorts of (FF . i) . s) where i is Element of CC, s is Element of the carrier of SG : verum } )))) by PRALG_3:14; then A29: dom ((commute g) . iB) = domar by Th3; A30: dom ((commute g) . iK) = domar by A28, Th3; A31: for n being set st n in dom ((commute g) . iK) holds ((commute g) . iB) . n = ((commute g) . iK) . n proof let x be set ; ::_thesis: ( x in dom ((commute g) . iK) implies ((commute g) . iB) . x = ((commute g) . iK) . x ) assume A32: x in dom ((commute g) . iK) ; ::_thesis: ((commute g) . iB) . x = ((commute g) . iK) . x then consider gn being Function, A being strict non-empty finitely-generated MSSubAlgebra of AG such that A33: gn = g . x and A34: ( ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds gn . A = gn . B ) & KK . x = A ) by A24, A30; A35: KK . x is MSSubAlgebra of K by A25, A30, A32; thus ((commute g) . iB) . x = gn . iB by A30, A32, A33, PRALG_3:21 .= gn . A by A26, A34, A35, MSUALG_2:6 .= gn . iK by A25, A30, A32, A34 .= ((commute g) . iK) . x by A30, A32, A33, PRALG_3:21 ; ::_thesis: verum end; A36: iK = FF . iK by A3; A37: (commute g) . iK is Element of Args (o,(FF . iK)) by A18, PRALG_3:20; A38: (commute g) . iB is Element of Args (o,(FF . iB)) by A18, PRALG_3:20; A39: iB = FF . iB by A3; thus q1 . K = (Den (o,(FF . iK))) . ((commute g) . iK) by A9, A18, PRALG_3:22 .= (Den (o,AG)) . ((commute g) . iK) by A36, A37, Th19 .= (Den (o,AG)) . ((commute g) . iB) by A28, A29, A31, Th3, FUNCT_1:2 .= (Den (o,(FF . iB))) . ((commute g) . iB) by A39, A38, Th19 .= q1 . B by A9, A18, PRALG_3:22 ; ::_thesis: verum end; end; end; then q in SOR . (the_result_sort_of o) by A4; hence q in ( the ResultSort of SG * SOR) . o by FUNCT_2:15; ::_thesis: verum end; then A40: (product FF) | SOR = MSAlgebra(# SOR,(Opers ((product FF),SOR)) #) by MSUALG_2:def_15; defpred S2[ set , set , set ] means ex s being SortSymbol of SG ex f being Element of (SORTS FF) . s ex A being strict non-empty finitely-generated MSSubAlgebra of AG st ( s = \$3 & f = \$2 & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds f . A = f . B ) & \$1 = f . A ); SOR is V2() proof defpred S3[ set ] means ex C being strict non-empty MSSubAlgebra of AG st ( \$1 = C & C is finitely-generated ); let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in the carrier of SG or not SOR . i is empty ) consider ST1 being set such that A41: for x being set holds ( x in ST1 iff ( x in SuperAlgebraSet the strict non-empty finitely-generated MSSubAlgebra of AG & S3[x] ) ) from XBOOLE_0:sch_1(); A42: ST1 c= CC proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in ST1 or q in CC ) assume q in ST1 ; ::_thesis: q in CC then A43: ex C being strict non-empty MSSubAlgebra of AG st ( q = C & C is finitely-generated ) by A41; then q in MSSub AG by MSUALG_2:def_19; hence q in CC by A1, A43; ::_thesis: verum end; defpred S4[ set , set ] means ex K being MSSubAlgebra of AG ex t being set st ( \$1 = K & t in the Sorts of K . i & \$2 = t ); assume A44: i in the carrier of SG ; ::_thesis: not SOR . i is empty then consider x being set such that A45: x in the Sorts of the strict non-empty finitely-generated MSSubAlgebra of AG . i by XBOOLE_0:def_1; reconsider s = i as SortSymbol of SG by A44; A46: for c being set st c in CC holds ex j being set st S4[c,j] proof let c be set ; ::_thesis: ( c in CC implies ex j being set st S4[c,j] ) assume c in CC ; ::_thesis: ex j being set st S4[c,j] then consider C being Element of MSSub AG such that A47: c = C and A48: ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = C by A1; consider R being strict non-empty finitely-generated MSSubAlgebra of AG such that A49: R = C by A48; consider t being set such that A50: t in the Sorts of R . i by A44, XBOOLE_0:def_1; take t ; ::_thesis: S4[c,t] take R ; ::_thesis: ex t being set st ( c = R & t in the Sorts of R . i & t = t ) take t ; ::_thesis: ( c = R & t in the Sorts of R . i & t = t ) thus c = R by A47, A49; ::_thesis: ( t in the Sorts of R . i & t = t ) thus ( t in the Sorts of R . i & t = t ) by A50; ::_thesis: verum end; consider f being ManySortedSet of CC such that A51: for c being set st c in CC holds S4[c,f . c] from PBOOLE:sch_3(A46); set g = f +* (ST1 --> x); A52: dom (ST1 --> x) = ST1 by FUNCOP_1:13; A53: for a being set st a in dom (Carrier (FF,s)) holds (f +* (ST1 --> x)) . a in (Carrier (FF,s)) . a proof let a be set ; ::_thesis: ( a in dom (Carrier (FF,s)) implies (f +* (ST1 --> x)) . a in (Carrier (FF,s)) . a ) assume a in dom (Carrier (FF,s)) ; ::_thesis: (f +* (ST1 --> x)) . a in (Carrier (FF,s)) . a then A54: a in CC ; then A55: ex U0 being MSAlgebra over SG st ( U0 = FF . a & (Carrier (FF,s)) . a = the Sorts of U0 . s ) by PRALG_2:def_9; consider K being MSSubAlgebra of AG, t being set such that A56: ( a = K & t in the Sorts of K . i ) and A57: f . a = t by A51, A54; percases ( a in ST1 or not a in ST1 ) ; supposeA58: a in ST1 ; ::_thesis: (f +* (ST1 --> x)) . a in (Carrier (FF,s)) . a then a in dom (ST1 --> x) by FUNCOP_1:13; then (f +* (ST1 --> x)) . a = (ST1 --> x) . a by FUNCT_4:13; then A59: (f +* (ST1 --> x)) . a = x by A58, FUNCOP_1:7; a in SuperAlgebraSet the strict non-empty finitely-generated MSSubAlgebra of AG by A41, A58; then consider M being strict MSSubAlgebra of AG such that A60: a = M and A61: the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of M by Def2; the Sorts of the strict non-empty finitely-generated MSSubAlgebra of AG is ManySortedSubset of the Sorts of M by A61, MSUALG_2:def_9; then the Sorts of the strict non-empty finitely-generated MSSubAlgebra of AG c= the Sorts of M by PBOOLE:def_18; then the Sorts of the strict non-empty finitely-generated MSSubAlgebra of AG . i c= the Sorts of M . i by A44, PBOOLE:def_2; then x in the Sorts of M . i by A45; hence (f +* (ST1 --> x)) . a in (Carrier (FF,s)) . a by A3, A54, A55, A59, A60; ::_thesis: verum end; suppose not a in ST1 ; ::_thesis: (f +* (ST1 --> x)) . a in (Carrier (FF,s)) . a then (f +* (ST1 --> x)) . a = t by A52, A57, FUNCT_4:11; hence (f +* (ST1 --> x)) . a in (Carrier (FF,s)) . a by A3, A54, A55, A56; ::_thesis: verum end; end; end; dom (f +* (ST1 --> x)) = (dom f) \/ (dom (ST1 --> x)) by FUNCT_4:def_1 .= CC \/ (dom (ST1 --> x)) by PARTFUN1:def_2 .= CC \/ ST1 by FUNCOP_1:13 .= CC by A42, XBOOLE_1:12 .= dom (Carrier (FF,s)) by PARTFUN1:def_2 ; then A62: f +* (ST1 --> x) in product (Carrier (FF,s)) by A53, CARD_3:9; S1[i,f +* (ST1 --> x)] proof reconsider g1 = f +* (ST1 --> x) as Element of (SORTS FF) . s by A62, PRALG_2:def_10; take s ; ::_thesis: ex f being Element of (SORTS FF) . s ex A being strict non-empty finitely-generated MSSubAlgebra of AG st ( s = i & f = f +* (ST1 --> x) & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds f . A = f . B ) ) take g1 ; ::_thesis: ex A being strict non-empty finitely-generated MSSubAlgebra of AG st ( s = i & g1 = f +* (ST1 --> x) & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds g1 . A = g1 . B ) ) take the strict non-empty finitely-generated MSSubAlgebra of AG ; ::_thesis: ( s = i & g1 = f +* (ST1 --> x) & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B holds g1 . the strict non-empty finitely-generated MSSubAlgebra of AG = g1 . B ) ) thus s = i ; ::_thesis: ( g1 = f +* (ST1 --> x) & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B holds g1 . the strict non-empty finitely-generated MSSubAlgebra of AG = g1 . B ) ) thus g1 = f +* (ST1 --> x) ; ::_thesis: for B being strict non-empty finitely-generated MSSubAlgebra of AG st the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B holds g1 . the strict non-empty finitely-generated MSSubAlgebra of AG = g1 . B let B be strict non-empty finitely-generated MSSubAlgebra of AG; ::_thesis: ( the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B implies g1 . the strict non-empty finitely-generated MSSubAlgebra of AG = g1 . B ) assume the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B ; ::_thesis: g1 . the strict non-empty finitely-generated MSSubAlgebra of AG = g1 . B then B in SuperAlgebraSet the strict non-empty finitely-generated MSSubAlgebra of AG by Def2; then A63: B in ST1 by A41; the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of the strict non-empty finitely-generated MSSubAlgebra of AG by MSUALG_2:5; then the strict non-empty finitely-generated MSSubAlgebra of AG in SuperAlgebraSet the strict non-empty finitely-generated MSSubAlgebra of AG by Def2; then A64: the strict non-empty finitely-generated MSSubAlgebra of AG in ST1 by A41; hence g1 . the strict non-empty finitely-generated MSSubAlgebra of AG = (ST1 --> x) . the strict non-empty finitely-generated MSSubAlgebra of AG by A52, FUNCT_4:13 .= x by A64, FUNCOP_1:7 .= (ST1 --> x) . B by A63, FUNCOP_1:7 .= g1 . B by A52, A63, FUNCT_4:13 ; ::_thesis: verum end; hence not SOR . i is empty by A4; ::_thesis: verum end; then reconsider PS = (product FF) | SOR as strict non-empty MSSubAlgebra of product F by A40, MSUALG_1:def_3; A65: now__::_thesis:_for_s_being_SortSymbol_of_SG for_f_being_Element_of_(SORTS_FF)_._s for_A_being_strict_non-empty_finitely-generated_MSSubAlgebra_of_AG_holds_f_._A_in_the_Sorts_of_AG_._s let s be SortSymbol of SG; ::_thesis: for f being Element of (SORTS FF) . s for A being strict non-empty finitely-generated MSSubAlgebra of AG holds f . A in the Sorts of AG . s let f be Element of (SORTS FF) . s; ::_thesis: for A being strict non-empty finitely-generated MSSubAlgebra of AG holds f . A in the Sorts of AG . s let A be strict non-empty finitely-generated MSSubAlgebra of AG; ::_thesis: f . A in the Sorts of AG . s A66: dom (Carrier (FF,s)) = CC by PARTFUN1:def_2; A in MSSub AG by MSUALG_2:def_19; then A67: A in dom (Carrier (FF,s)) by A1, A66; then consider U0 being MSAlgebra over SG such that A68: U0 = FF . A and A69: (Carrier (FF,s)) . A = the Sorts of U0 . s by PRALG_2:def_9; (SORTS FF) . s = product (Carrier (FF,s)) by PRALG_2:def_10; then A70: f . A in (Carrier (FF,s)) . A by A67, CARD_3:9; FF . A = A by A3, A67; then the Sorts of U0 is ManySortedSubset of the Sorts of AG by A68, MSUALG_2:def_9; then the Sorts of U0 c= the Sorts of AG by PBOOLE:def_18; then the Sorts of U0 . s c= the Sorts of AG . s by PBOOLE:def_2; hence f . A in the Sorts of AG . s by A69, A70; ::_thesis: verum end; A71: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_SG_holds_ for_x_being_set_st_x_in_the_Sorts_of_PS_._i_holds_ ex_y_being_set_st_ (_y_in_the_Sorts_of_AG_._i_&_S2[y,x,i]_) let i be set ; ::_thesis: ( i in the carrier of SG implies for x being set st x in the Sorts of PS . i holds ex y being set st ( y in the Sorts of AG . i & S2[y,x,i] ) ) assume A72: i in the carrier of SG ; ::_thesis: for x being set st x in the Sorts of PS . i holds ex y being set st ( y in the Sorts of AG . i & S2[y,x,i] ) let x be set ; ::_thesis: ( x in the Sorts of PS . i implies ex y being set st ( y in the Sorts of AG . i & S2[y,x,i] ) ) assume x in the Sorts of PS . i ; ::_thesis: ex y being set st ( y in the Sorts of AG . i & S2[y,x,i] ) then consider s being SortSymbol of SG, f being Element of (SORTS FF) . s, A being strict non-empty finitely-generated MSSubAlgebra of AG such that A73: s = i and A74: ( f = x & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds f . A = f . B ) ) by A4, A40, A72; take y = f . A; ::_thesis: ( y in the Sorts of AG . i & S2[y,x,i] ) thus y in the Sorts of AG . i by A65, A73; ::_thesis: S2[y,x,i] thus S2[y,x,i] by A73, A74; ::_thesis: verum end; consider BA being ManySortedFunction of PS,AG such that A75: for i being set st i in the carrier of SG holds ex g being Function of ( the Sorts of PS . i),( the Sorts of AG . i) st ( g = BA . i & ( for x being set st x in the Sorts of PS . i holds S2[g . x,x,i] ) ) from MSSUBFAM:sch_1(A71); take PS ; ::_thesis: ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG take BA ; ::_thesis: BA is_epimorphism PS,AG thus BA is_homomorphism PS,AG :: according to MSUALG_3:def_8 ::_thesis: BA is "onto" proof let o be OperSymbol of SG; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,PS) = {} or for b1 being Element of Args (o,PS) holds (BA . (the_result_sort_of o)) . ((Den (o,PS)) . b1) = (Den (o,AG)) . (BA # b1) ) assume Args (o,PS) <> {} ; ::_thesis: for b1 being Element of Args (o,PS) holds (BA . (the_result_sort_of o)) . ((Den (o,PS)) . b1) = (Den (o,AG)) . (BA # b1) let k be Element of Args (o,PS); ::_thesis: (BA . (the_result_sort_of o)) . ((Den (o,PS)) . k) = (Den (o,AG)) . (BA # k) set r = the_result_sort_of o; set ar = the_arity_of o; consider g being Function of ( the Sorts of PS . (the_result_sort_of o)),( the Sorts of AG . (the_result_sort_of o)) such that A76: g = BA . (the_result_sort_of o) and A77: for k being set st k in the Sorts of PS . (the_result_sort_of o) holds S2[g . k,k, the_result_sort_of o] by A75; consider s being SortSymbol of SG, f being Element of (SORTS FF) . s, A being strict non-empty finitely-generated MSSubAlgebra of AG such that s = the_result_sort_of o and A78: f = (Den (o,PS)) . k and A79: for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds f . A = f . B and A80: g . ((Den (o,PS)) . k) = f . A by A77, MSUALG_9:18; percases ( the_arity_of o = {} or the_arity_of o <> {} ) ; supposeA81: the_arity_of o = {} ; ::_thesis: (BA . (the_result_sort_of o)) . ((Den (o,PS)) . k) = (Den (o,AG)) . (BA # k) A in MSSub AG by MSUALG_2:def_19; then A in CC by A1; then reconsider iA = A as Element of CC ; reconsider ff1 = (Den (o,(product FF))) . k as Function by Th20; A82: (Den (o,(product FF))) . {} = const (o,(product FF)) by PRALG_3:def_1; Args (o,A) = {{}} by A81, PRALG_2:4; then A83: {} in Args (o,A) by TARSKI:def_1; A84: Args (o,PS) = {{}} by A81, PRALG_2:4; then A85: k = {} by TARSKI:def_1; thus (BA . (the_result_sort_of o)) . ((Den (o,PS)) . k) = ff1 . A by A76, A78, A80, Th19 .= (const (o,(product FF))) . iA by A84, A82, TARSKI:def_1 .= const (o,(FF . iA)) by A81, PRALG_3:9 .= (Den (o,(FF . iA))) . {} by PRALG_3:def_1 .= (Den (o,A)) . {} by A3 .= (Den (o,AG)) . {} by A83, Th19 .= (Den (o,AG)) . (BA # k) by A81, A85, PRALG_3:11 ; ::_thesis: verum end; supposeA86: the_arity_of o <> {} ; ::_thesis: (BA . (the_result_sort_of o)) . ((Den (o,PS)) . k) = (Den (o,AG)) . (BA # k) then reconsider domar = dom (the_arity_of o) as non empty finite set ; defpred S3[ set , set ] means ex kn being Function ex A being strict non-empty finitely-generated MSSubAlgebra of AG st ( kn = k . \$1 & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds kn . A = kn . B ) & (BA . ((the_arity_of o) . \$1)) . kn = kn . A & \$2 = A ); A87: for n being Element of domar ex b being Element of MSSub AG st S3[n,b] proof let n be Element of domar; ::_thesis: ex b being Element of MSSub AG st S3[n,b] consider g being Function of ( the Sorts of PS . ((the_arity_of o) . n)),( the Sorts of AG . ((the_arity_of o) . n)) such that A88: g = BA . ((the_arity_of o) . n) and A89: for x being set st x in the Sorts of PS . ((the_arity_of o) . n) holds S2[g . x,x,(the_arity_of o) . n] by A75, PARTFUN1:4; k . n in the Sorts of PS . ((the_arity_of o) /. n) by MSUALG_6:2; then k . n in the Sorts of PS . ((the_arity_of o) . n) by PARTFUN1:def_6; then consider s being SortSymbol of SG, f being Element of (SORTS FF) . s, A being strict non-empty finitely-generated MSSubAlgebra of AG such that s = (the_arity_of o) . n and A90: f = k . n and A91: for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds f . A = f . B and A92: g . (k . n) = f . A by A89; reconsider b = A as Element of MSSub AG by MSUALG_2:def_19; take b ; ::_thesis: S3[n,b] take f ; ::_thesis: ex A being strict non-empty finitely-generated MSSubAlgebra of AG st ( f = k . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds f . A = f . B ) & (BA . ((the_arity_of o) . n)) . f = f . A & b = A ) take A ; ::_thesis: ( f = k . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds f . A = f . B ) & (BA . ((the_arity_of o) . n)) . f = f . A & b = A ) thus f = k . n by A90; ::_thesis: ( ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds f . A = f . B ) & (BA . ((the_arity_of o) . n)) . f = f . A & b = A ) thus for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds f . A = f . B by A91; ::_thesis: ( (BA . ((the_arity_of o) . n)) . f = f . A & b = A ) thus (BA . ((the_arity_of o) . n)) . f = f . A by A88, A90, A92; ::_thesis: b = A thus b = A ; ::_thesis: verum end; consider KK being Function of domar,(MSSub AG) such that A93: for n being Element of domar holds S3[n,KK . n] from FUNCT_2:sch_3(A87); reconsider KK = KK as ManySortedSet of domar ; KK is MSAlgebra-Family of domar,SG proof let n be set ; :: according to PRALG_2:def_5 ::_thesis: ( not n in domar or KK . n is MSAlgebra over SG ) assume n in domar ; ::_thesis: KK . n is MSAlgebra over SG then ex kn being Function ex A being strict non-empty finitely-generated MSSubAlgebra of AG st ( kn = k . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds kn . A = kn . B ) & (BA . ((the_arity_of o) . n)) . kn = kn . A & KK . n = A ) by A93; hence KK . n is MSAlgebra over SG ; ::_thesis: verum end; then reconsider KK = KK as MSAlgebra-Family of domar,SG ; for n being Element of domar ex C being strict non-empty finitely-generated MSSubAlgebra of AG st C = KK . n proof let n be Element of domar; ::_thesis: ex C being strict non-empty finitely-generated MSSubAlgebra of AG st C = KK . n ex kn being Function ex A being strict non-empty finitely-generated MSSubAlgebra of AG st ( kn = k . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds kn . A = kn . B ) & (BA . ((the_arity_of o) . n)) . kn = kn . A & KK . n = A ) by A93; hence ex C being strict non-empty finitely-generated MSSubAlgebra of AG st C = KK . n ; ::_thesis: verum end; then consider K being strict non-empty finitely-generated MSSubAlgebra of AG such that A94: for n being Element of domar holds KK . n is MSSubAlgebra of K by Th25; consider MAX being strict non-empty finitely-generated MSSubAlgebra of AG such that A95: A is MSSubAlgebra of MAX and A96: K is MSSubAlgebra of MAX by Th26; MAX in MSSub AG by MSUALG_2:def_19; then MAX in CC by A1; then reconsider iA = MAX as Element of CC ; A97: k in Args (o,(product FF)) by Th18; then A98: (commute k) . iA is Element of Args (o,(FF . iA)) by A86, PRALG_3:20; then (commute k) . iA in Args (o,(FF . iA)) ; then A99: (commute k) . iA in Args (o,MAX) by A3; A100: k in Funcs ((dom (the_arity_of o)),(Funcs (CC,(union { ( the Sorts of (FF . i) . m) where i is Element of CC, m is Element of the carrier of SG : verum } )))) by A97, PRALG_3:14; then A101: dom ((commute k) . iA) = domar by Th3; A102: for n being set st n in dom ((commute k) . iA) holds (BA # k) . n = ((commute k) . iA) . n proof set fs = (commute k) . iA; reconsider fs = (commute k) . iA as Element of Args (o,MAX) by A3, A98; let n be set ; ::_thesis: ( n in dom ((commute k) . iA) implies (BA # k) . n = ((commute k) . iA) . n ) assume A103: n in dom ((commute k) . iA) ; ::_thesis: (BA # k) . n = ((commute k) . iA) . n then reconsider arn = (the_arity_of o) . n as SortSymbol of SG by A101, PARTFUN1:4; n in Seg (len fs) by A103, FINSEQ_1:def_3; then reconsider n9 = n as Nat ; consider kn being Function, Ki being strict non-empty finitely-generated MSSubAlgebra of AG such that A104: kn = k . n and A105: for B being strict non-empty finitely-generated MSSubAlgebra of AG st Ki is MSSubAlgebra of B holds kn . Ki = kn . B and A106: (BA . arn) . kn = kn . Ki and A107: KK . n = Ki by A93, A101, A103; A108: Ki is MSSubAlgebra of K by A94, A101, A103, A107; dom k = domar by A100, FUNCT_2:92; hence (BA # k) . n = (BA . ((the_arity_of o) /. n9)) . (k . n) by A101, A103, MSUALG_3:def_6 .= kn . (KK . n) by A101, A103, A104, A106, A107, PARTFUN1:def_6 .= kn . iA by A96, A105, A107, A108, MSUALG_2:6 .= ((commute k) . iA) . n by A97, A101, A103, A104, PRALG_3:21 ; ::_thesis: verum end; reconsider ff1 = (Den (o,(product FF))) . k as Function by Th20; A109: dom (BA # k) = domar by MSUALG_6:2; thus (BA . (the_result_sort_of o)) . ((Den (o,PS)) . k) = f . MAX by A76, A79, A80, A95 .= ff1 . MAX by A78, Th19 .= (Den (o,(FF . iA))) . ((commute k) . iA) by A86, A97, PRALG_3:22 .= (Den (o,MAX)) . ((commute k) . iA) by A3 .= (Den (o,AG)) . ((commute k) . iA) by A99, Th19 .= (Den (o,AG)) . (BA # k) by A100, A109, A102, Th3, FUNCT_1:2 ; ::_thesis: verum end; end; end; let i be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not i in the carrier of SG or proj2 (BA . i) = the Sorts of AG . i ) assume i in the carrier of SG ; ::_thesis: proj2 (BA . i) = the Sorts of AG . i then reconsider s = i as SortSymbol of SG ; consider ff being set such that A110: ff in the Sorts of PS . s by XBOOLE_0:def_1; rng (BA . s) c= the Sorts of AG . s ; hence rng (BA . i) c= the Sorts of AG . i ; :: according to XBOOLE_0:def_10 ::_thesis: the Sorts of AG . i c= proj2 (BA . i) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the Sorts of AG . i or y in proj2 (BA . i) ) assume A111: y in the Sorts of AG . i ; ::_thesis: y in proj2 (BA . i) A112: (SORTS FF) . s = product (Carrier (FF,s)) by PRALG_2:def_10; then ff in product (Carrier (FF,s)) by A4, A40, A110; then consider aa being Function such that ff = aa and A113: dom aa = dom (Carrier (FF,s)) and A114: for x being set st x in dom (Carrier (FF,s)) holds aa . x in (Carrier (FF,s)) . x by CARD_3:def_5; defpred S3[ set ] means ex Axx being MSSubAlgebra of AG st ( Axx = \$1 & y in the Sorts of Axx . s ); consider WW being set such that A115: for a being set holds ( a in WW iff ( a in CC & S3[a] ) ) from XBOOLE_0:sch_1(); set XX = aa +* (WW --> y); A116: dom (WW --> y) = WW by FUNCOP_1:13; A117: for xx being Element of CC st S3[xx] holds (aa +* (WW --> y)) . xx = y proof let xx be Element of CC; ::_thesis: ( S3[xx] implies (aa +* (WW --> y)) . xx = y ) assume S3[xx] ; ::_thesis: (aa +* (WW --> y)) . xx = y then A118: xx in WW by A115; hence (aa +* (WW --> y)) . xx = (WW --> y) . xx by A116, FUNCT_4:13 .= y by A118, FUNCOP_1:7 ; ::_thesis: verum end; A119: dom (Carrier (FF,s)) = CC by PARTFUN1:def_2; A120: for x being set st x in dom (Carrier (FF,s)) holds (aa +* (WW --> y)) . x in (Carrier (FF,s)) . x proof let x be set ; ::_thesis: ( x in dom (Carrier (FF,s)) implies (aa +* (WW --> y)) . x in (Carrier (FF,s)) . x ) assume A121: x in dom (Carrier (FF,s)) ; ::_thesis: (aa +* (WW --> y)) . x in (Carrier (FF,s)) . x then consider C being Element of MSSub AG such that A122: x = C and A123: ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = C by A1, A119; consider R being strict non-empty finitely-generated MSSubAlgebra of AG such that A124: R = C by A123; A125: R in CC by A1, A124; then A126: ( ex U0 being MSAlgebra over SG st ( U0 = FF . R & (Carrier (FF,s)) . R = the Sorts of U0 . s ) & FF . R = R ) by A3, PRALG_2:def_9; percases ( S3[x] or not S3[x] ) ; suppose S3[x] ; ::_thesis: (aa +* (WW --> y)) . x in (Carrier (FF,s)) . x hence (aa +* (WW --> y)) . x in (Carrier (FF,s)) . x by A117, A122, A124, A125, A126; ::_thesis: verum end; suppose not S3[x] ; ::_thesis: (aa +* (WW --> y)) . x in (Carrier (FF,s)) . x then not x in WW by A115; then (aa +* (WW --> y)) . x = aa . x by A116, FUNCT_4:11; hence (aa +* (WW --> y)) . x in (Carrier (FF,s)) . x by A114, A121; ::_thesis: verum end; end; end; A127: WW c= CC proof let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in WW or w in CC ) assume w in WW ; ::_thesis: w in CC hence w in CC by A115; ::_thesis: verum end; set L = the V2() V29() MSSubset of AG; A128: dom (BA . s) = the Sorts of PS . s by FUNCT_2:def_1; set SY = {s} --> {y}; dom ( the V2() V29() MSSubset of AG +* ({s} --> {y})) = (dom the V2() V29() MSSubset of AG) \/ (dom ({s} --> {y})) by FUNCT_4:def_1 .= the carrier of SG \/ (dom ({s} --> {y})) by PARTFUN1:def_2 .= the carrier of SG \/ {s} by FUNCOP_1:13 .= the carrier of SG by ZFMISC_1:40 ; then reconsider Y = the V2() V29() MSSubset of AG +* ({s} --> {y}) as ManySortedSet of the carrier of SG by PARTFUN1:def_2, RELAT_1:def_18; A129: s in {s} by TARSKI:def_1; dom ({s} --> {y}) = {s} by FUNCOP_1:13; then A130: Y . s = ({s} --> {y}) . s by A129, FUNCT_4:13 .= {y} by A129, FUNCOP_1:7 ; A131: now__::_thesis:_for_k_being_set_st_k_in_the_carrier_of_SG_&_k_<>_s_holds_ Y_._k_=_the_V2()_V29()_MSSubset_of_AG_._k let k be set ; ::_thesis: ( k in the carrier of SG & k <> s implies Y . k = the V2() V29() MSSubset of AG . k ) assume that k in the carrier of SG and A132: k <> s ; ::_thesis: Y . k = the V2() V29() MSSubset of AG . k not k in dom ({s} --> {y}) by A132, TARSKI:def_1; hence Y . k = the V2() V29() MSSubset of AG . k by FUNCT_4:11; ::_thesis: verum end; Y is ManySortedSubset of the Sorts of AG proof let j be set ; :: according to PBOOLE:def_2,PBOOLE:def_18 ::_thesis: ( not j in the carrier of SG or Y . j c= the Sorts of AG . j ) assume A133: j in the carrier of SG ; ::_thesis: Y . j c= the Sorts of AG . j let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y . j or x in the Sorts of AG . j ) assume A134: x in Y . j ; ::_thesis: x in the Sorts of AG . j percases ( j <> s or j = s ) ; supposeA135: j <> s ; ::_thesis: x in the Sorts of AG . j the V2() V29() MSSubset of AG c= the Sorts of AG by PBOOLE:def_18; then A136: the V2() V29() MSSubset of AG . j c= the Sorts of AG . j by A133, PBOOLE:def_2; x in the V2() V29() MSSubset of AG . j by A131, A133, A134, A135; hence x in the Sorts of AG . j by A136; ::_thesis: verum end; suppose j = s ; ::_thesis: x in the Sorts of AG . j hence x in the Sorts of AG . j by A111, A130, A134, TARSKI:def_1; ::_thesis: verum end; end; end; then reconsider Y = Y as MSSubset of AG ; Y is V2() proof let j be set ; :: according to PBOOLE:def_13 ::_thesis: ( not j in the carrier of SG or not Y . j is empty ) assume A137: j in the carrier of SG ; ::_thesis: not Y . j is empty percases ( j <> s or j = s ) ; suppose j <> s ; ::_thesis: not Y . j is empty then Y . j = the V2() V29() MSSubset of AG . j by A131, A137; hence not Y . j is empty by A137; ::_thesis: verum end; suppose j = s ; ::_thesis: not Y . j is empty hence not Y . j is empty by A130; ::_thesis: verum end; end; end; then reconsider Y = Y as V2() MSSubset of AG ; Y is V29() proof let j be set ; :: according to FINSET_1:def_5 ::_thesis: ( not j in the carrier of SG or Y . j is finite ) assume A138: j in the carrier of SG ; ::_thesis: Y . j is finite percases ( j <> s or j = s ) ; suppose j <> s ; ::_thesis: Y . j is finite then Y . j = the V2() V29() MSSubset of AG . j by A131, A138; hence Y . j is finite ; ::_thesis: verum end; suppose j = s ; ::_thesis: Y . j is finite hence Y . j is finite by A130; ::_thesis: verum end; end; end; then reconsider Y = Y as V2() V29() MSSubset of AG ; Y is MSSubset of (GenMSAlg Y) by MSUALG_2:def_17; then Y c= the Sorts of (GenMSAlg Y) by PBOOLE:def_18; then A139: Y . s c= the Sorts of (GenMSAlg Y) . s by PBOOLE:def_2; dom (aa +* (WW --> y)) = (dom aa) \/ (dom (WW --> y)) by FUNCT_4:def_1 .= CC \/ (dom (WW --> y)) by A113, PARTFUN1:def_2 .= CC \/ WW by FUNCOP_1:13 .= CC by A127, XBOOLE_1:12 ; then reconsider XX = aa +* (WW --> y) as Element of (SORTS FF) . s by A112, A119, A120, CARD_3:9; consider h being Function of ( the Sorts of PS . s),( the Sorts of AG . s) such that A140: h = BA . s and A141: for x being set st x in the Sorts of PS . s holds S2[h . x,x,s] by A75; A142: y in Y . s by A130, TARSKI:def_1; then A143: y in the Sorts of (GenMSAlg Y) . s by A139; S1[s,XX] proof take s ; ::_thesis: ex f being Element of (SORTS FF) . s ex A being strict non-empty finitely-generated MSSubAlgebra of AG st ( s = s & f = XX & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds f . A = f . B ) ) take XX ; ::_thesis: ex A being strict non-empty finitely-generated MSSubAlgebra of AG st ( s = s & XX = XX & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds XX . A = XX . B ) ) take TT = GenMSAlg Y; ::_thesis: ( s = s & XX = XX & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st TT is MSSubAlgebra of B holds XX . TT = XX . B ) ) thus s = s ; ::_thesis: ( XX = XX & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st TT is MSSubAlgebra of B holds XX . TT = XX . B ) ) thus XX = XX ; ::_thesis: for B being strict non-empty finitely-generated MSSubAlgebra of AG st TT is MSSubAlgebra of B holds XX . TT = XX . B let B be strict non-empty finitely-generated MSSubAlgebra of AG; ::_thesis: ( TT is MSSubAlgebra of B implies XX . TT = XX . B ) assume TT is MSSubAlgebra of B ; ::_thesis: XX . TT = XX . B then the Sorts of TT is ManySortedSubset of the Sorts of B by MSUALG_2:def_9; then the Sorts of TT c= the Sorts of B by PBOOLE:def_18; then A144: the Sorts of TT . s c= the Sorts of B . s by PBOOLE:def_2; A145: B in CC by A2; TT in CC by A2; hence XX . TT = y by A139, A142, A117 .= XX . B by A143, A117, A145, A144 ; ::_thesis: verum end; then A146: XX in SOR . s by A4; then S2[h . XX,XX,s] by A40, A141; then consider t being SortSymbol of SG, f being Element of (SORTS FF) . s, A being strict non-empty finitely-generated MSSubAlgebra of AG such that s = t and A147: ( f = XX & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds f . A = f . B ) & h . XX = f . A ) ; consider MAX being strict non-empty finitely-generated MSSubAlgebra of AG such that A148: A is MSSubAlgebra of MAX and A149: GenMSAlg Y is MSSubAlgebra of MAX by Th26; A150: MAX in CC by A2; the Sorts of (GenMSAlg Y) is ManySortedSubset of the Sorts of MAX by A149, MSUALG_2:def_9; then the Sorts of (GenMSAlg Y) c= the Sorts of MAX by PBOOLE:def_18; then A151: the Sorts of (GenMSAlg Y) . s c= the Sorts of MAX . s by PBOOLE:def_2; h . XX = XX . MAX by A147, A148 .= y by A143, A117, A151, A150 ; hence y in proj2 (BA . i) by A40, A128, A140, A146, FUNCT_1:def_3; ::_thesis: verum end; theorem :: EQUATION:28 for S being non empty non void ManySortedSign for U0 being free feasible MSAlgebra over S for A being free GeneratorSet of U0 for Z being MSSubset of U0 st Z c= A & GenMSAlg Z is feasible holds GenMSAlg Z is free proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being free feasible MSAlgebra over S for A being free GeneratorSet of U0 for Z being MSSubset of U0 st Z c= A & GenMSAlg Z is feasible holds GenMSAlg Z is free let U0 be free feasible MSAlgebra over S; ::_thesis: for A being free GeneratorSet of U0 for Z being MSSubset of U0 st Z c= A & GenMSAlg Z is feasible holds GenMSAlg Z is free let A be free GeneratorSet of U0; ::_thesis: for Z being MSSubset of U0 st Z c= A & GenMSAlg Z is feasible holds GenMSAlg Z is free let Z be MSSubset of U0; ::_thesis: ( Z c= A & GenMSAlg Z is feasible implies GenMSAlg Z is free ) assume that A1: Z c= A and A2: GenMSAlg Z is feasible ; ::_thesis: GenMSAlg Z is free reconsider Z1 = Z as MSSubset of (GenMSAlg Z) by MSUALG_2:def_17; the Sorts of (GenMSAlg Z1) = the Sorts of (GenMSAlg Z) by EXTENS_1:18; then reconsider z = Z as GeneratorSet of GenMSAlg Z by MSAFREE:def_4; reconsider z1 = z as ManySortedSubset of A by A1, PBOOLE:def_18; take z ; :: according to MSAFREE:def_6 ::_thesis: z is free z is free proof reconsider D = the Sorts of (GenMSAlg Z) as MSSubset of U0 by MSUALG_2:def_9; let U1 be non-empty MSAlgebra over S; :: according to MSAFREE:def_5 ::_thesis: for b1 being ManySortedFunction of z, the Sorts of U1 ex b2 being ManySortedFunction of the Sorts of (GenMSAlg Z), the Sorts of U1 st ( b2 is_homomorphism GenMSAlg Z,U1 & b2 || z = b1 ) let g be ManySortedFunction of z, the Sorts of U1; ::_thesis: ex b1 being ManySortedFunction of the Sorts of (GenMSAlg Z), the Sorts of U1 st ( b1 is_homomorphism GenMSAlg Z,U1 & b1 || z = g ) consider G being ManySortedFunction of A, the Sorts of U1 such that A3: G || z1 = g by Th6; consider h being ManySortedFunction of U0,U1 such that A4: h is_homomorphism U0,U1 and A5: h || A = G by MSAFREE:def_5; reconsider H = h || D as ManySortedFunction of (GenMSAlg Z),U1 ; take H ; ::_thesis: ( H is_homomorphism GenMSAlg Z,U1 & H || z = g ) thus H is_homomorphism GenMSAlg Z,U1 by A2, A4, Th22; ::_thesis: H || z = g thus g = h || Z by A3, A5, Th5 .= H || z by Th5 ; ::_thesis: verum end; hence z is free ; ::_thesis: verum end; begin definition let S be non empty non void ManySortedSign ; func TermAlg S -> MSAlgebra over S equals :: EQUATION:def 3 FreeMSA ( the carrier of S --> NAT); correctness coherence FreeMSA ( the carrier of S --> NAT) is MSAlgebra over S; ; end; :: deftheorem defines TermAlg EQUATION:def_3_:_ for S being non empty non void ManySortedSign holds TermAlg S = FreeMSA ( the carrier of S --> NAT); registration let S be non empty non void ManySortedSign ; cluster TermAlg S -> strict non-empty free ; coherence ( TermAlg S is strict & TermAlg S is non-empty & TermAlg S is free ) ; end; definition let S be non empty non void ManySortedSign ; func Equations S -> ManySortedSet of the carrier of S equals :: EQUATION:def 4 [| the Sorts of (TermAlg S), the Sorts of (TermAlg S)|]; correctness coherence [| the Sorts of (TermAlg S), the Sorts of (TermAlg S)|] is ManySortedSet of the carrier of S; ; end; :: deftheorem defines Equations EQUATION:def_4_:_ for S being non empty non void ManySortedSign holds Equations S = [| the Sorts of (TermAlg S), the Sorts of (TermAlg S)|]; registration let S be non empty non void ManySortedSign ; cluster Equations S -> V2() ; coherence Equations S is non-empty ; end; definition let S be non empty non void ManySortedSign ; mode EqualSet of S is ManySortedSubset of Equations S; end; notation let S be non empty non void ManySortedSign ; let s be SortSymbol of S; let x, y be Element of the Sorts of (TermAlg S) . s; synonym x '=' y for [S,s]; end; definition let S be non empty non void ManySortedSign ; let s be SortSymbol of S; let x, y be Element of the Sorts of (TermAlg S) . s; :: original: '=' redefine funcx '=' y -> Element of (Equations S) . s; coherence '=' is Element of (Equations S) . s proof [x,y] in [:( the Sorts of (TermAlg S) . s),( the Sorts of (TermAlg S) . s):] by ZFMISC_1:87; hence '=' is Element of (Equations S) . s by PBOOLE:def_16; ::_thesis: verum end; end; theorem Th29: :: EQUATION:29 for S being non empty non void ManySortedSign for s being SortSymbol of S for e being Element of (Equations S) . s holds e `1 in the Sorts of (TermAlg S) . s proof let S be non empty non void ManySortedSign ; ::_thesis: for s being SortSymbol of S for e being Element of (Equations S) . s holds e `1 in the Sorts of (TermAlg S) . s let s be SortSymbol of S; ::_thesis: for e being Element of (Equations S) . s holds e `1 in the Sorts of (TermAlg S) . s let e be Element of (Equations S) . s; ::_thesis: e `1 in the Sorts of (TermAlg S) . s set T = the Sorts of (TermAlg S); e is Element of [:( the Sorts of (TermAlg S) . s),( the Sorts of (TermAlg S) . s):] by PBOOLE:def_16; hence e `1 in the Sorts of (TermAlg S) . s by MCART_1:10; ::_thesis: verum end; theorem Th30: :: EQUATION:30 for S being non empty non void ManySortedSign for s being SortSymbol of S for e being Element of (Equations S) . s holds e `2 in the Sorts of (TermAlg S) . s proof let S be non empty non void ManySortedSign ; ::_thesis: for s being SortSymbol of S for e being Element of (Equations S) . s holds e `2 in the Sorts of (TermAlg S) . s let s be SortSymbol of S; ::_thesis: for e being Element of (Equations S) . s holds e `2 in the Sorts of (TermAlg S) . s let e be Element of (Equations S) . s; ::_thesis: e `2 in the Sorts of (TermAlg S) . s set T = the Sorts of (TermAlg S); e is Element of [:( the Sorts of (TermAlg S) . s),( the Sorts of (TermAlg S) . s):] by PBOOLE:def_16; hence e `2 in the Sorts of (TermAlg S) . s by MCART_1:10; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let A be MSAlgebra over S; let s be SortSymbol of S; let e be Element of (Equations S) . s; predA |= e means :Def5: :: EQUATION:def 5 for h being ManySortedFunction of (TermAlg S),A st h is_homomorphism TermAlg S,A holds (h . s) . (e `1) = (h . s) . (e `2); end; :: deftheorem Def5 defines |= EQUATION:def_5_:_ for S being non empty non void ManySortedSign for A being MSAlgebra over S for s being SortSymbol of S for e being Element of (Equations S) . s holds ( A |= e iff for h being ManySortedFunction of (TermAlg S),A st h is_homomorphism TermAlg S,A holds (h . s) . (e `1) = (h . s) . (e `2) ); definition let S be non empty non void ManySortedSign ; let A be MSAlgebra over S; let E be EqualSet of S; predA |= E means :Def6: :: EQUATION:def 6 for s being SortSymbol of S for e being Element of (Equations S) . s st e in E . s holds A |= e; end; :: deftheorem Def6 defines |= EQUATION:def_6_:_ for S being non empty non void ManySortedSign for A being MSAlgebra over S for E being EqualSet of S holds ( A |= E iff for s being SortSymbol of S for e being Element of (Equations S) . s st e in E . s holds A |= e ); theorem Th31: :: EQUATION:31 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S for s being SortSymbol of S for e being Element of (Equations S) . s for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= e holds U2 |= e proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S for s being SortSymbol of S for e being Element of (Equations S) . s for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= e holds U2 |= e let U0 be non-empty MSAlgebra over S; ::_thesis: for s being SortSymbol of S for e being Element of (Equations S) . s for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= e holds U2 |= e let s be SortSymbol of S; ::_thesis: for e being Element of (Equations S) . s for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= e holds U2 |= e let e be Element of (Equations S) . s; ::_thesis: for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= e holds U2 |= e let U2 be strict non-empty MSSubAlgebra of U0; ::_thesis: ( U0 |= e implies U2 |= e ) assume A1: U0 |= e ; ::_thesis: U2 |= e let h be ManySortedFunction of (TermAlg S),U2; :: according to EQUATION:def_5 ::_thesis: ( h is_homomorphism TermAlg S,U2 implies (h . s) . (e `1) = (h . s) . (e `2) ) assume A2: h is_homomorphism TermAlg S,U2 ; ::_thesis: (h . s) . (e `1) = (h . s) . (e `2) A3: the Sorts of (TermAlg S) is_transformable_to the Sorts of U2 proof let i be set ; :: according to PZFMISC1:def_3 ::_thesis: ( not i in the carrier of S or not the Sorts of U2 . i = {} or the Sorts of (TermAlg S) . i = {} ) assume i in the carrier of S ; ::_thesis: ( not the Sorts of U2 . i = {} or the Sorts of (TermAlg S) . i = {} ) hence ( not the Sorts of U2 . i = {} or the Sorts of (TermAlg S) . i = {} ) ; ::_thesis: verum end; the Sorts of U2 is MSSubset of U0 by MSUALG_2:def_9; then reconsider f1 = h as ManySortedFunction of (TermAlg S),U0 by A3, EXTENS_1:5; f1 is_homomorphism TermAlg S,U0 by A2, MSUALG_9:15; hence (h . s) . (e `1) = (h . s) . (e `2) by A1, Def5; ::_thesis: verum end; theorem :: EQUATION:32 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S for E being EqualSet of S for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= E holds U2 |= E proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S for E being EqualSet of S for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= E holds U2 |= E let U0 be non-empty MSAlgebra over S; ::_thesis: for E being EqualSet of S for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= E holds U2 |= E let E be EqualSet of S; ::_thesis: for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= E holds U2 |= E let U2 be strict non-empty MSSubAlgebra of U0; ::_thesis: ( U0 |= E implies U2 |= E ) assume A1: U0 |= E ; ::_thesis: U2 |= E let s be SortSymbol of S; :: according to EQUATION:def_6 ::_thesis: for e being Element of (Equations S) . s st e in E . s holds U2 |= e let e be Element of (Equations S) . s; ::_thesis: ( e in E . s implies U2 |= e ) assume e in E . s ; ::_thesis: U2 |= e then U0 |= e by A1, Def6; hence U2 |= e by Th31; ::_thesis: verum end; theorem Th33: :: EQUATION:33 for S being non empty non void ManySortedSign for U0, U1 being non-empty MSAlgebra over S for s being SortSymbol of S for e being Element of (Equations S) . s st U0,U1 are_isomorphic & U0 |= e holds U1 |= e proof let S be non empty non void ManySortedSign ; ::_thesis: for U0, U1 being non-empty MSAlgebra over S for s being SortSymbol of S for e being Element of (Equations S) . s st U0,U1 are_isomorphic & U0 |= e holds U1 |= e let U0, U1 be non-empty MSAlgebra over S; ::_thesis: for s being SortSymbol of S for e being Element of (Equations S) . s st U0,U1 are_isomorphic & U0 |= e holds U1 |= e let s be SortSymbol of S; ::_thesis: for e being Element of (Equations S) . s st U0,U1 are_isomorphic & U0 |= e holds U1 |= e let e be Element of (Equations S) . s; ::_thesis: ( U0,U1 are_isomorphic & U0 |= e implies U1 |= e ) assume that A1: U0,U1 are_isomorphic and A2: U0 |= e ; ::_thesis: U1 |= e consider F being ManySortedFunction of U0,U1 such that A3: F is_isomorphism U0,U1 by A1, MSUALG_3:def_11; consider G being ManySortedFunction of U1,U0 such that A4: G = F "" ; ( F is "1-1" & F is "onto" ) by A3, MSUALG_3:13; then A5: G . s = (F . s) " by A4, MSUALG_3:def_4; F is "onto" by A3, MSUALG_3:13; then A6: rng (F . s) = the Sorts of U1 . s by MSUALG_3:def_3; let h1 be ManySortedFunction of (TermAlg S),U1; :: according to EQUATION:def_5 ::_thesis: ( h1 is_homomorphism TermAlg S,U1 implies (h1 . s) . (e `1) = (h1 . s) . (e `2) ) assume A7: h1 is_homomorphism TermAlg S,U1 ; ::_thesis: (h1 . s) . (e `1) = (h1 . s) . (e `2) set F1 = G ** h1; G is_isomorphism U1,U0 by A3, A4, MSUALG_3:14; then G is_homomorphism U1,U0 by MSUALG_3:13; then A8: G ** h1 is_homomorphism TermAlg S,U0 by A7, MSUALG_3:10; F is "1-1" by A3, MSUALG_3:13; then A9: F . s is one-to-one by MSUALG_3:1; (G ** h1) . s = (G . s) * (h1 . s) by MSUALG_3:2; then A10: (F . s) * ((G ** h1) . s) = ((F . s) * (G . s)) * (h1 . s) by RELAT_1:36 .= (id ( the Sorts of U1 . s)) * (h1 . s) by A5, A6, A9, FUNCT_2:29 .= h1 . s by FUNCT_2:17 ; A11: dom ((G ** h1) . s) = the Sorts of (TermAlg S) . s by FUNCT_2:def_1; hence (h1 . s) . (e `1) = (F . s) . (((G ** h1) . s) . (e `1)) by A10, Th29, FUNCT_1:13 .= (F . s) . (((G ** h1) . s) . (e `2)) by A2, A8, Def5 .= (h1 . s) . (e `2) by A10, A11, Th30, FUNCT_1:13 ; ::_thesis: verum end; theorem :: EQUATION:34 for S being non empty non void ManySortedSign for U0, U1 being non-empty MSAlgebra over S for E being EqualSet of S st U0,U1 are_isomorphic & U0 |= E holds U1 |= E proof let S be non empty non void ManySortedSign ; ::_thesis: for U0, U1 being non-empty MSAlgebra over S for E being EqualSet of S st U0,U1 are_isomorphic & U0 |= E holds U1 |= E let U0, U1 be non-empty MSAlgebra over S; ::_thesis: for E being EqualSet of S st U0,U1 are_isomorphic & U0 |= E holds U1 |= E let E be EqualSet of S; ::_thesis: ( U0,U1 are_isomorphic & U0 |= E implies U1 |= E ) assume that A1: U0,U1 are_isomorphic and A2: U0 |= E ; ::_thesis: U1 |= E let s be SortSymbol of S; :: according to EQUATION:def_6 ::_thesis: for e being Element of (Equations S) . s st e in E . s holds U1 |= e let e be Element of (Equations S) . s; ::_thesis: ( e in E . s implies U1 |= e ) assume e in E . s ; ::_thesis: U1 |= e then U0 |= e by A2, Def6; hence U1 |= e by A1, Th33; ::_thesis: verum end; theorem Th35: :: EQUATION:35 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S for s being SortSymbol of S for e being Element of (Equations S) . s for R being MSCongruence of U0 st U0 |= e holds QuotMSAlg (U0,R) |= e proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S for s being SortSymbol of S for e being Element of (Equations S) . s for R being MSCongruence of U0 st U0 |= e holds QuotMSAlg (U0,R) |= e let U0 be non-empty MSAlgebra over S; ::_thesis: for s being SortSymbol of S for e being Element of (Equations S) . s for R being MSCongruence of U0 st U0 |= e holds QuotMSAlg (U0,R) |= e let s be SortSymbol of S; ::_thesis: for e being Element of (Equations S) . s for R being MSCongruence of U0 st U0 |= e holds QuotMSAlg (U0,R) |= e let e be Element of (Equations S) . s; ::_thesis: for R being MSCongruence of U0 st U0 |= e holds QuotMSAlg (U0,R) |= e let R be MSCongruence of U0; ::_thesis: ( U0 |= e implies QuotMSAlg (U0,R) |= e ) assume A1: U0 |= e ; ::_thesis: QuotMSAlg (U0,R) |= e set n = (MSNat_Hom (U0,R)) . s; let h be ManySortedFunction of (TermAlg S),(QuotMSAlg (U0,R)); :: according to EQUATION:def_5 ::_thesis: ( h is_homomorphism TermAlg S, QuotMSAlg (U0,R) implies (h . s) . (e `1) = (h . s) . (e `2) ) assume h is_homomorphism TermAlg S, QuotMSAlg (U0,R) ; ::_thesis: (h . s) . (e `1) = (h . s) . (e `2) then consider h0 being ManySortedFunction of (TermAlg S),U0 such that A2: h0 is_homomorphism TermAlg S,U0 and A3: h = (MSNat_Hom (U0,R)) ** h0 by Th24, MSUALG_4:3; A4: dom (h0 . s) = the Sorts of (TermAlg S) . s by FUNCT_2:def_1; thus (h . s) . (e `1) = (((MSNat_Hom (U0,R)) . s) * (h0 . s)) . (e `1) by A3, MSUALG_3:2 .= ((MSNat_Hom (U0,R)) . s) . ((h0 . s) . (e `1)) by A4, Th29, FUNCT_1:13 .= ((MSNat_Hom (U0,R)) . s) . ((h0 . s) . (e `2)) by A1, A2, Def5 .= (((MSNat_Hom (U0,R)) . s) * (h0 . s)) . (e `2) by A4, Th30, FUNCT_1:13 .= (h . s) . (e `2) by A3, MSUALG_3:2 ; ::_thesis: verum end; theorem :: EQUATION:36 for S being non empty non void ManySortedSign for U0 being non-empty MSAlgebra over S for E being EqualSet of S for R being MSCongruence of U0 st U0 |= E holds QuotMSAlg (U0,R) |= E proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being non-empty MSAlgebra over S for E being EqualSet of S for R being MSCongruence of U0 st U0 |= E holds QuotMSAlg (U0,R) |= E let U0 be non-empty MSAlgebra over S; ::_thesis: for E being EqualSet of S for R being MSCongruence of U0 st U0 |= E holds QuotMSAlg (U0,R) |= E let E be EqualSet of S; ::_thesis: for R being MSCongruence of U0 st U0 |= E holds QuotMSAlg (U0,R) |= E let R be MSCongruence of U0; ::_thesis: ( U0 |= E implies QuotMSAlg (U0,R) |= E ) assume A1: U0 |= E ; ::_thesis: QuotMSAlg (U0,R) |= E let s be SortSymbol of S; :: according to EQUATION:def_6 ::_thesis: for e being Element of (Equations S) . s st e in E . s holds QuotMSAlg (U0,R) |= e let e be Element of (Equations S) . s; ::_thesis: ( e in E . s implies QuotMSAlg (U0,R) |= e ) assume e in E . s ; ::_thesis: QuotMSAlg (U0,R) |= e then U0 |= e by A1, Def6; hence QuotMSAlg (U0,R) |= e by Th35; ::_thesis: verum end; Lm1: for S being non empty non void ManySortedSign for s being SortSymbol of S for e being Element of (Equations S) . s for I being non empty set for A being MSAlgebra-Family of I,S st ( for i being Element of I holds A . i |= e ) holds product A |= e proof let S be non empty non void ManySortedSign ; ::_thesis: for s being SortSymbol of S for e being Element of (Equations S) . s for I being non empty set for A being MSAlgebra-Family of I,S st ( for i being Element of I holds A . i |= e ) holds product A |= e let s be SortSymbol of S; ::_thesis: for e being Element of (Equations S) . s for I being non empty set for A being MSAlgebra-Family of I,S st ( for i being Element of I holds A . i |= e ) holds product A |= e let e be Element of (Equations S) . s; ::_thesis: for I being non empty set for A being MSAlgebra-Family of I,S st ( for i being Element of I holds A . i |= e ) holds product A |= e reconsider e2 = e `2 as Element of the Sorts of (TermAlg S) . s by Th30; reconsider e1 = e `1 as Element of the Sorts of (TermAlg S) . s by Th29; let I be non empty set ; ::_thesis: for A being MSAlgebra-Family of I,S st ( for i being Element of I holds A . i |= e ) holds product A |= e let A be MSAlgebra-Family of I,S; ::_thesis: ( ( for i being Element of I holds A . i |= e ) implies product A |= e ) assume A1: for i being Element of I holds A . i |= e ; ::_thesis: product A |= e let h be ManySortedFunction of (TermAlg S),(product A); :: according to EQUATION:def_5 ::_thesis: ( h is_homomorphism TermAlg S, product A implies (h . s) . (e `1) = (h . s) . (e `2) ) assume A2: h is_homomorphism TermAlg S, product A ; ::_thesis: (h . s) . (e `1) = (h . s) . (e `2) A3: dom (h . s) = the Sorts of (TermAlg S) . s by FUNCT_2:def_1; A4: now__::_thesis:_for_i_being_Element_of_I_holds_(proj_((Carrier_(A,s)),i))_._((h_._s)_._e1)_=_(proj_((Carrier_(A,s)),i))_._((h_._s)_._e2) let i be Element of I; ::_thesis: (proj ((Carrier (A,s)),i)) . ((h . s) . e1) = (proj ((Carrier (A,s)),i)) . ((h . s) . e2) set Z = (proj (A,i)) ** h; A5: A . i |= e by A1; proj (A,i) is_homomorphism product A,A . i by PRALG_3:24; then A6: (proj (A,i)) ** h is_homomorphism TermAlg S,A . i by A2, MSUALG_3:10; thus (proj ((Carrier (A,s)),i)) . ((h . s) . e1) = ((proj (A,i)) . s) . ((h . s) . e1) by PRALG_3:def_2 .= (((proj (A,i)) . s) * (h . s)) . e1 by A3, FUNCT_1:13 .= (((proj (A,i)) ** h) . s) . e1 by MSUALG_3:2 .= (((proj (A,i)) ** h) . s) . e2 by A5, A6, Def5 .= (((proj (A,i)) . s) * (h . s)) . e2 by MSUALG_3:2 .= ((proj (A,i)) . s) . ((h . s) . e2) by A3, FUNCT_1:13 .= (proj ((Carrier (A,s)),i)) . ((h . s) . e2) by PRALG_3:def_2 ; ::_thesis: verum end; the Sorts of (product A) . s = product (Carrier (A,s)) by PRALG_2:def_10; hence (h . s) . (e `1) = (h . s) . (e `2) by A4, MSUALG_9:14; ::_thesis: verum end; theorem Th37: :: EQUATION:37 for I being set for S being non empty non void ManySortedSign for s being SortSymbol of S for e being Element of (Equations S) . s for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds ex A being MSAlgebra over S st ( A = F . i & A |= e ) ) holds product F |= e proof let I be set ; ::_thesis: for S being non empty non void ManySortedSign for s being SortSymbol of S for e being Element of (Equations S) . s for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds ex A being MSAlgebra over S st ( A = F . i & A |= e ) ) holds product F |= e let S be non empty non void ManySortedSign ; ::_thesis: for s being SortSymbol of S for e being Element of (Equations S) . s for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds ex A being MSAlgebra over S st ( A = F . i & A |= e ) ) holds product F |= e let s be SortSymbol of S; ::_thesis: for e being Element of (Equations S) . s for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds ex A being MSAlgebra over S st ( A = F . i & A |= e ) ) holds product F |= e let e be Element of (Equations S) . s; ::_thesis: for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds ex A being MSAlgebra over S st ( A = F . i & A |= e ) ) holds product F |= e let F be MSAlgebra-Family of I,S; ::_thesis: ( ( for i being set st i in I holds ex A being MSAlgebra over S st ( A = F . i & A |= e ) ) implies product F |= e ) assume A1: for i being set st i in I holds ex A being MSAlgebra over S st ( A = F . i & A |= e ) ; ::_thesis: product F |= e percases ( I = {} or I <> {} ) ; suppose I = {} ; ::_thesis: product F |= e then reconsider J = I as empty set ; reconsider FJ = F as MSAlgebra-Family of J,S ; thus product F |= e ::_thesis: verum proof let h be ManySortedFunction of (TermAlg S),(product F); :: according to EQUATION:def_5 ::_thesis: ( h is_homomorphism TermAlg S, product F implies (h . s) . (e `1) = (h . s) . (e `2) ) assume h is_homomorphism TermAlg S, product F ; ::_thesis: (h . s) . (e `1) = (h . s) . (e `2) A2: the Sorts of (product FJ) . s = product (Carrier (FJ,s)) by PRALG_2:def_10 .= {{}} by CARD_3:10 ; A3: (h . s) . (e `2) in the Sorts of (product FJ) . s by Th30, FUNCT_2:5; (h . s) . (e `1) in the Sorts of (product FJ) . s by Th29, FUNCT_2:5; hence (h . s) . (e `1) = {} by A2, TARSKI:def_1 .= (h . s) . (e `2) by A2, A3, TARSKI:def_1 ; ::_thesis: verum end; end; suppose I <> {} ; ::_thesis: product F |= e then reconsider J = I as non empty set ; reconsider F1 = F as MSAlgebra-Family of J,S ; now__::_thesis:_for_i_being_Element_of_J_holds_F1_._i_|=_e let i be Element of J; ::_thesis: F1 . i |= e ex A being MSAlgebra over S st ( A = F1 . i & A |= e ) by A1; hence F1 . i |= e ; ::_thesis: verum end; hence product F |= e by Lm1; ::_thesis: verum end; end; end; theorem :: EQUATION:38 for I being set for S being non empty non void ManySortedSign for E being EqualSet of S for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds ex A being MSAlgebra over S st ( A = F . i & A |= E ) ) holds product F |= E proof let I be set ; ::_thesis: for S being non empty non void ManySortedSign for E being EqualSet of S for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds ex A being MSAlgebra over S st ( A = F . i & A |= E ) ) holds product F |= E let S be non empty non void ManySortedSign ; ::_thesis: for E being EqualSet of S for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds ex A being MSAlgebra over S st ( A = F . i & A |= E ) ) holds product F |= E let E be EqualSet of S; ::_thesis: for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds ex A being MSAlgebra over S st ( A = F . i & A |= E ) ) holds product F |= E let F be MSAlgebra-Family of I,S; ::_thesis: ( ( for i being set st i in I holds ex A being MSAlgebra over S st ( A = F . i & A |= E ) ) implies product F |= E ) assume A1: for i being set st i in I holds ex A being MSAlgebra over S st ( A = F . i & A |= E ) ; ::_thesis: product F |= E let s be SortSymbol of S; :: according to EQUATION:def_6 ::_thesis: for e being Element of (Equations S) . s st e in E . s holds product F |= e let e be Element of (Equations S) . s; ::_thesis: ( e in E . s implies product F |= e ) assume A2: e in E . s ; ::_thesis: product F |= e now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ex_A_being_MSAlgebra_over_S_st_ (_A_=_F_._i_&_A_|=_e_) let i be set ; ::_thesis: ( i in I implies ex A being MSAlgebra over S st ( A = F . i & A |= e ) ) assume i in I ; ::_thesis: ex A being MSAlgebra over S st ( A = F . i & A |= e ) then consider A being MSAlgebra over S such that A3: ( A = F . i & A |= E ) by A1; take A = A; ::_thesis: ( A = F . i & A |= e ) thus ( A = F . i & A |= e ) by A2, A3, Def6; ::_thesis: verum end; hence product F |= e by Th37; ::_thesis: verum end;