:: PRALG_3 semantic presentation begin registration let I be set ; let S be non empty non void ManySortedSign ; let AF be MSAlgebra-Family of I,S; cluster product AF -> non-empty ; coherence product AF is non-empty by MSUALG_1:def_3; end; registration let X be with_non-empty_elements set ; cluster id X -> non-empty ; coherence id X is non-empty proof reconsider NE = id X as ManySortedSet of X ; NE is V8() proof let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in X or not NE . i is empty ) assume i in X ; ::_thesis: not NE . i is empty hence not NE . i is empty by FUNCT_1:17; ::_thesis: verum end; hence id X is non-empty ; ::_thesis: verum end; end; theorem Th1: :: PRALG_3:1 for f, F being Function for A being set st f in product F holds f | A in product (F | A) proof let f, F be Function; ::_thesis: for A being set st f in product F holds f | A in product (F | A) let A be set ; ::_thesis: ( f in product F implies f | A in product (F | A) ) assume A1: f in product F ; ::_thesis: f | A in product (F | A) then dom f = dom F by CARD_3:9; then A2: dom (f | A) = (dom F) /\ A by RELAT_1:61 .= dom (F | A) by RELAT_1:61 ; for x being set st x in dom (F | A) holds (f | A) . x in (F | A) . x proof let x be set ; ::_thesis: ( x in dom (F | A) implies (f | A) . x in (F | A) . x ) assume A3: x in dom (F | A) ; ::_thesis: (f | A) . x in (F | A) . x then x in (dom F) /\ A by RELAT_1:61; then A4: x in dom F by XBOOLE_0:def_4; ( (F | A) . x = F . x & (f | A) . x = f . x ) by A2, A3, FUNCT_1:47; hence (f | A) . x in (F | A) . x by A1, A4, CARD_3:9; ::_thesis: verum end; hence f | A in product (F | A) by A2, CARD_3:9; ::_thesis: verum end; theorem Th2: :: PRALG_3:2 for I being non empty set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for s being SortSymbol of S for a being non empty Subset of I for Aa being MSAlgebra-Family of a,S st A | a = Aa holds Carrier (Aa,s) = (Carrier (A,s)) | a proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for s being SortSymbol of S for a being non empty Subset of I for Aa being MSAlgebra-Family of a,S st A | a = Aa holds Carrier (Aa,s) = (Carrier (A,s)) | a let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for s being SortSymbol of S for a being non empty Subset of I for Aa being MSAlgebra-Family of a,S st A | a = Aa holds Carrier (Aa,s) = (Carrier (A,s)) | a let A be MSAlgebra-Family of I,S; ::_thesis: for s being SortSymbol of S for a being non empty Subset of I for Aa being MSAlgebra-Family of a,S st A | a = Aa holds Carrier (Aa,s) = (Carrier (A,s)) | a let s be SortSymbol of S; ::_thesis: for a being non empty Subset of I for Aa being MSAlgebra-Family of a,S st A | a = Aa holds Carrier (Aa,s) = (Carrier (A,s)) | a let a be non empty Subset of I; ::_thesis: for Aa being MSAlgebra-Family of a,S st A | a = Aa holds Carrier (Aa,s) = (Carrier (A,s)) | a let Aa be MSAlgebra-Family of a,S; ::_thesis: ( A | a = Aa implies Carrier (Aa,s) = (Carrier (A,s)) | a ) assume A1: A | a = Aa ; ::_thesis: Carrier (Aa,s) = (Carrier (A,s)) | a dom ((Carrier (A,s)) | a) = (dom (Carrier (A,s))) /\ a by RELAT_1:61 .= I /\ a by PARTFUN1:def_2 .= a by XBOOLE_1:28 ; then reconsider Cas = (Carrier (A,s)) | a as ManySortedSet of a by PARTFUN1:def_2; for i being set st i in a holds (Carrier (Aa,s)) . i = Cas . i proof let i be set ; ::_thesis: ( i in a implies (Carrier (Aa,s)) . i = Cas . i ) assume A2: i in a ; ::_thesis: (Carrier (Aa,s)) . i = Cas . i then reconsider i9 = i as Element of a ; reconsider i99 = i9 as Element of I ; A3: ( Aa . i9 = A . i9 & ex U1 being MSAlgebra over S st ( U1 = A . i99 & (Carrier (A,s)) . i99 = the Sorts of U1 . s ) ) by A1, FUNCT_1:49, PRALG_2:def_9; ex U0 being MSAlgebra over S st ( U0 = Aa . i & (Carrier (Aa,s)) . i = the Sorts of U0 . s ) by A2, PRALG_2:def_9; hence (Carrier (Aa,s)) . i = Cas . i by A3, FUNCT_1:49; ::_thesis: verum end; hence Carrier (Aa,s) = (Carrier (A,s)) | a by PBOOLE:3; ::_thesis: verum end; theorem Th3: :: PRALG_3:3 for i being set for I being non empty set for EqR being Equivalence_Relation of I for c1, c2 being Element of Class EqR st i in c1 & i in c2 holds c1 = c2 proof let i be set ; ::_thesis: for I being non empty set for EqR being Equivalence_Relation of I for c1, c2 being Element of Class EqR st i in c1 & i in c2 holds c1 = c2 let I be non empty set ; ::_thesis: for EqR being Equivalence_Relation of I for c1, c2 being Element of Class EqR st i in c1 & i in c2 holds c1 = c2 let EqR be Equivalence_Relation of I; ::_thesis: for c1, c2 being Element of Class EqR st i in c1 & i in c2 holds c1 = c2 let c1, c2 be Element of Class EqR; ::_thesis: ( i in c1 & i in c2 implies c1 = c2 ) assume that A1: i in c1 and A2: i in c2 ; ::_thesis: c1 = c2 consider x1 being set such that x1 in I and A3: c1 = Class (EqR,x1) by EQREL_1:def_3; A4: [i,x1] in EqR by A1, A3, EQREL_1:19; consider x2 being set such that x2 in I and A5: c2 = Class (EqR,x2) by EQREL_1:def_3; [i,x2] in EqR by A2, A5, EQREL_1:19; then Class (EqR,x2) = Class (EqR,i) by A1, EQREL_1:35 .= c1 by A1, A3, A4, EQREL_1:35 ; hence c1 = c2 by A5; ::_thesis: verum end; Lm1: for f being Function for x being set st x in product f holds x is Function ; theorem :: PRALG_3:4 for D being non empty set for F being ManySortedFunction of D for C being non empty functional with_common_domain set st C = rng F holds for d being Element of D for e being set st e in DOM C holds (F . d) . e = ((commute F) . e) . d proof let D be non empty set ; ::_thesis: for F being ManySortedFunction of D for C being non empty functional with_common_domain set st C = rng F holds for d being Element of D for e being set st e in DOM C holds (F . d) . e = ((commute F) . e) . d let F be ManySortedFunction of D; ::_thesis: for C being non empty functional with_common_domain set st C = rng F holds for d being Element of D for e being set st e in DOM C holds (F . d) . e = ((commute F) . e) . d set E = union { (rng (F . d9)) where d9 is Element of D : verum } ; reconsider F9 = F as Function ; let C be non empty functional with_common_domain set ; ::_thesis: ( C = rng F implies for d being Element of D for e being set st e in DOM C holds (F . d) . e = ((commute F) . e) . d ) assume A1: C = rng F ; ::_thesis: for d being Element of D for e being set st e in DOM C holds (F . d) . e = ((commute F) . e) . d A2: rng F9 c= Funcs ((DOM C),(union { (rng (F . d9)) where d9 is Element of D : verum } )) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F9 or x in Funcs ((DOM C),(union { (rng (F . d9)) where d9 is Element of D : verum } )) ) assume x in rng F9 ; ::_thesis: x in Funcs ((DOM C),(union { (rng (F . d9)) where d9 is Element of D : verum } )) then consider d9 being set such that A3: d9 in dom F and A4: F . d9 = x by FUNCT_1:def_3; reconsider d9 = d9 as Element of D by A3; consider Fd being Function such that A5: Fd = F . d9 ; A6: rng Fd c= union { (rng (F . d9)) where d9 is Element of D : verum } proof A7: rng Fd in { (rng (F . d99)) where d99 is Element of D : verum } by A5; let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in rng Fd or x1 in union { (rng (F . d9)) where d9 is Element of D : verum } ) assume x1 in rng Fd ; ::_thesis: x1 in union { (rng (F . d9)) where d9 is Element of D : verum } hence x1 in union { (rng (F . d9)) where d9 is Element of D : verum } by A7, TARSKI:def_4; ::_thesis: verum end; F . d9 in rng F by A3, FUNCT_1:def_3; then dom Fd = DOM C by A1, A5, CARD_3:108; hence x in Funcs ((DOM C),(union { (rng (F . d9)) where d9 is Element of D : verum } )) by A4, A5, A6, FUNCT_2:def_2; ::_thesis: verum end; let d be Element of D; ::_thesis: for e being set st e in DOM C holds (F . d) . e = ((commute F) . e) . d let e be set ; ::_thesis: ( e in DOM C implies (F . d) . e = ((commute F) . e) . d ) assume A8: e in DOM C ; ::_thesis: (F . d) . e = ((commute F) . e) . d dom F9 = D by PARTFUN1:def_2; then F in Funcs (D,(Funcs ((DOM C),(union { (rng (F . d9)) where d9 is Element of D : verum } )))) by A2, FUNCT_2:def_2; hence (F . d) . e = ((commute F) . e) . d by A8, FUNCT_6:56; ::_thesis: verum end; begin definition let S be non empty non void ManySortedSign ; let U0 be MSAlgebra over S; let o be OperSymbol of S; func const (o,U0) -> set equals :: PRALG_3:def 1 (Den (o,U0)) . {}; correctness coherence (Den (o,U0)) . {} is set ; ; end; :: deftheorem defines const PRALG_3:def_1_:_ for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for o being OperSymbol of S holds const (o,U0) = (Den (o,U0)) . {}; theorem Th5: :: PRALG_3:5 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for o being OperSymbol of S st the_arity_of o = {} & Result (o,U0) <> {} holds const (o,U0) in Result (o,U0) proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for o being OperSymbol of S st the_arity_of o = {} & Result (o,U0) <> {} holds const (o,U0) in Result (o,U0) let U0 be MSAlgebra over S; ::_thesis: for o being OperSymbol of S st the_arity_of o = {} & Result (o,U0) <> {} holds const (o,U0) in Result (o,U0) let o be OperSymbol of S; ::_thesis: ( the_arity_of o = {} & Result (o,U0) <> {} implies const (o,U0) in Result (o,U0) ) assume that A1: the_arity_of o = {} and A2: Result (o,U0) <> {} ; ::_thesis: const (o,U0) in Result (o,U0) dom (Den (o,U0)) = Args (o,U0) by A2, FUNCT_2:def_1 .= {{}} by A1, PRALG_2:4 ; then {} in dom (Den (o,U0)) by TARSKI:def_1; then (Den (o,U0)) . {} in rng (Den (o,U0)) by FUNCT_1:def_3; hence const (o,U0) in Result (o,U0) ; ::_thesis: verum end; theorem :: PRALG_3:6 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for s being SortSymbol of S st the Sorts of U0 . s <> {} holds Constants (U0,s) = { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for s being SortSymbol of S st the Sorts of U0 . s <> {} holds Constants (U0,s) = { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } let U0 be MSAlgebra over S; ::_thesis: for s being SortSymbol of S st the Sorts of U0 . s <> {} holds Constants (U0,s) = { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } let s be SortSymbol of S; ::_thesis: ( the Sorts of U0 . s <> {} implies Constants (U0,s) = { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } ) assume A1: the Sorts of U0 . s <> {} ; ::_thesis: Constants (U0,s) = { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } thus Constants (U0,s) c= { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } :: according to XBOOLE_0:def_10 ::_thesis: { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } c= Constants (U0,s) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Constants (U0,s) or x in { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } ) assume A2: x in Constants (U0,s) ; ::_thesis: x in { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } ex A being non empty set st ( A = the Sorts of U0 . s & Constants (U0,s) = { a where a is Element of A : ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) by A1, MSUALG_2:def_3; then consider A being non empty set such that A = the Sorts of U0 . s and A3: x in { a where a is Element of A : ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } by A2; consider a being Element of A such that A4: a = x and A5: ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) by A3; consider o1 being OperSymbol of S such that A6: the Arity of S . o1 = {} and A7: the ResultSort of S . o1 = s and A8: a in rng (Den (o1,U0)) by A5; A9: ex x1 being set st ( x1 in dom (Den (o1,U0)) & a = (Den (o1,U0)) . x1 ) by A8, FUNCT_1:def_3; A10: the_result_sort_of o1 = s by A7, MSUALG_1:def_2; A11: the_arity_of o1 = {} by A6, MSUALG_1:def_1; then Args (o1,U0) = {{}} by PRALG_2:4; then x = const (o1,U0) by A4, A9, TARSKI:def_1; hence x in { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } by A10, A11; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } or x in Constants (U0,s) ) assume x in { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) } ; ::_thesis: x in Constants (U0,s) then consider o being Element of the carrier' of S such that A12: x = const (o,U0) and A13: the_result_sort_of o = s and A14: the_arity_of o = {} ; o in the carrier' of S ; then A15: o in dom the ResultSort of S by FUNCT_2:def_1; A16: Result (o,U0) = ( the Sorts of U0 * the ResultSort of S) . o by MSUALG_1:def_5 .= the Sorts of U0 . ( the ResultSort of S . o) by A15, FUNCT_1:13 .= the Sorts of U0 . s by A13, MSUALG_1:def_2 ; thus x in Constants (U0,s) ::_thesis: verum proof A17: ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & x in rng (Den (o,U0)) ) proof take o ; ::_thesis: ( the Arity of S . o = {} & the ResultSort of S . o = s & x in rng (Den (o,U0)) ) ( Args (o,U0) = dom (Den (o,U0)) & Args (o,U0) = {{}} ) by A1, A14, A16, FUNCT_2:def_1, PRALG_2:4; then {} in dom (Den (o,U0)) by TARSKI:def_1; hence ( the Arity of S . o = {} & the ResultSort of S . o = s & x in rng (Den (o,U0)) ) by A12, A13, A14, FUNCT_1:def_3, MSUALG_1:def_1, MSUALG_1:def_2; ::_thesis: verum end; consider A being non empty set such that A18: A = the Sorts of U0 . s and A19: Constants (U0,s) = { a where a is Element of A : ex o being OperSymbol of S st ( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } by A1, MSUALG_2:def_3; x is Element of A by A12, A14, A16, A18, Th5; hence x in Constants (U0,s) by A19, A17; ::_thesis: verum end; end; theorem Th7: :: PRALG_3:7 for I being non empty set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S st the_arity_of o = {} holds (commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )))) proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S st the_arity_of o = {} holds (commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )))) let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for o being OperSymbol of S st the_arity_of o = {} holds (commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )))) let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S st the_arity_of o = {} holds (commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )))) let o be OperSymbol of S; ::_thesis: ( the_arity_of o = {} implies (commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )))) ) set f = (commute (OPER A)) . o; set C = union { (Result (o,(A . i9))) where i9 is Element of I : verum } ; commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A)))))) by PRALG_2:6; then A1: ex f1 being Function st ( commute (OPER A) = f1 & dom f1 = the carrier' of S & rng f1 c= Funcs (I,(rng (uncurry (OPER A)))) ) by FUNCT_2:def_2; then (commute (OPER A)) . o in rng (commute (OPER A)) by FUNCT_1:def_3; then A2: ex fb being Function st ( fb = (commute (OPER A)) . o & dom fb = I & rng fb c= rng (uncurry (OPER A)) ) by A1, FUNCT_2:def_2; assume A3: the_arity_of o = {} ; ::_thesis: (commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )))) now__::_thesis:_for_x_being_set_st_x_in_rng_((commute_(OPER_A))_._o)_holds_ x_in_Funcs_({{}},(union__{__(Result_(o,(A_._i9)))_where_i9_is_Element_of_I_:_verum__}__)) let x be set ; ::_thesis: ( x in rng ((commute (OPER A)) . o) implies x in Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) ) assume x in rng ((commute (OPER A)) . o) ; ::_thesis: x in Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) then consider a being set such that A4: a in dom ((commute (OPER A)) . o) and A5: ((commute (OPER A)) . o) . a = x by FUNCT_1:def_3; (commute (OPER A)) . o = A ?. o ; then reconsider x9 = x as Function by A5; reconsider a = a as Element of I by A2, A4; A6: x9 = (A ?. o) . a by A5 .= Den (o,(A . a)) by PRALG_2:7 ; then A7: dom x9 = Args (o,(A . a)) by FUNCT_2:def_1 .= {{}} by A3, PRALG_2:4 ; now__::_thesis:_for_c_being_set_st_c_in_rng_x9_holds_ c_in_union__{__(Result_(o,(A_._i9)))_where_i9_is_Element_of_I_:_verum__}_ let c be set ; ::_thesis: ( c in rng x9 implies c in union { (Result (o,(A . i9))) where i9 is Element of I : verum } ) assume c in rng x9 ; ::_thesis: c in union { (Result (o,(A . i9))) where i9 is Element of I : verum } then consider b being set such that A8: b in dom x9 and A9: x9 . b = c by FUNCT_1:def_3; x9 . b = const (o,(A . a)) by A6, A7, A8, TARSKI:def_1; then A10: c is Element of Result (o,(A . a)) by A3, A9, Th5; Result (o,(A . a)) in { (Result (o,(A . i9))) where i9 is Element of I : verum } ; hence c in union { (Result (o,(A . i9))) where i9 is Element of I : verum } by A10, TARSKI:def_4; ::_thesis: verum end; then rng x9 c= union { (Result (o,(A . i9))) where i9 is Element of I : verum } by TARSKI:def_3; hence x in Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) by A7, FUNCT_2:def_2; ::_thesis: verum end; then rng ((commute (OPER A)) . o) c= Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) by TARSKI:def_3; hence (commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )))) by A2, FUNCT_2:def_2; ::_thesis: verum end; theorem Th8: :: PRALG_3:8 for I being non empty set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S st the_arity_of o = {} holds const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S st the_arity_of o = {} holds const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for o being OperSymbol of S st the_arity_of o = {} holds const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S st the_arity_of o = {} holds const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) let o be OperSymbol of S; ::_thesis: ( the_arity_of o = {} implies const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) ) set g = (commute (OPER A)) . o; set C = union { (Result (o,(A . i9))) where i9 is Element of I : verum } ; assume A1: the_arity_of o = {} ; ::_thesis: const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) then A2: (commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )))) by Th7; reconsider g = (commute (OPER A)) . o as Function ; (OPS A) . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by PRALG_2:def_13 .= commute (A ?. o) by A1, FUNCOP_1:def_8 ; then A3: const (o,(product A)) = (commute g) . {} by MSUALG_1:def_6; commute g in Funcs ({{}},(Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )))) by A2, FUNCT_6:55; then consider g1 being Function such that A4: g1 = commute g and A5: dom g1 = {{}} and A6: rng g1 c= Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) by FUNCT_2:def_2; {} in {{}} by TARSKI:def_1; then g1 . {} in rng g1 by A5, FUNCT_1:def_3; hence const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) by A3, A4, A6; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let I be non empty set ; let o be OperSymbol of S; let A be MSAlgebra-Family of I,S; cluster const (o,(product A)) -> Relation-like Function-like ; coherence ( const (o,(product A)) is Relation-like & const (o,(product A)) is Function-like ) proof const (o,(product A)) is Function proof percases ( the_arity_of o = {} or the_arity_of o <> {} ) ; suppose the_arity_of o = {} ; ::_thesis: const (o,(product A)) is Function then const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) by Th8; then ex g being Function st ( g = const (o,(product A)) & dom g = I & rng g c= union { (Result (o,(A . i9))) where i9 is Element of I : verum } ) by FUNCT_2:def_2; hence const (o,(product A)) is Function ; ::_thesis: verum end; supposeA1: the_arity_of o <> {} ; ::_thesis: const (o,(product A)) is Function dom ( the Sorts of (product A) * (the_arity_of o)) = dom (the_arity_of o) by PRALG_2:3; then A2: dom ( the Sorts of (product A) * (the_arity_of o)) <> dom {} by A1; dom (Den (o,(product A))) = Args (o,(product A)) by FUNCT_2:def_1 .= product ( the Sorts of (product A) * (the_arity_of o)) by PRALG_2:3 ; then not {} in dom (Den (o,(product A))) by A2, CARD_3:9; hence const (o,(product A)) is Function by FUNCT_1:def_2; ::_thesis: verum end; end; end; hence ( const (o,(product A)) is Relation-like & const (o,(product A)) is Function-like ) ; ::_thesis: verum end; end; theorem Th9: :: PRALG_3:9 for I being non empty set for S being non empty non void ManySortedSign for i being Element of I for A being MSAlgebra-Family of I,S for o being OperSymbol of S st the_arity_of o = {} holds (const (o,(product A))) . i = const (o,(A . i)) proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for i being Element of I for A being MSAlgebra-Family of I,S for o being OperSymbol of S st the_arity_of o = {} holds (const (o,(product A))) . i = const (o,(A . i)) let S be non empty non void ManySortedSign ; ::_thesis: for i being Element of I for A being MSAlgebra-Family of I,S for o being OperSymbol of S st the_arity_of o = {} holds (const (o,(product A))) . i = const (o,(A . i)) let i be Element of I; ::_thesis: for A being MSAlgebra-Family of I,S for o being OperSymbol of S st the_arity_of o = {} holds (const (o,(product A))) . i = const (o,(A . i)) let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S st the_arity_of o = {} holds (const (o,(product A))) . i = const (o,(A . i)) let o be OperSymbol of S; ::_thesis: ( the_arity_of o = {} implies (const (o,(product A))) . i = const (o,(A . i)) ) assume A1: the_arity_of o = {} ; ::_thesis: (const (o,(product A))) . i = const (o,(A . i)) set f = (commute (OPER A)) . o; set C = union { (Result (o,(A . i9))) where i9 is Element of I : verum } ; A2: (commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )))) by A1, Th7; (OPS A) . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by PRALG_2:def_13 .= commute (A ?. o) by A1, FUNCOP_1:def_8 ; then A3: const (o,(product A)) = (commute ((commute (OPER A)) . o)) . {} by MSUALG_1:def_6; A4: {} in {{}} by TARSKI:def_1; const (o,(A . i)) = ((A ?. o) . i) . {} by PRALG_2:7 .= (const (o,(product A))) . i by A2, A3, A4, FUNCT_6:56 ; hence (const (o,(product A))) . i = const (o,(A . i)) ; ::_thesis: verum end; theorem :: PRALG_3:10 for I being non empty set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S for f being Function st the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const (o,(A . i)) ) holds f = const (o,(product A)) proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S for f being Function st the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const (o,(A . i)) ) holds f = const (o,(product A)) let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for o being OperSymbol of S for f being Function st the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const (o,(A . i)) ) holds f = const (o,(product A)) let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S for f being Function st the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const (o,(A . i)) ) holds f = const (o,(product A)) let o be OperSymbol of S; ::_thesis: for f being Function st the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const (o,(A . i)) ) holds f = const (o,(product A)) let f be Function; ::_thesis: ( the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const (o,(A . i)) ) implies f = const (o,(product A)) ) assume that A1: the_arity_of o = {} and A2: dom f = I and A3: for i being Element of I holds f . i = const (o,(A . i)) ; ::_thesis: f = const (o,(product A)) A4: now__::_thesis:_for_a_being_set_st_a_in_I_holds_ f_._a_=_(const_(o,(product_A)))_._a let a be set ; ::_thesis: ( a in I implies f . a = (const (o,(product A))) . a ) assume a in I ; ::_thesis: f . a = (const (o,(product A))) . a then reconsider a9 = a as Element of I ; thus f . a = const (o,(A . a9)) by A3 .= (const (o,(product A))) . a by A1, Th9 ; ::_thesis: verum end; set C = union { (Result (o,(A . i9))) where i9 is Element of I : verum } ; const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } )) by A1, Th8; then ex g2 being Function st ( g2 = const (o,(product A)) & dom g2 = I & rng g2 c= union { (Result (o,(A . i9))) where i9 is Element of I : verum } ) by FUNCT_2:def_2; hence f = const (o,(product A)) by A2, A4, FUNCT_1:2; ::_thesis: verum end; theorem Th11: :: PRALG_3:11 for S being non empty non void ManySortedSign for U1, U2 being MSAlgebra over S for o being OperSymbol of S for e being Element of Args (o,U1) st e = {} & the_arity_of o = {} & Args (o,U1) <> {} & Args (o,U2) <> {} holds for F being ManySortedFunction of U1,U2 holds F # e = {} proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being MSAlgebra over S for o being OperSymbol of S for e being Element of Args (o,U1) st e = {} & the_arity_of o = {} & Args (o,U1) <> {} & Args (o,U2) <> {} holds for F being ManySortedFunction of U1,U2 holds F # e = {} let U1, U2 be MSAlgebra over S; ::_thesis: for o being OperSymbol of S for e being Element of Args (o,U1) st e = {} & the_arity_of o = {} & Args (o,U1) <> {} & Args (o,U2) <> {} holds for F being ManySortedFunction of U1,U2 holds F # e = {} let o be OperSymbol of S; ::_thesis: for e being Element of Args (o,U1) st e = {} & the_arity_of o = {} & Args (o,U1) <> {} & Args (o,U2) <> {} holds for F being ManySortedFunction of U1,U2 holds F # e = {} let e be Element of Args (o,U1); ::_thesis: ( e = {} & the_arity_of o = {} & Args (o,U1) <> {} & Args (o,U2) <> {} implies for F being ManySortedFunction of U1,U2 holds F # e = {} ) assume that A1: e = {} and A2: the_arity_of o = {} and A3: ( Args (o,U1) <> {} & Args (o,U2) <> {} ) ; ::_thesis: for F being ManySortedFunction of U1,U2 holds F # e = {} reconsider e1 = e as Function by A1; let F be ManySortedFunction of U1,U2; ::_thesis: F # e = {} rng (the_arity_of o) = {} by A2; then rng (the_arity_of o) c= dom F by XBOOLE_1:2; then A4: dom (F * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27 .= {} by A2 ; then rng (F * (the_arity_of o)) = {} by RELAT_1:42; then F * (the_arity_of o) is Function of {},{} by A4, FUNCT_2:1; then A5: e1 in product (doms (F * (the_arity_of o))) by A1, CARD_3:10, FUNCT_6:23, TARSKI:def_1; A6: F # e = (Frege (F * (the_arity_of o))) . e by A3, MSUALG_3:def_5 .= (F * (the_arity_of o)) .. e1 by A5, PRALG_2:def_2 ; then reconsider fn = F # e as Function ; A7: dom fn = {} by A4, A6, PRALG_1:def_17; thus F # e = {} by A7; ::_thesis: verum end; begin theorem Th12: :: PRALG_3:12 for S being non empty non void ManySortedSign for o being OperSymbol of S for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) holds x in product (doms (F * (the_arity_of o))) proof let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) holds x in product (doms (F * (the_arity_of o))) let o be OperSymbol of S; ::_thesis: for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) holds x in product (doms (F * (the_arity_of o))) let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) holds x in product (doms (F * (the_arity_of o))) let F be ManySortedFunction of U1,U2; ::_thesis: for x being Element of Args (o,U1) holds x in product (doms (F * (the_arity_of o))) let x be Element of Args (o,U1); ::_thesis: x in product (doms (F * (the_arity_of o))) x in Args (o,U1) ; then A1: x in product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3; then A2: dom x = dom ( the Sorts of U1 * (the_arity_of o)) by CARD_3:9 .= dom (the_arity_of o) by PRALG_2:3 ; dom F = the carrier of S by PARTFUN1:def_2; then A3: rng (the_arity_of o) c= dom F ; A4: now__::_thesis:_for_n_being_set_st_n_in_dom_(doms_(F_*_(the_arity_of_o)))_holds_ n_in_dom_x let n be set ; ::_thesis: ( n in dom (doms (F * (the_arity_of o))) implies n in dom x ) assume n in dom (doms (F * (the_arity_of o))) ; ::_thesis: n in dom x then n in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) by FUNCT_6:def_2; then n in dom (F * (the_arity_of o)) by FUNCT_6:19; hence n in dom x by A3, A2, RELAT_1:27; ::_thesis: verum end; A5: dom x = dom ( the Sorts of U1 * (the_arity_of o)) by A1, CARD_3:9; A6: now__::_thesis:_for_n_being_set_st_n_in_dom_(doms_(F_*_(the_arity_of_o)))_holds_ x_._n_in_(doms_(F_*_(the_arity_of_o)))_._n let n be set ; ::_thesis: ( n in dom (doms (F * (the_arity_of o))) implies x . n in (doms (F * (the_arity_of o))) . n ) assume A7: n in dom (doms (F * (the_arity_of o))) ; ::_thesis: x . n in (doms (F * (the_arity_of o))) . n then A8: n in dom (the_arity_of o) by A2, A4; then (the_arity_of o) . n in rng (the_arity_of o) by FUNCT_1:def_3; then reconsider s1 = (the_arity_of o) . n as Element of the carrier of S ; A9: n in dom (F * (the_arity_of o)) by A3, A8, RELAT_1:27; then (F * (the_arity_of o)) . n = F . s1 by FUNCT_1:12; then A10: (doms (F * (the_arity_of o))) . n = dom (F . s1) by A9, FUNCT_6:22 .= the Sorts of U1 . s1 by FUNCT_2:def_1 ; n in dom ( the Sorts of U1 * (the_arity_of o)) by A5, A4, A7; then x . n in ( the Sorts of U1 * (the_arity_of o)) . n by A1, CARD_3:9; hence x . n in (doms (F * (the_arity_of o))) . n by A5, A4, A7, A10, FUNCT_1:12; ::_thesis: verum end; now__::_thesis:_for_n_being_set_st_n_in_dom_x_holds_ n_in_dom_(doms_(F_*_(the_arity_of_o))) let n be set ; ::_thesis: ( n in dom x implies n in dom (doms (F * (the_arity_of o))) ) assume n in dom x ; ::_thesis: n in dom (doms (F * (the_arity_of o))) then A11: n in dom (F * (the_arity_of o)) by A3, A2, RELAT_1:27; (F * (the_arity_of o)) . n is Function ; then n in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) by A11, FUNCT_6:19; hence n in dom (doms (F * (the_arity_of o))) by FUNCT_6:def_2; ::_thesis: verum end; then A12: dom x c= dom (doms (F * (the_arity_of o))) by TARSKI:def_3; dom (doms (F * (the_arity_of o))) c= dom x by A4, TARSKI:def_3; then dom x = dom (doms (F * (the_arity_of o))) by A12, XBOOLE_0:def_10; hence x in product (doms (F * (the_arity_of o))) by A6, CARD_3:9; ::_thesis: verum end; theorem Th13: :: PRALG_3:13 for S being non empty non void ManySortedSign for o being OperSymbol of S for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) for n being set st n in dom (the_arity_of o) holds (F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n) proof let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) for n being set st n in dom (the_arity_of o) holds (F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n) let o be OperSymbol of S; ::_thesis: for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) for n being set st n in dom (the_arity_of o) holds (F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n) let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) for n being set st n in dom (the_arity_of o) holds (F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n) let F be ManySortedFunction of U1,U2; ::_thesis: for x being Element of Args (o,U1) for n being set st n in dom (the_arity_of o) holds (F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n) let x be Element of Args (o,U1); ::_thesis: for n being set st n in dom (the_arity_of o) holds (F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n) let n be set ; ::_thesis: ( n in dom (the_arity_of o) implies (F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n) ) assume A1: n in dom (the_arity_of o) ; ::_thesis: (F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n) dom F = the carrier of S by PARTFUN1:def_2; then rng (the_arity_of o) c= dom F ; then A2: n in dom (F * (the_arity_of o)) by A1, RELAT_1:27; A3: x in product (doms (F * (the_arity_of o))) by Th12; thus (F # x) . n = ((Frege (F * (the_arity_of o))) . x) . n by MSUALG_3:def_5 .= ((F * (the_arity_of o)) .. x) . n by A3, PRALG_2:def_2 .= ((F * (the_arity_of o)) . n) . (x . n) by A2, PRALG_1:def_17 .= (F . ((the_arity_of o) . n)) . (x . n) by A2, FUNCT_1:12 .= (F . ((the_arity_of o) /. n)) . (x . n) by A1, PARTFUN1:def_6 ; ::_thesis: verum end; theorem Th14: :: PRALG_3:14 for I being non empty set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S for x being Element of Args (o,(product A)) holds x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )))) proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S for x being Element of Args (o,(product A)) holds x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )))) let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for o being OperSymbol of S for x being Element of Args (o,(product A)) holds x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )))) let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S for x being Element of Args (o,(product A)) holds x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )))) let o be OperSymbol of S; ::_thesis: for x being Element of Args (o,(product A)) holds x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )))) let x be Element of Args (o,(product A)); ::_thesis: x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )))) set C = union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ; consider x1 being Function such that A1: x1 = x ; x in Args (o,(product A)) ; then A2: x in product ( the Sorts of (product A) * (the_arity_of o)) by PRALG_2:3; dom (SORTS A) = the carrier of S by PARTFUN1:def_2; then A3: rng (the_arity_of o) c= dom (SORTS A) ; now__::_thesis:_for_c_being_set_st_c_in_rng_x1_holds_ c_in_Funcs_(I,(union__{__(_the_Sorts_of_(A_._i9)_._s9)_where_i9_is_Element_of_I,_s9_is_Element_of_the_carrier_of_S_:_verum__}__)) let c be set ; ::_thesis: ( c in rng x1 implies c in Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )) ) assume c in rng x1 ; ::_thesis: c in Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )) then consider n being set such that A4: n in dom x1 and A5: x1 . n = c by FUNCT_1:def_3; A6: n in dom ((SORTS A) * (the_arity_of o)) by A2, A1, A4, CARD_3:9; then n in dom (the_arity_of o) by A3, RELAT_1:27; then (the_arity_of o) . n in rng (the_arity_of o) by FUNCT_1:def_3; then reconsider s1 = (the_arity_of o) . n as Element of the carrier of S ; x1 . n in ((SORTS A) * (the_arity_of o)) . n by A2, A1, A6, CARD_3:9; then x1 . n in (SORTS A) . s1 by A6, FUNCT_1:12; then x1 . n in product (Carrier (A,s1)) by PRALG_2:def_10; then consider g being Function such that A7: g = x1 . n and A8: dom g = dom (Carrier (A,s1)) and A9: for i9 being set st i9 in dom (Carrier (A,s1)) holds g . i9 in (Carrier (A,s1)) . i9 by CARD_3:def_5; now__::_thesis:_for_c1_being_set_st_c1_in_rng_g_holds_ c1_in_union__{__(_the_Sorts_of_(A_._i9)_._s9)_where_i9_is_Element_of_I,_s9_is_Element_of_the_carrier_of_S_:_verum__}_ let c1 be set ; ::_thesis: ( c1 in rng g implies c1 in union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ) assume c1 in rng g ; ::_thesis: c1 in union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } then consider i1 being set such that A10: i1 in dom g and A11: g . i1 = c1 by FUNCT_1:def_3; reconsider i1 = i1 as Element of I by A8, A10; ex U0 being MSAlgebra over S st ( U0 = A . i1 & (Carrier (A,s1)) . i1 = the Sorts of U0 . s1 ) by PRALG_2:def_9; then A12: g . i1 in the Sorts of (A . i1) . s1 by A8, A9, A10; the Sorts of (A . i1) . s1 in { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ; hence c1 in union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } by A11, A12, TARSKI:def_4; ::_thesis: verum end; then A13: rng g c= union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } by TARSKI:def_3; dom g = I by A8, PARTFUN1:def_2; hence c in Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )) by A5, A7, A13, FUNCT_2:def_2; ::_thesis: verum end; then A14: rng x1 c= Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )) by TARSKI:def_3; dom x = dom ((SORTS A) * (the_arity_of o)) by A2, CARD_3:9 .= dom (the_arity_of o) by A3, RELAT_1:27 ; hence x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )))) by A1, A14, FUNCT_2:def_2; ::_thesis: verum end; theorem Th15: :: PRALG_3:15 for I being non empty set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S for x being Element of Args (o,(product A)) for n being set st n in dom (the_arity_of o) holds x . n in product (Carrier (A,((the_arity_of o) /. n))) proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S for x being Element of Args (o,(product A)) for n being set st n in dom (the_arity_of o) holds x . n in product (Carrier (A,((the_arity_of o) /. n))) let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for o being OperSymbol of S for x being Element of Args (o,(product A)) for n being set st n in dom (the_arity_of o) holds x . n in product (Carrier (A,((the_arity_of o) /. n))) let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S for x being Element of Args (o,(product A)) for n being set st n in dom (the_arity_of o) holds x . n in product (Carrier (A,((the_arity_of o) /. n))) let o be OperSymbol of S; ::_thesis: for x being Element of Args (o,(product A)) for n being set st n in dom (the_arity_of o) holds x . n in product (Carrier (A,((the_arity_of o) /. n))) let x be Element of Args (o,(product A)); ::_thesis: for n being set st n in dom (the_arity_of o) holds x . n in product (Carrier (A,((the_arity_of o) /. n))) let n be set ; ::_thesis: ( n in dom (the_arity_of o) implies x . n in product (Carrier (A,((the_arity_of o) /. n))) ) assume A1: n in dom (the_arity_of o) ; ::_thesis: x . n in product (Carrier (A,((the_arity_of o) /. n))) dom (SORTS A) = the carrier of S by PARTFUN1:def_2; then rng (the_arity_of o) c= dom (SORTS A) ; then A2: n in dom ((SORTS A) * (the_arity_of o)) by A1, RELAT_1:27; x in Args (o,(product A)) ; then x in product ( the Sorts of (product A) * (the_arity_of o)) by PRALG_2:3; then x . n in ((SORTS A) * (the_arity_of o)) . n by A2, CARD_3:9; then x . n in (SORTS A) . ((the_arity_of o) . n) by A2, FUNCT_1:12; then x . n in (SORTS A) . ((the_arity_of o) /. n) by A1, PARTFUN1:def_6; hence x . n in product (Carrier (A,((the_arity_of o) /. n))) by PRALG_2:def_10; ::_thesis: verum end; theorem Th16: :: PRALG_3:16 for I being non empty set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S for i being Element of I for n being set st n in dom (the_arity_of o) holds for s being SortSymbol of S st s = (the_arity_of o) . n holds for y being Element of Args (o,(product A)) for g being Function st g = y . n holds g . i in the Sorts of (A . i) . s proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S for i being Element of I for n being set st n in dom (the_arity_of o) holds for s being SortSymbol of S st s = (the_arity_of o) . n holds for y being Element of Args (o,(product A)) for g being Function st g = y . n holds g . i in the Sorts of (A . i) . s let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for o being OperSymbol of S for i being Element of I for n being set st n in dom (the_arity_of o) holds for s being SortSymbol of S st s = (the_arity_of o) . n holds for y being Element of Args (o,(product A)) for g being Function st g = y . n holds g . i in the Sorts of (A . i) . s let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S for i being Element of I for n being set st n in dom (the_arity_of o) holds for s being SortSymbol of S st s = (the_arity_of o) . n holds for y being Element of Args (o,(product A)) for g being Function st g = y . n holds g . i in the Sorts of (A . i) . s let o be OperSymbol of S; ::_thesis: for i being Element of I for n being set st n in dom (the_arity_of o) holds for s being SortSymbol of S st s = (the_arity_of o) . n holds for y being Element of Args (o,(product A)) for g being Function st g = y . n holds g . i in the Sorts of (A . i) . s let i be Element of I; ::_thesis: for n being set st n in dom (the_arity_of o) holds for s being SortSymbol of S st s = (the_arity_of o) . n holds for y being Element of Args (o,(product A)) for g being Function st g = y . n holds g . i in the Sorts of (A . i) . s let n be set ; ::_thesis: ( n in dom (the_arity_of o) implies for s being SortSymbol of S st s = (the_arity_of o) . n holds for y being Element of Args (o,(product A)) for g being Function st g = y . n holds g . i in the Sorts of (A . i) . s ) assume n in dom (the_arity_of o) ; ::_thesis: for s being SortSymbol of S st s = (the_arity_of o) . n holds for y being Element of Args (o,(product A)) for g being Function st g = y . n holds g . i in the Sorts of (A . i) . s then A1: n in dom ( the Sorts of (product A) * (the_arity_of o)) by PRALG_2:3; let s be SortSymbol of S; ::_thesis: ( s = (the_arity_of o) . n implies for y being Element of Args (o,(product A)) for g being Function st g = y . n holds g . i in the Sorts of (A . i) . s ) assume A2: s = (the_arity_of o) . n ; ::_thesis: for y being Element of Args (o,(product A)) for g being Function st g = y . n holds g . i in the Sorts of (A . i) . s let y be Element of Args (o,(product A)); ::_thesis: for g being Function st g = y . n holds g . i in the Sorts of (A . i) . s y in Args (o,(product A)) ; then A3: y in product ( the Sorts of (product A) * (the_arity_of o)) by PRALG_2:3; let g be Function; ::_thesis: ( g = y . n implies g . i in the Sorts of (A . i) . s ) assume g = y . n ; ::_thesis: g . i in the Sorts of (A . i) . s then g in ( the Sorts of (product A) * (the_arity_of o)) . n by A1, A3, CARD_3:9; then g in the Sorts of (product A) . s by A2, A1, FUNCT_1:12; then A4: g in product (Carrier (A,s)) by PRALG_2:def_10; i in I ; then A5: i in dom (Carrier (A,s)) by PARTFUN1:def_2; ex U0 being MSAlgebra over S st ( U0 = A . i & (Carrier (A,s)) . i = the Sorts of U0 . s ) by PRALG_2:def_9; hence g . i in the Sorts of (A . i) . s by A5, A4, CARD_3:9; ::_thesis: verum end; theorem Th17: :: PRALG_3:17 for I being non empty set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds commute y in product (doms (A ?. o)) proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds commute y in product (doms (A ?. o)) let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for o being OperSymbol of S for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds commute y in product (doms (A ?. o)) let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds commute y in product (doms (A ?. o)) let o be OperSymbol of S; ::_thesis: for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds commute y in product (doms (A ?. o)) let y be Element of Args (o,(product A)); ::_thesis: ( the_arity_of o <> {} implies commute y in product (doms (A ?. o)) ) set D = union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ; A1: y in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )))) by Th14; assume the_arity_of o <> {} ; ::_thesis: commute y in product (doms (A ?. o)) then commute y in Funcs (I,(Funcs ((dom (the_arity_of o)),(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )))) by A1, FUNCT_6:55; then A2: ex f being Function st ( f = commute y & dom f = I & rng f c= Funcs ((dom (the_arity_of o)),(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )) ) by FUNCT_2:def_2; A3: now__::_thesis:_for_i1_being_set_st_i1_in_dom_(doms_(A_?._o))_holds_ (commute_y)_._i1_in_(doms_(A_?._o))_._i1 let i1 be set ; ::_thesis: ( i1 in dom (doms (A ?. o)) implies (commute y) . i1 in (doms (A ?. o)) . i1 ) assume i1 in dom (doms (A ?. o)) ; ::_thesis: (commute y) . i1 in (doms (A ?. o)) . i1 then reconsider ii = i1 as Element of I by PRALG_2:11; A4: now__::_thesis:_for_n_being_set_st_n_in_dom_(_the_Sorts_of_(A_._ii)_*_(the_arity_of_o))_holds_ ((commute_y)_._ii)_._n_in_(_the_Sorts_of_(A_._ii)_*_(the_arity_of_o))_._n let n be set ; ::_thesis: ( n in dom ( the Sorts of (A . ii) * (the_arity_of o)) implies ((commute y) . ii) . n in ( the Sorts of (A . ii) * (the_arity_of o)) . n ) assume A5: n in dom ( the Sorts of (A . ii) * (the_arity_of o)) ; ::_thesis: ((commute y) . ii) . n in ( the Sorts of (A . ii) * (the_arity_of o)) . n then A6: n in dom (the_arity_of o) by PRALG_2:3; then (the_arity_of o) . n in rng (the_arity_of o) by FUNCT_1:def_3; then reconsider s1 = (the_arity_of o) . n as SortSymbol of S ; A7: ex ff being Function st ( ff = y & dom ff = dom (the_arity_of o) & rng ff c= Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )) ) by A1, FUNCT_2:def_2; then n in dom y by A5, PRALG_2:3; then y . n in rng y by FUNCT_1:def_3; then consider g being Function such that A8: g = y . n and dom g = I and rng g c= union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } by A7, FUNCT_2:def_2; ( ((commute y) . ii) . n = g . ii & g . ii in the Sorts of (A . ii) . s1 ) by A1, A6, A8, Th16, FUNCT_6:56; hence ((commute y) . ii) . n in ( the Sorts of (A . ii) * (the_arity_of o)) . n by A5, FUNCT_1:12; ::_thesis: verum end; (commute y) . ii in rng (commute y) by A2, FUNCT_1:def_3; then ex h being Function st ( h = (commute y) . ii & dom h = dom (the_arity_of o) & rng h c= union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ) by A2, FUNCT_2:def_2; then dom ((commute y) . ii) = dom ( the Sorts of (A . ii) * (the_arity_of o)) by PRALG_2:3; then (commute y) . ii in product ( the Sorts of (A . ii) * (the_arity_of o)) by A4, CARD_3:9; then (commute y) . ii in Args (o,(A . ii)) by PRALG_2:3; hence (commute y) . i1 in (doms (A ?. o)) . i1 by PRALG_2:11; ::_thesis: verum end; dom (commute y) = dom (doms (A ?. o)) by A2, PRALG_2:11; hence commute y in product (doms (A ?. o)) by A3, CARD_3:9; ::_thesis: verum end; theorem Th18: :: PRALG_3:18 for I being non empty set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds y in dom (Commute (Frege (A ?. o))) proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds y in dom (Commute (Frege (A ?. o))) let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for o being OperSymbol of S for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds y in dom (Commute (Frege (A ?. o))) let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds y in dom (Commute (Frege (A ?. o))) let o be OperSymbol of S; ::_thesis: for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds y in dom (Commute (Frege (A ?. o))) let y be Element of Args (o,(product A)); ::_thesis: ( the_arity_of o <> {} implies y in dom (Commute (Frege (A ?. o))) ) set D = union { ( the Sorts of (A . ii) . ss) where ii is Element of I, ss is Element of the carrier of S : verum } ; assume A1: the_arity_of o <> {} ; ::_thesis: y in dom (Commute (Frege (A ?. o))) then commute y in product (doms (A ?. o)) by Th17; then A2: commute y in dom (Frege (A ?. o)) by PARTFUN1:def_2; y in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . ii) . ss) where ii is Element of I, ss is Element of the carrier of S : verum } )))) by Th14; then y = commute (commute y) by A1, FUNCT_6:57; hence y in dom (Commute (Frege (A ?. o))) by A2, PRALG_2:def_1; ::_thesis: verum end; theorem Th19: :: PRALG_3:19 for I being set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S for x being Element of Args (o,(product A)) holds (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o))) proof let I be set ; ::_thesis: for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S for x being Element of Args (o,(product A)) holds (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o))) let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for o being OperSymbol of S for x being Element of Args (o,(product A)) holds (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o))) let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S for x being Element of Args (o,(product A)) holds (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o))) let o be OperSymbol of S; ::_thesis: for x being Element of Args (o,(product A)) holds (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o))) let x be Element of Args (o,(product A)); ::_thesis: (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o))) Result (o,(product A)) = (SORTS A) . (the_result_sort_of o) by PRALG_2:3 .= product (Carrier (A,(the_result_sort_of o))) by PRALG_2:def_10 ; hence (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o))) ; ::_thesis: verum end; theorem Th20: :: PRALG_3:20 for I being non empty set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for i being Element of I for o being OperSymbol of S st the_arity_of o <> {} holds for U1 being non-empty MSAlgebra over S for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i)) proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for i being Element of I for o being OperSymbol of S st the_arity_of o <> {} holds for U1 being non-empty MSAlgebra over S for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i)) let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for i being Element of I for o being OperSymbol of S st the_arity_of o <> {} holds for U1 being non-empty MSAlgebra over S for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i)) let A be MSAlgebra-Family of I,S; ::_thesis: for i being Element of I for o being OperSymbol of S st the_arity_of o <> {} holds for U1 being non-empty MSAlgebra over S for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i)) let i be Element of I; ::_thesis: for o being OperSymbol of S st the_arity_of o <> {} holds for U1 being non-empty MSAlgebra over S for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i)) let o be OperSymbol of S; ::_thesis: ( the_arity_of o <> {} implies for U1 being non-empty MSAlgebra over S for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i)) ) assume A1: the_arity_of o <> {} ; ::_thesis: for U1 being non-empty MSAlgebra over S for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i)) let U1 be non-empty MSAlgebra over S; ::_thesis: for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i)) let x be Element of Args (o,(product A)); ::_thesis: (commute x) . i is Element of Args (o,(A . i)) i in I ; then A2: i in dom (doms (A ?. o)) by PRALG_2:11; commute x in product (doms (A ?. o)) by A1, Th17; then (commute x) . i in (doms (A ?. o)) . i by A2, CARD_3:9; hence (commute x) . i is Element of Args (o,(A . i)) by PRALG_2:11; ::_thesis: verum end; theorem Th21: :: PRALG_3:21 for I being non empty set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for i being Element of I for o being OperSymbol of S for x being Element of Args (o,(product A)) for n being set st n in dom (the_arity_of o) holds for f being Function st f = x . n holds ((commute x) . i) . n = f . i proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for i being Element of I for o being OperSymbol of S for x being Element of Args (o,(product A)) for n being set st n in dom (the_arity_of o) holds for f being Function st f = x . n holds ((commute x) . i) . n = f . i let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for i being Element of I for o being OperSymbol of S for x being Element of Args (o,(product A)) for n being set st n in dom (the_arity_of o) holds for f being Function st f = x . n holds ((commute x) . i) . n = f . i let A be MSAlgebra-Family of I,S; ::_thesis: for i being Element of I for o being OperSymbol of S for x being Element of Args (o,(product A)) for n being set st n in dom (the_arity_of o) holds for f being Function st f = x . n holds ((commute x) . i) . n = f . i let i be Element of I; ::_thesis: for o being OperSymbol of S for x being Element of Args (o,(product A)) for n being set st n in dom (the_arity_of o) holds for f being Function st f = x . n holds ((commute x) . i) . n = f . i let o be OperSymbol of S; ::_thesis: for x being Element of Args (o,(product A)) for n being set st n in dom (the_arity_of o) holds for f being Function st f = x . n holds ((commute x) . i) . n = f . i let x be Element of Args (o,(product A)); ::_thesis: for n being set st n in dom (the_arity_of o) holds for f being Function st f = x . n holds ((commute x) . i) . n = f . i let n be set ; ::_thesis: ( n in dom (the_arity_of o) implies for f being Function st f = x . n holds ((commute x) . i) . n = f . i ) assume A1: n in dom (the_arity_of o) ; ::_thesis: for f being Function st f = x . n holds ((commute x) . i) . n = f . i set C = union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ; A2: x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )))) by Th14; let g be Function; ::_thesis: ( g = x . n implies ((commute x) . i) . n = g . i ) assume g = x . n ; ::_thesis: ((commute x) . i) . n = g . i hence ((commute x) . i) . n = g . i by A1, A2, FUNCT_6:56; ::_thesis: verum end; theorem Th22: :: PRALG_3:22 for I being non empty set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S st the_arity_of o <> {} holds for y being Element of Args (o,(product A)) for i9 being Element of I for g being Function st g = (Den (o,(product A))) . y holds g . i9 = (Den (o,(A . i9))) . ((commute y) . i9) proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S st the_arity_of o <> {} holds for y being Element of Args (o,(product A)) for i9 being Element of I for g being Function st g = (Den (o,(product A))) . y holds g . i9 = (Den (o,(A . i9))) . ((commute y) . i9) let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for o being OperSymbol of S st the_arity_of o <> {} holds for y being Element of Args (o,(product A)) for i9 being Element of I for g being Function st g = (Den (o,(product A))) . y holds g . i9 = (Den (o,(A . i9))) . ((commute y) . i9) let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S st the_arity_of o <> {} holds for y being Element of Args (o,(product A)) for i9 being Element of I for g being Function st g = (Den (o,(product A))) . y holds g . i9 = (Den (o,(A . i9))) . ((commute y) . i9) let o be OperSymbol of S; ::_thesis: ( the_arity_of o <> {} implies for y being Element of Args (o,(product A)) for i9 being Element of I for g being Function st g = (Den (o,(product A))) . y holds g . i9 = (Den (o,(A . i9))) . ((commute y) . i9) ) assume A1: the_arity_of o <> {} ; ::_thesis: for y being Element of Args (o,(product A)) for i9 being Element of I for g being Function st g = (Den (o,(product A))) . y holds g . i9 = (Den (o,(A . i9))) . ((commute y) . i9) let y be Element of Args (o,(product A)); ::_thesis: for i9 being Element of I for g being Function st g = (Den (o,(product A))) . y holds g . i9 = (Den (o,(A . i9))) . ((commute y) . i9) let i9 be Element of I; ::_thesis: for g being Function st g = (Den (o,(product A))) . y holds g . i9 = (Den (o,(A . i9))) . ((commute y) . i9) A2: y in dom (Commute (Frege (A ?. o))) by A1, Th18; A3: commute y in product (doms (A ?. o)) by A1, Th17; A4: Den (o,(product A)) = (OPS A) . o by MSUALG_1:def_6 .= IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by PRALG_2:def_13 .= Commute (Frege (A ?. o)) by A1, FUNCOP_1:def_8 ; A5: dom (A ?. o) = I by PARTFUN1:def_2; let g be Function; ::_thesis: ( g = (Den (o,(product A))) . y implies g . i9 = (Den (o,(A . i9))) . ((commute y) . i9) ) assume g = (Den (o,(product A))) . y ; ::_thesis: g . i9 = (Den (o,(A . i9))) . ((commute y) . i9) then g = (Frege (A ?. o)) . (commute y) by A4, A2, PRALG_2:def_1 .= (A ?. o) .. (commute y) by A3, PRALG_2:def_2 ; then g . i9 = ((A ?. o) . i9) . ((commute y) . i9) by A5, PRALG_1:def_17 .= (Den (o,(A . i9))) . ((commute y) . i9) by PRALG_2:7 ; hence g . i9 = (Den (o,(A . i9))) . ((commute y) . i9) ; ::_thesis: verum end; begin definition let I be non empty set ; let S be non empty non void ManySortedSign ; let A be MSAlgebra-Family of I,S; let i be Element of I; func proj (A,i) -> ManySortedFunction of (product A),(A . i) means :Def2: :: PRALG_3:def 2 for s being Element of S holds it . s = proj ((Carrier (A,s)),i); existence ex b1 being ManySortedFunction of (product A),(A . i) st for s being Element of S holds b1 . s = proj ((Carrier (A,s)),i) proof deffunc H1( Element of S) -> set = proj ((Carrier (A,\$1)),i); consider F being ManySortedSet of the carrier of S such that A1: for s being Element of S holds F . s = H1(s) from PBOOLE:sch_5(); F is ManySortedFunction of (product A),(A . i) proof let s be set ; :: according to PBOOLE:def_15 ::_thesis: ( not s in the carrier of S or F . s is Element of K10(K11(( the Sorts of (product A) . s),( the Sorts of (A . i) . s))) ) assume A2: s in the carrier of S ; ::_thesis: F . s is Element of K10(K11(( the Sorts of (product A) . s),( the Sorts of (A . i) . s))) F . s is Function of ( the Sorts of (product A) . s),( the Sorts of (A . i) . s) proof reconsider s9 = s as Element of S by A2; F . s = proj ((Carrier (A,s9)),i) by A1; then reconsider F9 = F . s as Function ; A3: rng F9 c= the Sorts of (A . i) . s proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F9 or y in the Sorts of (A . i) . s ) A4: ( dom (Carrier (A,s9)) = I & ex U0 being MSAlgebra over S st ( U0 = A . i & (Carrier (A,s9)) . i = the Sorts of U0 . s9 ) ) by PARTFUN1:def_2, PRALG_2:def_9; assume y in rng F9 ; ::_thesis: y in the Sorts of (A . i) . s then y in rng (proj ((Carrier (A,s9)),i)) by A1; then consider x1 being set such that A5: x1 in dom (proj ((Carrier (A,s9)),i)) and A6: y = (proj ((Carrier (A,s9)),i)) . x1 by FUNCT_1:def_3; A7: x1 in product (Carrier (A,s9)) by A5; then reconsider x1 = x1 as Function ; y = x1 . i by A5, A6, CARD_3:def_16; hence y in the Sorts of (A . i) . s by A7, A4, CARD_3:9; ::_thesis: verum end; dom F9 = dom (proj ((Carrier (A,s9)),i)) by A1 .= product (Carrier (A,s9)) by CARD_3:def_16 .= the Sorts of (product A) . s by PRALG_2:def_10 ; hence F . s is Function of ( the Sorts of (product A) . s),( the Sorts of (A . i) . s) by A2, A3, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; hence F . s is Element of K10(K11(( the Sorts of (product A) . s),( the Sorts of (A . i) . s))) ; ::_thesis: verum end; then reconsider F9 = F as ManySortedFunction of (product A),(A . i) ; take F9 ; ::_thesis: for s being Element of S holds F9 . s = proj ((Carrier (A,s)),i) thus for s being Element of S holds F9 . s = proj ((Carrier (A,s)),i) by A1; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of (product A),(A . i) st ( for s being Element of S holds b1 . s = proj ((Carrier (A,s)),i) ) & ( for s being Element of S holds b2 . s = proj ((Carrier (A,s)),i) ) holds b1 = b2 proof let F, G be ManySortedFunction of (product A),(A . i); ::_thesis: ( ( for s being Element of S holds F . s = proj ((Carrier (A,s)),i) ) & ( for s being Element of S holds G . s = proj ((Carrier (A,s)),i) ) implies F = G ) assume that A8: for s being Element of S holds F . s = proj ((Carrier (A,s)),i) and A9: for s being Element of S holds G . s = proj ((Carrier (A,s)),i) ; ::_thesis: F = G now__::_thesis:_for_s9_being_set_st_s9_in_the_carrier_of_S_holds_ F_._s9_=_G_._s9 let s9 be set ; ::_thesis: ( s9 in the carrier of S implies F . s9 = G . s9 ) assume s9 in the carrier of S ; ::_thesis: F . s9 = G . s9 then reconsider s99 = s9 as Element of S ; thus F . s9 = proj ((Carrier (A,s99)),i) by A8 .= G . s9 by A9 ; ::_thesis: verum end; hence F = G by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def2 defines proj PRALG_3:def_2_:_ for I being non empty set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for i being Element of I for b5 being ManySortedFunction of (product A),(A . i) holds ( b5 = proj (A,i) iff for s being Element of S holds b5 . s = proj ((Carrier (A,s)),i) ); theorem Th23: :: PRALG_3:23 for I being non empty set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S for x being Element of Args (o,(product A)) st the_arity_of o <> {} holds for i being Element of I holds (proj (A,i)) # x = (commute x) . i proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S for x being Element of Args (o,(product A)) st the_arity_of o <> {} holds for i being Element of I holds (proj (A,i)) # x = (commute x) . i let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for o being OperSymbol of S for x being Element of Args (o,(product A)) st the_arity_of o <> {} holds for i being Element of I holds (proj (A,i)) # x = (commute x) . i let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S for x being Element of Args (o,(product A)) st the_arity_of o <> {} holds for i being Element of I holds (proj (A,i)) # x = (commute x) . i let o be OperSymbol of S; ::_thesis: for x being Element of Args (o,(product A)) st the_arity_of o <> {} holds for i being Element of I holds (proj (A,i)) # x = (commute x) . i let x be Element of Args (o,(product A)); ::_thesis: ( the_arity_of o <> {} implies for i being Element of I holds (proj (A,i)) # x = (commute x) . i ) assume A1: the_arity_of o <> {} ; ::_thesis: for i being Element of I holds (proj (A,i)) # x = (commute x) . i set C = union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ; let i be Element of I; ::_thesis: (proj (A,i)) # x = (commute x) . i A2: x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )))) by Th14; then A3: commute x in Funcs (I,(Funcs ((dom (the_arity_of o)),(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )))) by A1, FUNCT_6:55; then dom (commute x) = I by FUNCT_2:92; then A4: (commute x) . i in rng (commute x) by FUNCT_1:def_3; A5: now__::_thesis:_for_n_being_set_st_n_in_dom_(the_arity_of_o)_holds_ ((proj_(A,i))_#_x)_._n_=_((commute_x)_._i)_._n A6: rng x c= Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )) by A2, FUNCT_2:92; let n be set ; ::_thesis: ( n in dom (the_arity_of o) implies ((proj (A,i)) # x) . n = ((commute x) . i) . n ) assume A7: n in dom (the_arity_of o) ; ::_thesis: ((proj (A,i)) # x) . n = ((commute x) . i) . n x . n in product (Carrier (A,((the_arity_of o) /. n))) by A7, Th15; then A8: x . n in dom (proj ((Carrier (A,((the_arity_of o) /. n))),i)) by CARD_3:def_16; n in dom x by A2, A7, FUNCT_2:92; then x . n in rng x by FUNCT_1:def_3; then consider g being Function such that A9: g = x . n and dom g = I and rng g c= union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } by A6, FUNCT_2:def_2; thus ((proj (A,i)) # x) . n = ((proj (A,i)) . ((the_arity_of o) /. n)) . (x . n) by A7, Th13 .= (proj ((Carrier (A,((the_arity_of o) /. n))),i)) . (x . n) by Def2 .= g . i by A9, A8, CARD_3:def_16 .= ((commute x) . i) . n by A2, A7, A9, FUNCT_6:56 ; ::_thesis: verum end; A10: x in product (doms ((proj (A,i)) * (the_arity_of o))) by Th12; rng (commute x) c= Funcs ((dom (the_arity_of o)),(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } )) by A3, FUNCT_2:92; then A11: dom ((commute x) . i) = dom (the_arity_of o) by A4, FUNCT_2:92; dom (proj (A,i)) = the carrier of S by PARTFUN1:def_2; then A12: rng (the_arity_of o) c= dom (proj (A,i)) ; dom ((proj (A,i)) # x) = dom ((Frege ((proj (A,i)) * (the_arity_of o))) . x) by MSUALG_3:def_5 .= dom (((proj (A,i)) * (the_arity_of o)) .. x) by A10, PRALG_2:def_2 .= dom ((proj (A,i)) * (the_arity_of o)) by PRALG_1:def_17 .= dom (the_arity_of o) by A12, RELAT_1:27 ; hence (proj (A,i)) # x = (commute x) . i by A11, A5, FUNCT_1:2; ::_thesis: verum end; theorem :: PRALG_3:24 for I being non empty set for S being non empty non void ManySortedSign for i being Element of I for A being MSAlgebra-Family of I,S holds proj (A,i) is_homomorphism product A,A . i proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for i being Element of I for A being MSAlgebra-Family of I,S holds proj (A,i) is_homomorphism product A,A . i let S be non empty non void ManySortedSign ; ::_thesis: for i being Element of I for A being MSAlgebra-Family of I,S holds proj (A,i) is_homomorphism product A,A . i let i be Element of I; ::_thesis: for A being MSAlgebra-Family of I,S holds proj (A,i) is_homomorphism product A,A . i let A be MSAlgebra-Family of I,S; ::_thesis: proj (A,i) is_homomorphism product A,A . i thus proj (A,i) is_homomorphism product A,A . i ::_thesis: verum proof let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,(product A)) = {} or for b1 being Element of Args (o,(product A)) holds ((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . b1) = (Den (o,(A . i))) . ((proj (A,i)) # b1) ) assume Args (o,(product A)) <> {} ; ::_thesis: for b1 being Element of Args (o,(product A)) holds ((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . b1) = (Den (o,(A . i))) . ((proj (A,i)) # b1) let x be Element of Args (o,(product A)); ::_thesis: ((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(A . i))) . ((proj (A,i)) # x) set F = proj (A,i); set s = the_result_sort_of o; o in the carrier' of S ; then A1: o in dom the ResultSort of S by FUNCT_2:def_1; A2: Result (o,(product A)) = ( the Sorts of (product A) * the ResultSort of S) . o by MSUALG_1:def_5 .= the Sorts of (product A) . ( the ResultSort of S . o) by A1, FUNCT_1:13 .= (SORTS A) . (the_result_sort_of o) by MSUALG_1:def_2 .= product (Carrier (A,(the_result_sort_of o))) by PRALG_2:def_10 ; thus ((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(A . i))) . ((proj (A,i)) # x) ::_thesis: verum proof percases ( the_arity_of o = {} or the_arity_of o <> {} ) ; supposeA3: the_arity_of o = {} ; ::_thesis: ((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(A . i))) . ((proj (A,i)) # x) then const (o,(product A)) in product (Carrier (A,(the_result_sort_of o))) by A2, Th5; then A4: const (o,(product A)) in dom (proj ((Carrier (A,(the_result_sort_of o))),i)) by CARD_3:def_16; A5: Args (o,(product A)) = {{}} by A3, PRALG_2:4; then A6: x = {} by TARSKI:def_1; ((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = ((proj (A,i)) . (the_result_sort_of o)) . (const (o,(product A))) by A5, TARSKI:def_1 .= (proj ((Carrier (A,(the_result_sort_of o))),i)) . (const (o,(product A))) by Def2 .= (const (o,(product A))) . i by A4, CARD_3:def_16 .= const (o,(A . i)) by A3, Th9 .= (Den (o,(A . i))) . ((proj (A,i)) # x) by A3, A6, Th11 ; hence ((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(A . i))) . ((proj (A,i)) # x) ; ::_thesis: verum end; supposeA7: the_arity_of o <> {} ; ::_thesis: ((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(A . i))) . ((proj (A,i)) # x) reconsider D = (Den (o,(product A))) . x as Function by A2; (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o))) by A2; then A8: (Den (o,(product A))) . x in dom (proj ((Carrier (A,(the_result_sort_of o))),i)) by CARD_3:def_16; ((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (proj ((Carrier (A,(the_result_sort_of o))),i)) . ((Den (o,(product A))) . x) by Def2 .= D . i by A8, CARD_3:def_16 .= (Den (o,(A . i))) . ((commute x) . i) by A7, Th22 .= (Den (o,(A . i))) . ((proj (A,i)) # x) by A7, Th23 ; hence ((proj (A,i)) . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(A . i))) . ((proj (A,i)) # x) ; ::_thesis: verum end; end; end; end; end; theorem Th25: :: PRALG_3:25 for I being non empty set for S being non empty non void ManySortedSign for i being Element of I for A being MSAlgebra-Family of I,S for s being SortSymbol of S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds ( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s ) proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for i being Element of I for A being MSAlgebra-Family of I,S for s being SortSymbol of S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds ( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s ) let S be non empty non void ManySortedSign ; ::_thesis: for i being Element of I for A being MSAlgebra-Family of I,S for s being SortSymbol of S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds ( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s ) let i be Element of I; ::_thesis: for A being MSAlgebra-Family of I,S for s being SortSymbol of S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds ( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s ) let A be MSAlgebra-Family of I,S; ::_thesis: for s being SortSymbol of S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds ( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s ) let s be SortSymbol of S; ::_thesis: for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds ( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s ) let U1 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds ( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s ) let F be ManySortedFunction of I; ::_thesis: ( ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) implies ( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s ) ) assume A1: for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ; ::_thesis: ( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s ) set FS = { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ; set CA = the carrier of S; A2: rng F c= Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F or x in Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ) ) assume x in rng F ; ::_thesis: x in Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ) then consider i9 being set such that A3: i9 in dom F and A4: F . i9 = x by FUNCT_1:def_3; reconsider i1 = i9 as Element of I by A3; consider F9 being ManySortedFunction of U1,(A . i1) such that A5: F9 = F . i1 and F9 is_homomorphism U1,A . i1 by A1; A6: rng F9 c= { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } proof let x9 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x9 in rng F9 or x9 in { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ) assume x9 in rng F9 ; ::_thesis: x9 in { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } then consider s9 being set such that A7: s9 in dom F9 and A8: F9 . s9 = x9 by FUNCT_1:def_3; s9 is SortSymbol of S by A7; hence x9 in { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } by A5, A8; ::_thesis: verum end; dom F9 = the carrier of S by PARTFUN1:def_2; hence x in Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ) by A4, A5, A6, FUNCT_2:def_2; ::_thesis: verum end; A9: dom F = I by PARTFUN1:def_2; hence F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) by A2, FUNCT_2:def_2; ::_thesis: ((commute F) . s) . i = (F . i) . s F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) by A9, A2, FUNCT_2:def_2; hence ((commute F) . s) . i = (F . i) . s by FUNCT_6:56; ::_thesis: verum end; theorem Th26: :: PRALG_3:26 for I being non empty set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for s being SortSymbol of S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds (commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for s being SortSymbol of S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds (commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for s being SortSymbol of S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds (commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) let A be MSAlgebra-Family of I,S; ::_thesis: for s being SortSymbol of S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds (commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) let s be SortSymbol of S; ::_thesis: for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds (commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) let U1 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds (commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) let F be ManySortedFunction of I; ::_thesis: ( ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) implies (commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) ) assume A1: for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ; ::_thesis: (commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) set SU = the Sorts of U1; set CA = the carrier of S; set SA = union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ; set SA9 = { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ; set FS = { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ; F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) by A1, Th25; then commute F in Funcs ( the carrier of S,(Funcs (I, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) by FUNCT_6:55; then consider F9 being Function such that A2: ( F9 = commute F & dom F9 = the carrier of S ) and A3: rng F9 c= Funcs (I, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ) by FUNCT_2:def_2; (commute F) . s in rng F9 by A2, FUNCT_1:def_3; then A4: ex F2 being Function st ( F2 = (commute F) . s & dom F2 = I & rng F2 c= { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ) by A3, FUNCT_2:def_2; rng ((commute F) . s) c= Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )) proof let x9 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x9 in rng ((commute F) . s) or x9 in Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )) ) assume x9 in rng ((commute F) . s) ; ::_thesis: x9 in Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )) then consider i9 being set such that A5: i9 in dom ((commute F) . s) and A6: x9 = ((commute F) . s) . i9 by FUNCT_1:def_3; reconsider i1 = i9 as Element of I by A4, A5; consider F9 being ManySortedFunction of U1,(A . i1) such that A7: F9 = F . i1 and F9 is_homomorphism U1,A . i1 by A1; the Sorts of (A . i1) . s c= union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } proof A8: the Sorts of (A . i1) . s in { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the Sorts of (A . i1) . s or y in union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ) assume y in the Sorts of (A . i1) . s ; ::_thesis: y in union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } hence y in union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } by A8, TARSKI:def_4; ::_thesis: verum end; then A9: ( dom (F9 . s) = the Sorts of U1 . s & rng (F9 . s) c= union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ) by FUNCT_2:def_1, XBOOLE_1:1; x9 = F9 . s by A1, A6, A7, Th25; hence x9 in Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )) by A9, FUNCT_2:def_2; ::_thesis: verum end; hence (commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A4, FUNCT_2:def_2; ::_thesis: verum end; theorem Th27: :: PRALG_3:27 for I being non empty set for S being non empty non void ManySortedSign for i being Element of I for A being MSAlgebra-Family of I,S for s being SortSymbol of S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds for x being set st x in the Sorts of U1 . s holds for f being Function st f = (commute ((commute F) . s)) . x holds f . i = (F9 . s) . x proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for i being Element of I for A being MSAlgebra-Family of I,S for s being SortSymbol of S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds for x being set st x in the Sorts of U1 . s holds for f being Function st f = (commute ((commute F) . s)) . x holds f . i = (F9 . s) . x let S be non empty non void ManySortedSign ; ::_thesis: for i being Element of I for A being MSAlgebra-Family of I,S for s being SortSymbol of S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds for x being set st x in the Sorts of U1 . s holds for f being Function st f = (commute ((commute F) . s)) . x holds f . i = (F9 . s) . x let i be Element of I; ::_thesis: for A being MSAlgebra-Family of I,S for s being SortSymbol of S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds for x being set st x in the Sorts of U1 . s holds for f being Function st f = (commute ((commute F) . s)) . x holds f . i = (F9 . s) . x let A be MSAlgebra-Family of I,S; ::_thesis: for s being SortSymbol of S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds for x being set st x in the Sorts of U1 . s holds for f being Function st f = (commute ((commute F) . s)) . x holds f . i = (F9 . s) . x let s be SortSymbol of S; ::_thesis: for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds for x being set st x in the Sorts of U1 . s holds for f being Function st f = (commute ((commute F) . s)) . x holds f . i = (F9 . s) . x let U1 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds for x being set st x in the Sorts of U1 . s holds for f being Function st f = (commute ((commute F) . s)) . x holds f . i = (F9 . s) . x set SU = the Sorts of U1; set SA = union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ; let F be ManySortedFunction of I; ::_thesis: ( ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) implies for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds for x being set st x in the Sorts of U1 . s holds for f being Function st f = (commute ((commute F) . s)) . x holds f . i = (F9 . s) . x ) assume A1: for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ; ::_thesis: for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds for x being set st x in the Sorts of U1 . s holds for f being Function st f = (commute ((commute F) . s)) . x holds f . i = (F9 . s) . x A2: (commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A1, Th26; then dom ((commute F) . s) = I by FUNCT_2:92; then A3: ((commute F) . s) . i in rng ((commute F) . s) by FUNCT_1:def_3; reconsider f9 = (commute F) . s as Function ; rng ((commute F) . s) c= Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )) by A2, FUNCT_2:92; then consider g being Function such that A4: g = f9 . i and dom g = the Sorts of U1 . s and rng g c= union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } by A3, FUNCT_2:def_2; let F9 be ManySortedFunction of U1,(A . i); ::_thesis: ( F9 = F . i implies for x being set st x in the Sorts of U1 . s holds for f being Function st f = (commute ((commute F) . s)) . x holds f . i = (F9 . s) . x ) assume A5: F9 = F . i ; ::_thesis: for x being set st x in the Sorts of U1 . s holds for f being Function st f = (commute ((commute F) . s)) . x holds f . i = (F9 . s) . x let x1 be set ; ::_thesis: ( x1 in the Sorts of U1 . s implies for f being Function st f = (commute ((commute F) . s)) . x1 holds f . i = (F9 . s) . x1 ) assume A6: x1 in the Sorts of U1 . s ; ::_thesis: for f being Function st f = (commute ((commute F) . s)) . x1 holds f . i = (F9 . s) . x1 let f be Function; ::_thesis: ( f = (commute ((commute F) . s)) . x1 implies f . i = (F9 . s) . x1 ) assume A7: f = (commute ((commute F) . s)) . x1 ; ::_thesis: f . i = (F9 . s) . x1 g = F9 . s by A1, A5, A4, Th25; hence f . i = (F9 . s) . x1 by A6, A7, A2, A4, FUNCT_6:56; ::_thesis: verum end; theorem Th28: :: PRALG_3:28 for I being non empty set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for s being SortSymbol of S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds for x being set st x in the Sorts of U1 . s holds (commute ((commute F) . s)) . x in product (Carrier (A,s)) proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for s being SortSymbol of S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds for x being set st x in the Sorts of U1 . s holds (commute ((commute F) . s)) . x in product (Carrier (A,s)) let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for s being SortSymbol of S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds for x being set st x in the Sorts of U1 . s holds (commute ((commute F) . s)) . x in product (Carrier (A,s)) let A be MSAlgebra-Family of I,S; ::_thesis: for s being SortSymbol of S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds for x being set st x in the Sorts of U1 . s holds (commute ((commute F) . s)) . x in product (Carrier (A,s)) let s be SortSymbol of S; ::_thesis: for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds for x being set st x in the Sorts of U1 . s holds (commute ((commute F) . s)) . x in product (Carrier (A,s)) let U1 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds for x being set st x in the Sorts of U1 . s holds (commute ((commute F) . s)) . x in product (Carrier (A,s)) set SU = the Sorts of U1; set SA = union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ; let F be ManySortedFunction of I; ::_thesis: ( ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) implies for x being set st x in the Sorts of U1 . s holds (commute ((commute F) . s)) . x in product (Carrier (A,s)) ) assume A1: for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ; ::_thesis: for x being set st x in the Sorts of U1 . s holds (commute ((commute F) . s)) . x in product (Carrier (A,s)) (commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A1, Th26; then commute ((commute F) . s) in Funcs (( the Sorts of U1 . s),(Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by FUNCT_6:55; then consider f9 being Function such that A2: f9 = commute ((commute F) . s) and A3: dom f9 = the Sorts of U1 . s and A4: rng f9 c= Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )) by FUNCT_2:def_2; let x be set ; ::_thesis: ( x in the Sorts of U1 . s implies (commute ((commute F) . s)) . x in product (Carrier (A,s)) ) assume A5: x in the Sorts of U1 . s ; ::_thesis: (commute ((commute F) . s)) . x in product (Carrier (A,s)) f9 . x in rng f9 by A5, A3, FUNCT_1:def_3; then consider f being Function such that A6: f = (commute ((commute F) . s)) . x and A7: dom f = I and rng f c= union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } by A2, A4, FUNCT_2:def_2; A8: now__::_thesis:_for_i1_being_set_st_i1_in_dom_(Carrier_(A,s))_holds_ ((commute_((commute_F)_._s))_._x)_._i1_in_(Carrier_(A,s))_._i1 let i1 be set ; ::_thesis: ( i1 in dom (Carrier (A,s)) implies ((commute ((commute F) . s)) . x) . i1 in (Carrier (A,s)) . i1 ) assume i1 in dom (Carrier (A,s)) ; ::_thesis: ((commute ((commute F) . s)) . x) . i1 in (Carrier (A,s)) . i1 then reconsider i9 = i1 as Element of I ; consider F1 being ManySortedFunction of U1,(A . i9) such that A9: F1 = F . i9 and F1 is_homomorphism U1,A . i9 by A1; x in dom (F1 . s) by A5, FUNCT_2:def_1; then A10: ( ex U0 being MSAlgebra over S st ( U0 = A . i9 & (Carrier (A,s)) . i9 = the Sorts of U0 . s ) & (F1 . s) . x in rng (F1 . s) ) by FUNCT_1:def_3, PRALG_2:def_9; f . i9 = (F1 . s) . x by A1, A5, A6, A9, Th27; hence ((commute ((commute F) . s)) . x) . i1 in (Carrier (A,s)) . i1 by A6, A10; ::_thesis: verum end; dom ((commute ((commute F) . s)) . x) = dom (Carrier (A,s)) by A6, A7, PARTFUN1:def_2; hence (commute ((commute F) . s)) . x in product (Carrier (A,s)) by A8, CARD_3:9; ::_thesis: verum end; theorem :: PRALG_3:29 for I being non empty set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds ex H being ManySortedFunction of U1,(product A) st ( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) ) proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds ex H being ManySortedFunction of U1,(product A) st ( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) ) let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds ex H being ManySortedFunction of U1,(product A) st ( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) ) let A be MSAlgebra-Family of I,S; ::_thesis: for U1 being non-empty MSAlgebra over S for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds ex H being ManySortedFunction of U1,(product A) st ( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) ) let U1 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds ex H being ManySortedFunction of U1,(product A) st ( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) ) let F be ManySortedFunction of I; ::_thesis: ( ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ) implies ex H being ManySortedFunction of U1,(product A) st ( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) ) ) assume A1: for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st ( F1 = F . i & F1 is_homomorphism U1,A . i ) ; ::_thesis: ex H being ManySortedFunction of U1,(product A) st ( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) ) set SU = the Sorts of U1; set CA = the carrier of S; set SA = union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ; deffunc H1( Element of S) -> set = commute ((commute F) . \$1); consider H being ManySortedSet of the carrier of S such that A2: for s9 being Element of the carrier of S holds H . s9 = H1(s9) from PBOOLE:sch_5(); now__::_thesis:_for_s9_being_set_st_s9_in_the_carrier_of_S_holds_ H_._s9_is_Function_of_(_the_Sorts_of_U1_._s9),(_the_Sorts_of_(product_A)_._s9) let s9 be set ; ::_thesis: ( s9 in the carrier of S implies H . s9 is Function of ( the Sorts of U1 . s9),( the Sorts of (product A) . s9) ) assume A3: s9 in the carrier of S ; ::_thesis: H . s9 is Function of ( the Sorts of U1 . s9),( the Sorts of (product A) . s9) then reconsider s99 = s9 as SortSymbol of S ; (commute F) . s9 in Funcs (I,(Funcs (( the Sorts of U1 . s9),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A1, A3, Th26; then commute ((commute F) . s9) in Funcs (( the Sorts of U1 . s9),(Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A3, FUNCT_6:55; then H . s9 in Funcs (( the Sorts of U1 . s9),(Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A2, A3; then consider Hs being Function such that A4: Hs = H . s9 and A5: dom Hs = the Sorts of U1 . s9 and A6: rng Hs c= Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )) by FUNCT_2:def_2; rng Hs c= the Sorts of (product A) . s9 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng Hs or x in the Sorts of (product A) . s9 ) assume A7: x in rng Hs ; ::_thesis: x in the Sorts of (product A) . s9 then consider f being Function such that A8: f = x and A9: dom f = I and rng f c= union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } by A6, FUNCT_2:def_2; consider x1 being set such that A10: x1 in dom Hs and A11: Hs . x1 = f by A7, A8, FUNCT_1:def_3; A12: now__::_thesis:_for_i9_being_set_st_i9_in_dom_(Carrier_(A,s99))_holds_ f_._i9_in_(Carrier_(A,s99))_._i9 let i9 be set ; ::_thesis: ( i9 in dom (Carrier (A,s99)) implies f . i9 in (Carrier (A,s99)) . i9 ) assume i9 in dom (Carrier (A,s99)) ; ::_thesis: f . i9 in (Carrier (A,s99)) . i9 then reconsider i99 = i9 as Element of I ; consider F9 being ManySortedFunction of U1,(A . i99) such that A13: F9 = F . i99 and F9 is_homomorphism U1,A . i99 by A1; H . s99 = commute ((commute F) . s99) by A2; then A14: f . i99 = (F9 . s99) . x1 by A1, A4, A5, A10, A11, A13, Th27; dom (F9 . s99) = dom Hs by A5, FUNCT_2:def_1; then A15: (F9 . s9) . x1 in rng (F9 . s9) by A10, FUNCT_1:def_3; ( ex U0 being MSAlgebra over S st ( U0 = A . i99 & (Carrier (A,s99)) . i99 = the Sorts of U0 . s99 ) & rng (F9 . s99) c= the Sorts of (A . i99) . s99 ) by PRALG_2:def_9; hence f . i9 in (Carrier (A,s99)) . i9 by A14, A15; ::_thesis: verum end; dom (Carrier (A,s99)) = dom f by A9, PARTFUN1:def_2; then f in product (Carrier (A,s99)) by A12, CARD_3:9; hence x in the Sorts of (product A) . s9 by A8, PRALG_2:def_10; ::_thesis: verum end; hence H . s9 is Function of ( the Sorts of U1 . s9),( the Sorts of (product A) . s9) by A3, A4, A5, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; then reconsider H = H as ManySortedFunction of U1,(product A) by PBOOLE:def_15; A16: H is_homomorphism U1, product A proof let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,U1) = {} or for b1 being Element of Args (o,U1) holds (H . (the_result_sort_of o)) . ((Den (o,U1)) . b1) = (Den (o,(product A))) . (H # b1) ) assume Args (o,U1) <> {} ; ::_thesis: for b1 being Element of Args (o,U1) holds (H . (the_result_sort_of o)) . ((Den (o,U1)) . b1) = (Den (o,(product A))) . (H # b1) let x be Element of Args (o,U1); ::_thesis: (H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x) set s9 = the_result_sort_of o; A17: Result (o,U1) = the Sorts of U1 . (the_result_sort_of o) by PRALG_2:3; then A18: (Den (o,U1)) . x in the Sorts of U1 . (the_result_sort_of o) ; thus (H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x) ::_thesis: verum proof percases ( the_arity_of o = {} or the_arity_of o <> {} ) ; supposeA19: the_arity_of o = {} ; ::_thesis: (H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x) set f = (commute ((commute F) . (the_result_sort_of o))) . (const (o,U1)); Args (o,U1) = {{}} by A19, PRALG_2:4; then A20: x = {} by TARSKI:def_1; A21: now__::_thesis:_for_i9_being_set_st_i9_in_I_holds_ ((commute_((commute_F)_._(the_result_sort_of_o)))_._(const_(o,U1)))_._i9_=_(const_(o,(product_A)))_._i9 let i9 be set ; ::_thesis: ( i9 in I implies ((commute ((commute F) . (the_result_sort_of o))) . (const (o,U1))) . i9 = (const (o,(product A))) . i9 ) assume i9 in I ; ::_thesis: ((commute ((commute F) . (the_result_sort_of o))) . (const (o,U1))) . i9 = (const (o,(product A))) . i9 then reconsider ii = i9 as Element of I ; consider F1 being ManySortedFunction of U1,(A . ii) such that A22: F1 = F . ii and A23: F1 is_homomorphism U1,A . ii by A1; A24: F1 # x = {} by A19, A20, Th11; thus ((commute ((commute F) . (the_result_sort_of o))) . (const (o,U1))) . i9 = (F1 . (the_result_sort_of o)) . ((Den (o,U1)) . x) by A1, A17, A20, A22, Th27 .= const (o,(A . ii)) by A23, A24, MSUALG_3:def_7 .= (const (o,(product A))) . i9 by A19, Th9 ; ::_thesis: verum end; const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i1))) where i1 is Element of I : verum } )) by A19, Th8; then A25: ex Co being Function st ( Co = const (o,(product A)) & dom Co = I & rng Co c= union { (Result (o,(A . i1))) where i1 is Element of I : verum } ) by FUNCT_2:def_2; (commute ((commute F) . (the_result_sort_of o))) . (const (o,U1)) in product (Carrier (A,(the_result_sort_of o))) by A1, A18, A20, Th28; then dom ((commute ((commute F) . (the_result_sort_of o))) . (const (o,U1))) = dom (Carrier (A,(the_result_sort_of o))) by CARD_3:9 .= I by PARTFUN1:def_2 ; then A26: (commute ((commute F) . (the_result_sort_of o))) . (const (o,U1)) = const (o,(product A)) by A25, A21, FUNCT_1:2; H # x = {} by A19, A20, Th11; hence (H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x) by A2, A20, A26; ::_thesis: verum end; supposeA27: the_arity_of o <> {} ; ::_thesis: (H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x) A28: Den (o,(product A)) = (OPS A) . o by MSUALG_1:def_6 .= IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by PRALG_2:def_13 .= Commute (Frege (A ?. o)) by A27, FUNCOP_1:def_8 ; A29: now__::_thesis:_for_y_being_Element_of_Args_(o,(product_A))_holds_(Den_(o,(product_A)))_._y_in_rng_(Frege_(A_?._o)) let y be Element of Args (o,(product A)); ::_thesis: (Den (o,(product A))) . y in rng (Frege (A ?. o)) commute y in product (doms (A ?. o)) by A27, Th17; then A30: commute y in dom (Frege (A ?. o)) by PARTFUN1:def_2; y in dom (Commute (Frege (A ?. o))) by A27, Th18; then (Den (o,(product A))) . y = (Frege (A ?. o)) . (commute y) by A28, PRALG_2:def_1; hence (Den (o,(product A))) . y in rng (Frege (A ?. o)) by A30, FUNCT_1:def_3; ::_thesis: verum end; then reconsider f1 = (Den (o,(product A))) . (H # x) as Function by PRALG_2:8; f1 in rng (Frege (A ?. o)) by A29; then A31: dom f1 = I by PRALG_2:9; set D = union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } ; set f = (commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x); A32: H # x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } )))) by Th14; A33: now__::_thesis:_for_i9_being_set_st_i9_in_I_holds_ ((commute_((commute_F)_._(the_result_sort_of_o)))_._((Den_(o,U1))_._x))_._i9_=_f1_._i9 let i9 be set ; ::_thesis: ( i9 in I implies ((commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x)) . i9 = f1 . i9 ) assume i9 in I ; ::_thesis: ((commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x)) . i9 = f1 . i9 then reconsider ii = i9 as Element of I ; consider F1 being ManySortedFunction of U1,(A . ii) such that A34: F1 = F . ii and A35: F1 is_homomorphism U1,A . ii by A1; A36: (F1 . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(A . ii))) . (F1 # x) by A35, MSUALG_3:def_7; A37: now__::_thesis:_for_n_being_set_st_n_in_dom_(the_arity_of_o)_holds_ ((commute_(H_#_x))_._ii)_._n_=_(F1_#_x)_._n let n be set ; ::_thesis: ( n in dom (the_arity_of o) implies ((commute (H # x)) . ii) . n = (F1 # x) . n ) assume A38: n in dom (the_arity_of o) ; ::_thesis: ((commute (H # x)) . ii) . n = (F1 # x) . n then (the_arity_of o) . n in rng (the_arity_of o) by FUNCT_1:def_3; then reconsider s1 = (the_arity_of o) . n as Element of the carrier of S ; A39: (F1 # x) . n = (F1 . ((the_arity_of o) /. n)) . (x . n) by A38, Th13 .= (F1 . s1) . (x . n) by A38, PARTFUN1:def_6 ; x in Args (o,U1) ; then A40: x in product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3; then A41: dom x = dom ( the Sorts of U1 * (the_arity_of o)) by CARD_3:9; A42: dom x = dom ( the Sorts of U1 * (the_arity_of o)) by A40, CARD_3:9 .= dom (the_arity_of o) by PRALG_2:3 ; then x . n in ( the Sorts of U1 * (the_arity_of o)) . n by A38, A40, A41, CARD_3:9; then A43: x . n in the Sorts of U1 . s1 by A38, A42, A41, FUNCT_1:12; A44: (H # x) . n = (H . ((the_arity_of o) /. n)) . (x . n) by A38, Th13 .= (H . s1) . (x . n) by A38, PARTFUN1:def_6 .= (commute ((commute F) . s1)) . (x . n) by A2 ; then reconsider g = (H # x) . n as Function ; thus ((commute (H # x)) . ii) . n = g . ii by A32, A38, FUNCT_6:56 .= (F1 # x) . n by A1, A34, A43, A39, A44, Th27 ; ::_thesis: verum end; dom F1 = the carrier of S by PARTFUN1:def_2; then A45: rng (the_arity_of o) c= dom F1 ; commute (H # x) in Funcs (I,(Funcs ((dom (the_arity_of o)),(union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } )))) by A27, A32, FUNCT_6:55; then consider ff being Function such that A46: ff = commute (H # x) and A47: dom ff = I and A48: rng ff c= Funcs ((dom (the_arity_of o)),(union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } )) by FUNCT_2:def_2; ff . ii in rng ff by A47, FUNCT_1:def_3; then A49: ex gg being Function st ( gg = (commute (H # x)) . ii & dom gg = dom (the_arity_of o) & rng gg c= union { ( the Sorts of (A . i9) . ss) where i9 is Element of I, ss is Element of the carrier of S : verum } ) by A46, A48, FUNCT_2:def_2; A50: x in product (doms (F1 * (the_arity_of o))) by Th12; dom (F1 # x) = dom ((Frege (F1 * (the_arity_of o))) . x) by MSUALG_3:def_5 .= dom ((F1 * (the_arity_of o)) .. x) by A50, PRALG_2:def_2 .= dom (F1 * (the_arity_of o)) by PRALG_1:def_17 .= dom (the_arity_of o) by A45, RELAT_1:27 ; then F1 # x = (commute (H # x)) . ii by A49, A37, FUNCT_1:2; then ((commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x)) . i9 = (Den (o,(A . ii))) . ((commute (H # x)) . ii) by A1, A17, A34, A36, Th27 .= f1 . i9 by A27, Th22 ; hence ((commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x)) . i9 = f1 . i9 ; ::_thesis: verum end; (commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x) in product (Carrier (A,(the_result_sort_of o))) by A1, A17, Th28; then dom ((commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x)) = dom (Carrier (A,(the_result_sort_of o))) by CARD_3:9 .= I by PARTFUN1:def_2 ; then (commute ((commute F) . (the_result_sort_of o))) . ((Den (o,U1)) . x) = f1 by A31, A33, FUNCT_1:2; hence (H . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(product A))) . (H # x) by A2; ::_thesis: verum end; end; end; end; take H ; ::_thesis: ( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) ) for i being Element of I holds (proj (A,i)) ** H = F . i proof let i be Element of I; ::_thesis: (proj (A,i)) ** H = F . i consider F1 being ManySortedFunction of U1,(A . i) such that A51: F1 = F . i and F1 is_homomorphism U1,A . i by A1; A52: dom ((proj (A,i)) ** H) = (dom (proj (A,i))) /\ (dom H) by PBOOLE:def_19 .= the carrier of S /\ (dom H) by PARTFUN1:def_2 .= the carrier of S /\ the carrier of S by PARTFUN1:def_2 .= the carrier of S ; A53: now__::_thesis:_for_s9_being_set_st_s9_in_the_carrier_of_S_holds_ ((proj_(A,i))_**_H)_._s9_=_F1_._s9 let s9 be set ; ::_thesis: ( s9 in the carrier of S implies ((proj (A,i)) ** H) . s9 = F1 . s9 ) assume s9 in the carrier of S ; ::_thesis: ((proj (A,i)) ** H) . s9 = F1 . s9 then reconsider s1 = s9 as SortSymbol of S ; A54: ((proj (A,i)) ** H) . s9 = ((proj (A,i)) . s1) * (H . s1) by A52, PBOOLE:def_19 .= (proj ((Carrier (A,s1)),i)) * (H . s1) by Def2 .= (proj ((Carrier (A,s1)),i)) * (commute ((commute F) . s1)) by A2 ; (commute F) . s1 in Funcs (I,(Funcs (( the Sorts of U1 . s1),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by A1, Th26; then commute ((commute F) . s1) in Funcs (( the Sorts of U1 . s1),(Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )))) by FUNCT_6:55; then consider f9 being Function such that A55: f9 = commute ((commute F) . s1) and A56: dom f9 = the Sorts of U1 . s1 and rng f9 c= Funcs (I,(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } )) by FUNCT_2:def_2; rng f9 c= dom (proj ((Carrier (A,s1)),i)) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f9 or y in dom (proj ((Carrier (A,s1)),i)) ) assume y in rng f9 ; ::_thesis: y in dom (proj ((Carrier (A,s1)),i)) then consider x9 being set such that A57: x9 in dom f9 and A58: f9 . x9 = y by FUNCT_1:def_3; (commute ((commute F) . s1)) . x9 in product (Carrier (A,s1)) by A1, A56, A57, Th28; hence y in dom (proj ((Carrier (A,s1)),i)) by A55, A58, CARD_3:def_16; ::_thesis: verum end; then A59: dom (((proj (A,i)) ** H) . s9) = the Sorts of U1 . s9 by A55, A56, A54, RELAT_1:27; A60: now__::_thesis:_for_x_being_set_st_x_in_the_Sorts_of_U1_._s9_holds_ (((proj_(A,i))_**_H)_._s9)_._x_=_(F1_._s9)_._x let x be set ; ::_thesis: ( x in the Sorts of U1 . s9 implies (((proj (A,i)) ** H) . s9) . x = (F1 . s9) . x ) assume A61: x in the Sorts of U1 . s9 ; ::_thesis: (((proj (A,i)) ** H) . s9) . x = (F1 . s9) . x then (commute ((commute F) . s1)) . x in product (Carrier (A,s1)) by A1, Th28; then A62: (commute ((commute F) . s1)) . x in dom (proj ((Carrier (A,s1)),i)) by CARD_3:def_16; thus (((proj (A,i)) ** H) . s9) . x = (proj ((Carrier (A,s1)),i)) . ((commute ((commute F) . s1)) . x) by A54, A59, A61, FUNCT_1:12 .= ((commute ((commute F) . s1)) . x) . i by A62, CARD_3:def_16 .= (F1 . s9) . x by A1, A51, A61, Th27 ; ::_thesis: verum end; dom (F1 . s9) = dom (F1 . s1) .= the Sorts of U1 . s9 by FUNCT_2:def_1 ; hence ((proj (A,i)) ** H) . s9 = F1 . s9 by A59, A60, FUNCT_1:2; ::_thesis: verum end; dom F1 = the carrier of S by PARTFUN1:def_2; hence (proj (A,i)) ** H = F . i by A51, A52, A53, FUNCT_1:2; ::_thesis: verum end; hence ( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) ) by A16; ::_thesis: verum end; begin definition let I be non empty set ; let J be ManySortedSet of I; let S be non empty non void ManySortedSign ; mode MSAlgebra-Class of S,J -> ManySortedSet of I means :Def3: :: PRALG_3:def 3 for i being set st i in I holds it . i is MSAlgebra-Family of J . i,S; existence ex b1 being ManySortedSet of I st for i being set st i in I holds b1 . i is MSAlgebra-Family of J . i,S proof defpred S1[ set , set ] means \$2 is MSAlgebra-Family of J . \$1,S; A1: for i being set st i in I holds ex F being set st S1[i,F] proof let i be set ; ::_thesis: ( i in I implies ex F being set st S1[i,F] ) assume i in I ; ::_thesis: ex F being set st S1[i,F] set F = the MSAlgebra-Family of J . i,S; take the MSAlgebra-Family of J . i,S ; ::_thesis: S1[i, the MSAlgebra-Family of J . i,S] thus S1[i, the MSAlgebra-Family of J . i,S] ; ::_thesis: verum end; consider C being ManySortedSet of I such that A2: for i being set st i in I holds S1[i,C . i] from PBOOLE:sch_3(A1); take C ; ::_thesis: for i being set st i in I holds C . i is MSAlgebra-Family of J . i,S thus for i being set st i in I holds C . i is MSAlgebra-Family of J . i,S by A2; ::_thesis: verum end; end; :: deftheorem Def3 defines MSAlgebra-Class PRALG_3:def_3_:_ for I being non empty set for J being ManySortedSet of I for S being non empty non void ManySortedSign for b4 being ManySortedSet of I holds ( b4 is MSAlgebra-Class of S,J iff for i being set st i in I holds b4 . i is MSAlgebra-Family of J . i,S ); definition let I be non empty set ; let S be non empty non void ManySortedSign ; let A be MSAlgebra-Family of I,S; let EqR be Equivalence_Relation of I; funcA / EqR -> MSAlgebra-Class of S, id (Class EqR) means :Def4: :: PRALG_3:def 4 for c being set st c in Class EqR holds it . c = A | c; existence ex b1 being MSAlgebra-Class of S, id (Class EqR) st for c being set st c in Class EqR holds b1 . c = A | c proof thus ex X being MSAlgebra-Class of S, id (Class EqR) st for c being set st c in Class EqR holds X . c = A | c ::_thesis: verum proof deffunc H1( set ) -> set = A | \$1; consider X being ManySortedSet of Class EqR such that A1: for c being set st c in Class EqR holds X . c = H1(c) from PBOOLE:sch_4(); X is MSAlgebra-Class of S, id (Class EqR) proof let c be set ; :: according to PRALG_3:def_3 ::_thesis: ( c in Class EqR implies X . c is MSAlgebra-Family of (id (Class EqR)) . c,S ) assume A2: c in Class EqR ; ::_thesis: X . c is MSAlgebra-Family of (id (Class EqR)) . c,S A3: dom (A | c) = (dom A) /\ c by RELAT_1:61 .= I /\ c by PARTFUN1:def_2 .= c by A2, XBOOLE_1:28 .= (id (Class EqR)) . c by A2, FUNCT_1:18 ; then reconsider ac = A | c as ManySortedSet of (id (Class EqR)) . c by PARTFUN1:def_2, RELAT_1:def_18; ac is MSAlgebra-Family of (id (Class EqR)) . c,S proof let i be set ; :: according to PRALG_2:def_5 ::_thesis: ( not i in (id (Class EqR)) . c or ac . i is MSAlgebra over S ) assume A4: i in (id (Class EqR)) . c ; ::_thesis: ac . i is MSAlgebra over S dom ac = c by A2, A3, FUNCT_1:18; then reconsider i9 = i as Element of I by A2, A3, A4; A . i9 is non-empty MSAlgebra over S ; hence ac . i is MSAlgebra over S by A3, A4, FUNCT_1:47; ::_thesis: verum end; hence X . c is MSAlgebra-Family of (id (Class EqR)) . c,S by A1, A2; ::_thesis: verum end; then reconsider X = X as MSAlgebra-Class of S, id (Class EqR) ; take X ; ::_thesis: for c being set st c in Class EqR holds X . c = A | c thus for c being set st c in Class EqR holds X . c = A | c by A1; ::_thesis: verum end; end; uniqueness for b1, b2 being MSAlgebra-Class of S, id (Class EqR) st ( for c being set st c in Class EqR holds b1 . c = A | c ) & ( for c being set st c in Class EqR holds b2 . c = A | c ) holds b1 = b2 proof for X, Y being MSAlgebra-Class of S, id (Class EqR) st ( for c being set st c in Class EqR holds X . c = A | c ) & ( for c being set st c in Class EqR holds Y . c = A | c ) holds X = Y proof let X, Y be MSAlgebra-Class of S, id (Class EqR); ::_thesis: ( ( for c being set st c in Class EqR holds X . c = A | c ) & ( for c being set st c in Class EqR holds Y . c = A | c ) implies X = Y ) assume that A5: for c being set st c in Class EqR holds X . c = A | c and A6: for c being set st c in Class EqR holds Y . c = A | c ; ::_thesis: X = Y now__::_thesis:_for_c_being_set_st_c_in_Class_EqR_holds_ X_._c_=_Y_._c let c be set ; ::_thesis: ( c in Class EqR implies X . c = Y . c ) assume A7: c in Class EqR ; ::_thesis: X . c = Y . c hence X . c = A | c by A5 .= Y . c by A6, A7 ; ::_thesis: verum end; hence X = Y by PBOOLE:3; ::_thesis: verum end; hence for b1, b2 being MSAlgebra-Class of S, id (Class EqR) st ( for c being set st c in Class EqR holds b1 . c = A | c ) & ( for c being set st c in Class EqR holds b2 . c = A | c ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def4 defines / PRALG_3:def_4_:_ for I being non empty set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for EqR being Equivalence_Relation of I for b5 being MSAlgebra-Class of S, id (Class EqR) holds ( b5 = A / EqR iff for c being set st c in Class EqR holds b5 . c = A | c ); definition let I be non empty set ; let S be non empty non void ManySortedSign ; let J be V8() ManySortedSet of I; let C be MSAlgebra-Class of S,J; func product C -> MSAlgebra-Family of I,S means :Def5: :: PRALG_3:def 5 for i being Element of I st i in I holds ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st ( Ji = J . i & Cs = C . i & it . i = product Cs ); existence ex b1 being MSAlgebra-Family of I,S st for i being Element of I st i in I holds ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st ( Ji = J . i & Cs = C . i & b1 . i = product Cs ) proof thus ex PC being MSAlgebra-Family of I,S st for i being Element of I st i in I holds ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st ( Ji = J . i & Cs = C . i & PC . i = product Cs ) ::_thesis: verum proof defpred S1[ set , set ] means ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st ( Ji = J . \$1 & Cs = C . \$1 & \$2 = product Cs ); A1: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ ex_j_being_set_st_S1[i,j] let i be set ; ::_thesis: ( i in I implies ex j being set st S1[i,j] ) assume A2: i in I ; ::_thesis: ex j being set st S1[i,j] then reconsider Ji = J . i as non empty set ; reconsider Cs = C . i as MSAlgebra-Family of Ji,S by A2, Def3; ex a being set st a = product Cs ; then consider j being set such that A3: ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st ( Ji = J . i & Cs = C . i & j = product Cs ) ; take j = j; ::_thesis: S1[i,j] thus S1[i,j] by A3; ::_thesis: verum end; consider PC being ManySortedSet of I such that A4: for i being set st i in I holds S1[i,PC . i] from PBOOLE:sch_3(A1); now__::_thesis:_for_i_being_set_st_i_in_I_holds_ PC_._i_is_non-empty_MSAlgebra_over_S let i be set ; ::_thesis: ( i in I implies PC . i is non-empty MSAlgebra over S ) assume i in I ; ::_thesis: PC . i is non-empty MSAlgebra over S then ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st ( Ji = J . i & Cs = C . i & PC . i = product Cs ) by A4; hence PC . i is non-empty MSAlgebra over S ; ::_thesis: verum end; then reconsider PC = PC as MSAlgebra-Family of I,S by PRALG_2:def_5; take PC ; ::_thesis: for i being Element of I st i in I holds ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st ( Ji = J . i & Cs = C . i & PC . i = product Cs ) thus for i being Element of I st i in I holds ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st ( Ji = J . i & Cs = C . i & PC . i = product Cs ) by A4; ::_thesis: verum end; end; uniqueness for b1, b2 being MSAlgebra-Family of I,S st ( for i being Element of I st i in I holds ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st ( Ji = J . i & Cs = C . i & b1 . i = product Cs ) ) & ( for i being Element of I st i in I holds ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st ( Ji = J . i & Cs = C . i & b2 . i = product Cs ) ) holds b1 = b2 proof for PC1, PC2 being MSAlgebra-Family of I,S st ( for i being Element of I st i in I holds ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st ( Ji = J . i & Cs = C . i & PC1 . i = product Cs ) ) & ( for i being Element of I st i in I holds ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st ( Ji = J . i & Cs = C . i & PC2 . i = product Cs ) ) holds PC1 = PC2 proof let PC1, PC2 be MSAlgebra-Family of I,S; ::_thesis: ( ( for i being Element of I st i in I holds ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st ( Ji = J . i & Cs = C . i & PC1 . i = product Cs ) ) & ( for i being Element of I st i in I holds ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st ( Ji = J . i & Cs = C . i & PC2 . i = product Cs ) ) implies PC1 = PC2 ) assume A5: ( ( for i being Element of I st i in I holds ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st ( Ji = J . i & Cs = C . i & PC1 . i = product Cs ) ) & ( for i being Element of I st i in I holds ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st ( Ji = J . i & Cs = C . i & PC2 . i = product Cs ) ) ) ; ::_thesis: PC1 = PC2 now__::_thesis:_for_i1_being_set_st_i1_in_I_holds_ PC1_._i1_=_PC2_._i1 let i1 be set ; ::_thesis: ( i1 in I implies PC1 . i1 = PC2 . i1 ) assume i1 in I ; ::_thesis: PC1 . i1 = PC2 . i1 then reconsider i9 = i1 as Element of I ; ( ex Ji1 being non empty set ex Cs1 being MSAlgebra-Family of Ji1,S st ( Ji1 = J . i9 & Cs1 = C . i9 & PC1 . i9 = product Cs1 ) & ex Ji2 being non empty set ex Cs2 being MSAlgebra-Family of Ji2,S st ( Ji2 = J . i9 & Cs2 = C . i9 & PC2 . i9 = product Cs2 ) ) by A5; hence PC1 . i1 = PC2 . i1 ; ::_thesis: verum end; hence PC1 = PC2 by PBOOLE:3; ::_thesis: verum end; hence for b1, b2 being MSAlgebra-Family of I,S st ( for i being Element of I st i in I holds ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st ( Ji = J . i & Cs = C . i & b1 . i = product Cs ) ) & ( for i being Element of I st i in I holds ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st ( Ji = J . i & Cs = C . i & b2 . i = product Cs ) ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def5 defines product PRALG_3:def_5_:_ for I being non empty set for S being non empty non void ManySortedSign for J being V8() ManySortedSet of I for C being MSAlgebra-Class of S,J for b5 being MSAlgebra-Family of I,S holds ( b5 = product C iff for i being Element of I st i in I holds ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st ( Ji = J . i & Cs = C . i & b5 . i = product Cs ) ); theorem :: PRALG_3:30 for I being non empty set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for EqR being Equivalence_Relation of I holds product A, product (product (A / EqR)) are_isomorphic proof let I be non empty set ; ::_thesis: for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for EqR being Equivalence_Relation of I holds product A, product (product (A / EqR)) are_isomorphic let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for EqR being Equivalence_Relation of I holds product A, product (product (A / EqR)) are_isomorphic let A be MSAlgebra-Family of I,S; ::_thesis: for EqR being Equivalence_Relation of I holds product A, product (product (A / EqR)) are_isomorphic let EqR be Equivalence_Relation of I; ::_thesis: product A, product (product (A / EqR)) are_isomorphic set U1 = product A; set U2 = product (product (A / EqR)); set U19 = the Sorts of (product A); set U29 = the Sorts of (product (product (A / EqR))); defpred S1[ set , set , set ] means for f1, g1 being Function st f1 = \$2 & g1 = \$1 holds for e being Element of Class EqR holds g1 . e = f1 | e; A1: for s being set st s in the carrier of S holds for x being set st x in the Sorts of (product A) . s holds ex y being set st ( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] ) proof let s be set ; ::_thesis: ( s in the carrier of S implies for x being set st x in the Sorts of (product A) . s holds ex y being set st ( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] ) ) assume s in the carrier of S ; ::_thesis: for x being set st x in the Sorts of (product A) . s holds ex y being set st ( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] ) then reconsider s9 = s as SortSymbol of S ; A2: the Sorts of (product A) . s9 = product (Carrier (A,s9)) by PRALG_2:def_10; let x be set ; ::_thesis: ( x in the Sorts of (product A) . s implies ex y being set st ( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] ) ) assume A3: x in the Sorts of (product A) . s ; ::_thesis: ex y being set st ( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] ) reconsider x = x as Function by A3, A2; deffunc H1( set ) -> set = x | \$1; consider y being ManySortedSet of Class EqR such that A4: for c being set st c in Class EqR holds y . c = H1(c) from PBOOLE:sch_4(); A5: dom (Carrier ((product (A / EqR)),s9)) = Class EqR by PARTFUN1:def_2; A6: for a being set st a in dom (Carrier ((product (A / EqR)),s9)) holds y . a in (Carrier ((product (A / EqR)),s9)) . a proof set A9 = product (A / EqR); let a be set ; ::_thesis: ( a in dom (Carrier ((product (A / EqR)),s9)) implies y . a in (Carrier ((product (A / EqR)),s9)) . a ) assume A7: a in dom (Carrier ((product (A / EqR)),s9)) ; ::_thesis: y . a in (Carrier ((product (A / EqR)),s9)) . a A8: (A / EqR) . a = A | a by A7, Def4; reconsider a = a as non empty Subset of I by A5, A7; A9: ex U0 being MSAlgebra over S st ( U0 = (product (A / EqR)) . a & (Carrier ((product (A / EqR)),s9)) . a = the Sorts of U0 . s9 ) by A7, PRALG_2:def_9; A10: dom (A | a) = (dom A) /\ a by RELAT_1:61 .= I /\ a by PARTFUN1:def_2 .= a by XBOOLE_1:28 ; then reconsider Aa1 = A | a as ManySortedSet of a by PARTFUN1:def_2; for i being set st i in a holds Aa1 . i is non-empty MSAlgebra over S proof let i be set ; ::_thesis: ( i in a implies Aa1 . i is non-empty MSAlgebra over S ) assume A11: i in a ; ::_thesis: Aa1 . i is non-empty MSAlgebra over S then A . i is non-empty MSAlgebra over S by PRALG_2:def_5; hence Aa1 . i is non-empty MSAlgebra over S by A10, A11, FUNCT_1:47; ::_thesis: verum end; then reconsider Aa = Aa1 as MSAlgebra-Family of a,S by PRALG_2:def_5; x | a in product ((Carrier (A,s9)) | a) by A3, A2, Th1; then A12: x | a in product (Carrier (Aa,s9)) by Th2; consider Ji being non empty set , Cs being MSAlgebra-Family of Ji,S such that A13: Ji = (id (Class EqR)) . a and A14: ( Cs = (A / EqR) . a & (product (A / EqR)) . a = product Cs ) by A7, Def5; Ji = a by A7, A13, FUNCT_1:18; then (Carrier ((product (A / EqR)),s9)) . a = product (Carrier (Aa,s9)) by A8, A14, A9, PRALG_2:def_10; hence y . a in (Carrier ((product (A / EqR)),s9)) . a by A4, A7, A12; ::_thesis: verum end; take y ; ::_thesis: ( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] ) dom (Carrier ((product (A / EqR)),s9)) = Class EqR by PARTFUN1:def_2 .= dom y by PARTFUN1:def_2 ; then y in product (Carrier ((product (A / EqR)),s9)) by A6, CARD_3:9; hence ( y in the Sorts of (product (product (A / EqR))) . s & S1[y,x,s] ) by A4, PRALG_2:def_10; ::_thesis: verum end; consider F being ManySortedFunction of the Sorts of (product A), the Sorts of (product (product (A / EqR))) such that A15: for s being set st s in the carrier of S holds ex f being Function of ( the Sorts of (product A) . s),( the Sorts of (product (product (A / EqR))) . s) st ( f = F . s & ( for x being set st x in the Sorts of (product A) . s holds S1[f . x,x,s] ) ) from MSSUBFAM:sch_1(A1); A16: F is_homomorphism product A, product (product (A / EqR)) proof let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,(product A)) = {} or for b1 being Element of Args (o,(product A)) holds (F . (the_result_sort_of o)) . ((Den (o,(product A))) . b1) = (Den (o,(product (product (A / EqR))))) . (F # b1) ) assume Args (o,(product A)) <> {} ; ::_thesis: for b1 being Element of Args (o,(product A)) holds (F . (the_result_sort_of o)) . ((Den (o,(product A))) . b1) = (Den (o,(product (product (A / EqR))))) . (F # b1) let x be Element of Args (o,(product A)); ::_thesis: (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x) thus (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x) ::_thesis: verum proof A17: (Den (o,(product A))) . x in Result (o,(product A)) ; then A18: (Den (o,(product A))) . x in the Sorts of (product A) . (the_result_sort_of o) by PRALG_2:3; set s = the_result_sort_of o; set U3 = product (A / EqR); A19: the Sorts of (product (product (A / EqR))) . (the_result_sort_of o) = product (Carrier ((product (A / EqR)),(the_result_sort_of o))) by PRALG_2:def_10; A20: ex f being Function of ( the Sorts of (product A) . (the_result_sort_of o)),( the Sorts of (product (product (A / EqR))) . (the_result_sort_of o)) st ( f = F . (the_result_sort_of o) & ( for x9 being set st x9 in the Sorts of (product A) . (the_result_sort_of o) holds S1[f . x9,x9, the_result_sort_of o] ) ) by A15; A21: dom (F . (the_result_sort_of o)) = (SORTS A) . (the_result_sort_of o) by FUNCT_2:def_1 .= product (Carrier (A,(the_result_sort_of o))) by PRALG_2:def_10 ; A22: (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o))) by Th19; percases ( the_arity_of o = {} or the_arity_of o <> {} ) ; supposeA23: the_arity_of o = {} ; ::_thesis: (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x) then Args (o,(product A)) = {{}} by PRALG_2:4; then A24: x = {} by TARSKI:def_1; then A25: (F . (the_result_sort_of o)) . (const (o,(product A))) in rng (F . (the_result_sort_of o)) by A21, A22, FUNCT_1:def_3; reconsider g1 = (F . (the_result_sort_of o)) . (const (o,(product A))) as Function by A19; A26: dom (const (o,(product A))) = dom (Carrier (A,(the_result_sort_of o))) by A22, A24, CARD_3:9 .= I by PARTFUN1:def_2 ; A27: now__::_thesis:_for_e_being_Element_of_Class_EqR_holds_(const_(o,(product_A)))_|_e_=_const_(o,((product_(A_/_EqR))_._e)) let e be Element of Class EqR; ::_thesis: (const (o,(product A))) | e = const (o,((product (A / EqR)) . e)) consider Ji being non empty set , Cs being MSAlgebra-Family of Ji,S such that A28: Ji = (id (Class EqR)) . e and A29: Cs = (A / EqR) . e and A30: (product (A / EqR)) . e = product Cs by Def5; A31: dom ((const (o,(product A))) | e) = I /\ e by A26, RELAT_1:61 .= e by XBOOLE_1:28 ; A32: now__::_thesis:_for_i1_being_set_st_i1_in_e_holds_ ((const_(o,(product_A)))_|_e)_._i1_=_(const_(o,(product_Cs)))_._i1 let i1 be set ; ::_thesis: ( i1 in e implies ((const (o,(product A))) | e) . i1 = (const (o,(product Cs))) . i1 ) A33: dom (A | e) = (dom A) /\ e by RELAT_1:61 .= I /\ e by PARTFUN1:def_2 .= e by XBOOLE_1:28 ; assume A34: i1 in e ; ::_thesis: ((const (o,(product A))) | e) . i1 = (const (o,(product Cs))) . i1 then reconsider ii = i1 as Element of Ji by A28, FUNCT_1:18; reconsider ii9 = ii as Element of I by A34; Cs = A | e by A29, Def4; then A35: Cs . ii = A . ii9 by A34, A33, FUNCT_1:47; thus ((const (o,(product A))) | e) . i1 = (const (o,(product A))) . i1 by A31, A34, FUNCT_1:47 .= const (o,(A . ii9)) by A23, Th9 .= (const (o,(product Cs))) . i1 by A23, A35, Th9 ; ::_thesis: verum end; const (o,(product Cs)) in Funcs (Ji,(union { (Result (o,(Cs . i9))) where i9 is Element of Ji : verum } )) by A23, Th8; then dom (const (o,(product Cs))) = Ji by FUNCT_2:92 .= e by A28, FUNCT_1:18 ; hence (const (o,(product A))) | e = const (o,((product (A / EqR)) . e)) by A30, A31, A32, FUNCT_1:2; ::_thesis: verum end; A36: const (o,(product A)) in the Sorts of (product A) . (the_result_sort_of o) by A17, A24, PRALG_2:3; A37: now__::_thesis:_for_x1_being_set_st_x1_in_Class_EqR_holds_ g1_._x1_=_(const_(o,(product_(product_(A_/_EqR)))))_._x1 let x1 be set ; ::_thesis: ( x1 in Class EqR implies g1 . x1 = (const (o,(product (product (A / EqR))))) . x1 ) consider f1 being Function such that A38: f1 = const (o,(product A)) ; assume x1 in Class EqR ; ::_thesis: g1 . x1 = (const (o,(product (product (A / EqR))))) . x1 then reconsider e = x1 as Element of Class EqR ; g1 . e = f1 | e by A20, A36, A38; hence g1 . x1 = const (o,((product (A / EqR)) . e)) by A27, A38 .= (const (o,(product (product (A / EqR))))) . x1 by A23, Th9 ; ::_thesis: verum end; const (o,(product (product (A / EqR)))) in Funcs ((Class EqR),(union { (Result (o,((product (A / EqR)) . i9))) where i9 is Element of Class EqR : verum } )) by A23, Th8; then A39: dom (const (o,(product (product (A / EqR))))) = Class EqR by FUNCT_2:92; dom g1 = dom (Carrier ((product (A / EqR)),(the_result_sort_of o))) by A19, A25, CARD_3:9 .= Class EqR by PARTFUN1:def_2 ; then (F . (the_result_sort_of o)) . (const (o,(product A))) = const (o,(product (product (A / EqR)))) by A39, A37, FUNCT_1:2; hence (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x) by A23, A24, Th11; ::_thesis: verum end; supposeA40: the_arity_of o <> {} ; ::_thesis: (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x) A41: (Den (o,(product (product (A / EqR))))) . (F # x) in product (Carrier ((product (A / EqR)),(the_result_sort_of o))) by Th19; then reconsider f1 = (Den (o,(product (product (A / EqR))))) . (F # x) as Function ; A42: dom f1 = dom (Carrier ((product (A / EqR)),(the_result_sort_of o))) by A41, CARD_3:9 .= Class EqR by PARTFUN1:def_2 ; A43: (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) in rng (F . (the_result_sort_of o)) by A21, A22, FUNCT_1:def_3; reconsider g1 = (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) as Function by A19; A44: now__::_thesis:_for_e_being_Element_of_Class_EqR for_f2_being_Function_st_f2_=_(Den_(o,(product_A)))_._x_holds_ f2_|_e_=_(Den_(o,((product_(A_/_EqR))_._e)))_._((commute_(F_#_x))_._e) let e be Element of Class EqR; ::_thesis: for f2 being Function st f2 = (Den (o,(product A))) . x holds f2 | e = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e) consider Ji being non empty set , Cs being MSAlgebra-Family of Ji,S such that A45: Ji = (id (Class EqR)) . e and A46: Cs = (A / EqR) . e and A47: (product (A / EqR)) . e = product Cs by Def5; A48: (commute (F # x)) . e is Element of Args (o,((product (A / EqR)) . e)) by A40, Th20; then A49: (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e) in product (Carrier (Cs,(the_result_sort_of o))) by A47, Th19; then reconsider f3 = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e) as Function ; A50: now__::_thesis:_for_i1_being_Element_of_I_st_i1_in_e_holds_ (commute_((commute_(F_#_x))_._e))_._i1_=_(commute_x)_._i1 let i1 be Element of I; ::_thesis: ( i1 in e implies (commute ((commute (F # x)) . e)) . i1 = (commute x) . i1 ) assume A51: i1 in e ; ::_thesis: (commute ((commute (F # x)) . e)) . i1 = (commute x) . i1 then reconsider i2 = i1 as Element of Ji by A45, FUNCT_1:18; A52: now__::_thesis:_for_n_being_set_st_n_in_dom_(the_arity_of_o)_holds_ ((commute_((commute_(F_#_x))_._e))_._i1)_._n_=_((commute_x)_._i1)_._n let n be set ; ::_thesis: ( n in dom (the_arity_of o) implies ((commute ((commute (F # x)) . e)) . i1) . n = ((commute x) . i1) . n ) assume A53: n in dom (the_arity_of o) ; ::_thesis: ((commute ((commute (F # x)) . e)) . i1) . n = ((commute x) . i1) . n then (the_arity_of o) . n in rng (the_arity_of o) by FUNCT_1:def_3; then reconsider s1 = (the_arity_of o) . n as SortSymbol of S ; A54: x . n in product (Carrier (A,((the_arity_of o) /. n))) by A53, Th15; then reconsider f4 = x . n as Function ; A55: x . n in product (Carrier (A,s1)) by A53, A54, PARTFUN1:def_6; then A56: x . n in (SORTS A) . s1 by PRALG_2:def_10; dom f4 = dom (Carrier (A,s1)) by A55, CARD_3:9 .= I by PARTFUN1:def_2 ; then A57: dom (f4 | e) = I /\ e by RELAT_1:61 .= e by XBOOLE_1:28 ; (F # x) . n in product (Carrier ((product (A / EqR)),((the_arity_of o) /. n))) by A53, Th15; then reconsider f5 = (F # x) . n as Function ; consider f7 being Function of ( the Sorts of (product A) . s1),( the Sorts of (product (product (A / EqR))) . s1) such that A58: f7 = F . s1 and A59: for x9 being set st x9 in the Sorts of (product A) . s1 holds S1[f7 . x9,x9,s1] by A15; f5 = (F . ((the_arity_of o) /. n)) . (x . n) by A53, Th13 .= f7 . (x . n) by A53, A58, PARTFUN1:def_6 ; then A60: f5 . e = f4 | e by A56, A59; then reconsider f6 = f5 . e as Function ; f6 = ((commute (F # x)) . e) . n by A53, Th21; hence ((commute ((commute (F # x)) . e)) . i1) . n = (f4 | e) . i2 by A47, A48, A53, A60, Th21 .= f4 . i2 by A51, A57, FUNCT_1:47 .= ((commute x) . i1) . n by A53, Th21 ; ::_thesis: verum end; (commute x) . i1 is Element of Args (o,(A . i1)) by A40, Th20; then (commute x) . i1 in Args (o,(A . i1)) ; then (commute x) . i1 in product ( the Sorts of (A . i1) * (the_arity_of o)) by PRALG_2:3; then A61: dom ((commute x) . i1) = dom ( the Sorts of (A . i1) * (the_arity_of o)) by CARD_3:9 .= dom (the_arity_of o) by PRALG_2:3 ; (commute ((commute (F # x)) . e)) . i2 is Element of Args (o,(Cs . i2)) by A40, A47, A48, Th20; then (commute ((commute (F # x)) . e)) . i2 in Args (o,(Cs . i2)) ; then (commute ((commute (F # x)) . e)) . i2 in product ( the Sorts of (Cs . i2) * (the_arity_of o)) by PRALG_2:3; then dom ((commute ((commute (F # x)) . e)) . i1) = dom ( the Sorts of (Cs . i2) * (the_arity_of o)) by CARD_3:9 .= dom (the_arity_of o) by PRALG_2:3 ; hence (commute ((commute (F # x)) . e)) . i1 = (commute x) . i1 by A61, A52, FUNCT_1:2; ::_thesis: verum end; let f2 be Function; ::_thesis: ( f2 = (Den (o,(product A))) . x implies f2 | e = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e) ) assume A62: f2 = (Den (o,(product A))) . x ; ::_thesis: f2 | e = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e) dom f2 = dom (Carrier (A,(the_result_sort_of o))) by A22, A62, CARD_3:9 .= I by PARTFUN1:def_2 ; then A63: dom (f2 | e) = I /\ e by RELAT_1:61 .= e by XBOOLE_1:28 ; A64: (commute (F # x)) . e is Element of Args (o,(product Cs)) by A40, A47, Th20; A65: now__::_thesis:_for_x1_being_set_st_x1_in_e_holds_ f3_._x1_=_(f2_|_e)_._x1 let x1 be set ; ::_thesis: ( x1 in e implies f3 . x1 = (f2 | e) . x1 ) A66: dom (A | e) = (dom A) /\ e by RELAT_1:61 .= I /\ e by PARTFUN1:def_2 .= e by XBOOLE_1:28 ; assume A67: x1 in e ; ::_thesis: f3 . x1 = (f2 | e) . x1 then reconsider i2 = x1 as Element of Ji by A45, FUNCT_1:18; reconsider i1 = i2 as Element of I by A67; Cs = A | e by A46, Def4; then Cs . i2 = A . i1 by A67, A66, FUNCT_1:47; hence f3 . x1 = (Den (o,(A . i1))) . ((commute ((commute (F # x)) . e)) . i2) by A40, A47, A64, Th22 .= (Den (o,(A . i1))) . ((commute x) . i1) by A50, A67 .= f2 . x1 by A40, A62, Th22 .= (f2 | e) . x1 by A63, A67, FUNCT_1:47 ; ::_thesis: verum end; dom f3 = dom (Carrier (Cs,(the_result_sort_of o))) by A49, CARD_3:9 .= Ji by PARTFUN1:def_2 .= e by A45, FUNCT_1:18 ; hence f2 | e = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e) by A63, A65, FUNCT_1:2; ::_thesis: verum end; A68: now__::_thesis:_for_x1_being_set_st_x1_in_Class_EqR_holds_ g1_._x1_=_f1_._x1 reconsider f2 = (Den (o,(product A))) . x as Function by A22; let x1 be set ; ::_thesis: ( x1 in Class EqR implies g1 . x1 = f1 . x1 ) assume x1 in Class EqR ; ::_thesis: g1 . x1 = f1 . x1 then reconsider e = x1 as Element of Class EqR ; g1 . e = f2 | e by A20, A18; hence g1 . x1 = (Den (o,((product (A / EqR)) . e))) . ((commute (F # x)) . e) by A44 .= f1 . x1 by A40, Th22 ; ::_thesis: verum end; dom g1 = dom (Carrier ((product (A / EqR)),(the_result_sort_of o))) by A19, A43, CARD_3:9 .= Class EqR by PARTFUN1:def_2 ; hence (F . (the_result_sort_of o)) . ((Den (o,(product A))) . x) = (Den (o,(product (product (A / EqR))))) . (F # x) by A42, A68, FUNCT_1:2; ::_thesis: verum end; end; end; end; F is "1-1" proof let s be set ; :: according to MSUALG_3:def_2 ::_thesis: for b1 being set holds ( not s in dom F or not F . s = b1 or b1 is one-to-one ) let g be Function; ::_thesis: ( not s in dom F or not F . s = g or g is one-to-one ) assume that A69: s in dom F and A70: F . s = g ; ::_thesis: g is one-to-one consider f being Function of ( the Sorts of (product A) . s),( the Sorts of (product (product (A / EqR))) . s) such that A71: f = F . s and A72: for x being set st x in the Sorts of (product A) . s holds S1[f . x,x,s] by A15, A69; let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom g or not x2 in dom g or not g . x1 = g . x2 or x1 = x2 ) assume that A73: x1 in dom g and A74: x2 in dom g and A75: g . x1 = g . x2 ; ::_thesis: x1 = x2 A76: dom f = dom g by A70, A71; thus x1 = x2 ::_thesis: verum proof reconsider s9 = s as SortSymbol of S by A69; A77: the Sorts of (product A) . s9 = product (Carrier (A,s9)) by PRALG_2:def_10; then A78: ex gg being Function st ( x1 = gg & dom gg = dom (Carrier (A,s9)) & ( for x9 being set st x9 in dom (Carrier (A,s9)) holds gg . x9 in (Carrier (A,s9)) . x9 ) ) by A73, A76, CARD_3:def_5; A79: ex gg1 being Function st ( x2 = gg1 & dom gg1 = dom (Carrier (A,s9)) & ( for x9 being set st x9 in dom (Carrier (A,s9)) holds gg1 . x9 in (Carrier (A,s9)) . x9 ) ) by A74, A76, A77, CARD_3:def_5; reconsider x2 = x2 as Function by A74, A76, A77; A80: dom x2 = I by A79, PARTFUN1:def_2; reconsider x1 = x1 as Function by A73, A76, A77; A81: the Sorts of (product (product (A / EqR))) . s = product (Carrier ((product (A / EqR)),s9)) by PRALG_2:def_10; A82: for i being set st i in I holds x1 . i = x2 . i proof reconsider f99 = f . x2 as Function by A81; let i be set ; ::_thesis: ( i in I implies x1 . i = x2 . i ) assume A83: i in I ; ::_thesis: x1 . i = x2 . i then A84: Class (EqR,i) is Element of Class EqR by EQREL_1:def_3; then x1 | (Class (EqR,i)) = f99 . (Class (EqR,i)) by A70, A73, A75, A71, A72, A76 .= x2 | (Class (EqR,i)) by A74, A72, A76, A84 ; then x1 . i = (x2 | (Class (EqR,i))) . i by A83, EQREL_1:20, FUNCT_1:49 .= x2 . i by A83, EQREL_1:20, FUNCT_1:49 ; hence x1 . i = x2 . i ; ::_thesis: verum end; dom x1 = I by A78, PARTFUN1:def_2; hence x1 = x2 by A80, A82, FUNCT_1:2; ::_thesis: verum end; end; then A85: F is_monomorphism product A, product (product (A / EqR)) by A16, MSUALG_3:def_9; F is "onto" proof let s be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not s in the carrier of S or rng (F . s) = the Sorts of (product (product (A / EqR))) . s ) assume A86: s in the carrier of S ; ::_thesis: rng (F . s) = the Sorts of (product (product (A / EqR))) . s reconsider s9 = s as SortSymbol of S by A86; consider f being Function of ( the Sorts of (product A) . s),( the Sorts of (product (product (A / EqR))) . s) such that A87: f = F . s and A88: for x being set st x in the Sorts of (product A) . s holds S1[f . x,x,s] by A15, A86; A89: the Sorts of (product A) . s9 = product (Carrier (A,s9)) by PRALG_2:def_10; for y being set holds ( y in the Sorts of (product (product (A / EqR))) . s iff ex x being set st ( x in dom f & y = f . x ) ) proof let y be set ; ::_thesis: ( y in the Sorts of (product (product (A / EqR))) . s iff ex x being set st ( x in dom f & y = f . x ) ) A90: ( y in the Sorts of (product (product (A / EqR))) . s implies ex x being set st ( x in dom f & y = f . x ) ) proof assume y in the Sorts of (product (product (A / EqR))) . s ; ::_thesis: ex x being set st ( x in dom f & y = f . x ) then A91: y in product (Carrier ((product (A / EqR)),s9)) by PRALG_2:def_10; then A92: ex gg being Function st ( y = gg & dom gg = dom (Carrier ((product (A / EqR)),s9)) & ( for x9 being set st x9 in dom (Carrier ((product (A / EqR)),s9)) holds gg . x9 in (Carrier ((product (A / EqR)),s9)) . x9 ) ) by CARD_3:def_5; reconsider y = y as Function by A91; defpred S2[ set , set ] means ex e being Element of Class EqR ex f being Function st ( \$1 in e & f = y . e & \$2 = f . \$1 ); A93: for i being set st i in I holds ex j being set st S2[i,j] proof let i be set ; ::_thesis: ( i in I implies ex j being set st S2[i,j] ) assume A94: i in I ; ::_thesis: ex j being set st S2[i,j] Class (EqR,i) in Class EqR by A94, EQREL_1:def_3; then consider e being Element of Class EqR such that A95: e = Class (EqR,i) ; consider Ji being non empty set , Cs being MSAlgebra-Family of Ji,S such that Ji = (id (Class EqR)) . e and Cs = (A / EqR) . e and A96: (product (A / EqR)) . e = product Cs by Def5; ex U0 being MSAlgebra over S st ( U0 = (product (A / EqR)) . e & (Carrier ((product (A / EqR)),s9)) . e = the Sorts of U0 . s9 ) by PRALG_2:def_9; then ( dom (Carrier ((product (A / EqR)),s9)) = Class EqR & (Carrier ((product (A / EqR)),s9)) . e = product (Carrier (Cs,s9)) ) by A96, PARTFUN1:def_2, PRALG_2:def_10; then reconsider y9 = y . e as Function by A92, Lm1; S2[i,y9 . i] by A94, A95, EQREL_1:20; hence ex j being set st S2[i,j] ; ::_thesis: verum end; consider x being ManySortedSet of I such that A97: for i being set st i in I holds S2[i,x . i] from PBOOLE:sch_3(A93); A98: dom (Carrier ((product (A / EqR)),s9)) = Class EqR by PARTFUN1:def_2; A99: for z being set st z in dom (Carrier (A,s9)) holds x . z in (Carrier (A,s9)) . z proof let z be set ; ::_thesis: ( z in dom (Carrier (A,s9)) implies x . z in (Carrier (A,s9)) . z ) assume z in dom (Carrier (A,s9)) ; ::_thesis: x . z in (Carrier (A,s9)) . z then z in I ; then consider e being Element of Class EqR, f1 being Function such that A100: z in e and A101: ( f1 = y . e & x . z = f1 . z ) by A97; dom ((Carrier (A,s9)) | e) = (dom (Carrier (A,s9))) /\ e by RELAT_1:61 .= I /\ e by PARTFUN1:def_2 .= e by XBOOLE_1:28 ; then A102: ((Carrier (A,s9)) | e) . z = (Carrier (A,s9)) . z by A100, FUNCT_1:47; consider Ji being non empty set , Cs being MSAlgebra-Family of Ji,S such that A103: Ji = (id (Class EqR)) . e and A104: Cs = (A / EqR) . e and A105: (product (A / EqR)) . e = product Cs by Def5; ( Cs = A | e & Ji = e ) by A103, A104, Def4, FUNCT_1:18; then A106: Carrier (Cs,s9) = (Carrier (A,s9)) | e by Th2; ex U0 being MSAlgebra over S st ( U0 = (product (A / EqR)) . e & (Carrier ((product (A / EqR)),s9)) . e = the Sorts of U0 . s9 ) by PRALG_2:def_9; then A107: (Carrier ((product (A / EqR)),s9)) . e = product (Carrier (Cs,s9)) by A105, PRALG_2:def_10; y . e in (Carrier ((product (A / EqR)),s9)) . e by A92, A98; then A108: ex g being Function st ( y . e = g & dom g = dom (Carrier (Cs,s9)) & ( for x9 being set st x9 in dom (Carrier (Cs,s9)) holds g . x9 in (Carrier (Cs,s9)) . x9 ) ) by A107, CARD_3:def_5; dom (Carrier (Cs,s9)) = Ji by PARTFUN1:def_2 .= e by A103, FUNCT_1:18 ; hence x . z in (Carrier (A,s9)) . z by A100, A101, A108, A102, A106; ::_thesis: verum end; dom x = I by PARTFUN1:def_2 .= dom (Carrier (A,s9)) by PARTFUN1:def_2 ; then A109: x in the Sorts of (product A) . s9 by A89, A99, CARD_3:9; then A110: x in dom f by FUNCT_2:def_1; then f . x in rng f by FUNCT_1:def_3; then f . x in the Sorts of (product (product (A / EqR))) . s ; then A111: f . x in product (Carrier ((product (A / EqR)),s9)) by PRALG_2:def_10; then reconsider f9 = f . x as Function ; A112: for e being set st e in Class EqR holds y . e = f9 . e proof let e be set ; ::_thesis: ( e in Class EqR implies y . e = f9 . e ) assume e in Class EqR ; ::_thesis: y . e = f9 . e then reconsider e = e as Element of Class EqR ; consider Ji being non empty set , Cs being MSAlgebra-Family of Ji,S such that A113: Ji = (id (Class EqR)) . e and Cs = (A / EqR) . e and A114: (product (A / EqR)) . e = product Cs by Def5; ex U0 being MSAlgebra over S st ( U0 = (product (A / EqR)) . e & (Carrier ((product (A / EqR)),s9)) . e = the Sorts of U0 . s9 ) by PRALG_2:def_9; then A115: (Carrier ((product (A / EqR)),s9)) . e = product (Carrier (Cs,s9)) by A114, PRALG_2:def_10; A116: y . e in (Carrier ((product (A / EqR)),s9)) . e by A92, A98; then reconsider y9 = y . e as Function by A115; A117: dom (x | e) = (dom x) /\ e by RELAT_1:61 .= I /\ e by PARTFUN1:def_2 .= e by XBOOLE_1:28 ; A118: for i being set st i in e holds (x | e) . i = y9 . i proof let i be set ; ::_thesis: ( i in e implies (x | e) . i = y9 . i ) assume A119: i in e ; ::_thesis: (x | e) . i = y9 . i then consider e1 being Element of Class EqR, f1 being Function such that A120: i in e1 and A121: ( f1 = y . e1 & x . i = f1 . i ) by A97; e = e1 by A119, A120, Th3; hence (x | e) . i = y9 . i by A117, A119, A121, FUNCT_1:47; ::_thesis: verum end; ex g being Function st ( y . e = g & dom g = dom (Carrier (Cs,s9)) & ( for x9 being set st x9 in dom (Carrier (Cs,s9)) holds g . x9 in (Carrier (Cs,s9)) . x9 ) ) by A116, A115, CARD_3:def_5; then dom y9 = Ji by PARTFUN1:def_2 .= e by A113, FUNCT_1:18 ; then x | e = y9 by A117, A118, FUNCT_1:def_11; hence y . e = f9 . e by A88, A109; ::_thesis: verum end; ex gg9 being Function st ( f . x = gg9 & dom gg9 = dom (Carrier ((product (A / EqR)),s9)) & ( for x9 being set st x9 in dom (Carrier ((product (A / EqR)),s9)) holds gg9 . x9 in (Carrier ((product (A / EqR)),s9)) . x9 ) ) by A111, CARD_3:def_5; then y = f9 by A92, A98, A112, FUNCT_1:def_11; hence ex x being set st ( x in dom f & y = f . x ) by A110; ::_thesis: verum end; ( ex x being set st ( x in dom f & y = f . x ) implies y in the Sorts of (product (product (A / EqR))) . s ) proof given x being set such that A122: x in dom f and A123: y = f . x ; ::_thesis: y in the Sorts of (product (product (A / EqR))) . s f . x in rng f by A122, FUNCT_1:def_3; hence y in the Sorts of (product (product (A / EqR))) . s by A123; ::_thesis: verum end; hence ( y in the Sorts of (product (product (A / EqR))) . s iff ex x being set st ( x in dom f & y = f . x ) ) by A90; ::_thesis: verum end; hence rng (F . s) = the Sorts of (product (product (A / EqR))) . s by A87, FUNCT_1:def_3; ::_thesis: verum end; then F is_epimorphism product A, product (product (A / EqR)) by A16, MSUALG_3:def_8; then F is_isomorphism product A, product (product (A / EqR)) by A85, MSUALG_3:def_10; hence product A, product (product (A / EqR)) are_isomorphic by MSUALG_3:def_11; ::_thesis: verum end;