:: PRALG_2 semantic presentation begin registration let X be functional non empty with_common_domain set ; cluster -> DOM X -defined for Element of X; coherence for b1 being Element of X holds b1 is DOM X -defined proof let x be Element of X; ::_thesis: x is DOM X -defined DOM X = dom x by CARD_3:108; hence x is DOM X -defined by RELAT_1:def_18; ::_thesis: verum end; end; registration let X be functional non empty with_common_domain set ; cluster -> total for Element of X; coherence for b1 being Element of X holds b1 is total proof let x be Element of X; ::_thesis: x is total DOM X = dom x by CARD_3:108; hence x is total by PARTFUN1:def_2; ::_thesis: verum end; end; begin definition let F be Function; func Commute F -> Function means :Def1: :: PRALG_2:def 1 ( ( for x being set holds ( x in dom it iff ex f being Function st ( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom it holds it . f = F . (commute f) ) ); existence ex b1 being Function st ( ( for x being set holds ( x in dom b1 iff ex f being Function st ( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b1 holds b1 . f = F . (commute f) ) ) proof defpred S1[ set , set ] means ex f being Function st ( $1 = f & $2 = commute f ); A1: for x, y1, y2 being set st S1[x,y1] & S1[x,y2] holds y1 = y2 ; consider X being set such that A2: for x being set holds ( x in X iff ex y being set st ( y in dom F & S1[y,x] ) ) from TARSKI:sch_1(A1); defpred S2[ set , set ] means for f being Function st $1 = f holds $2 = F . (commute f); A3: now__::_thesis:_for_x_being_set_st_x_in_X_holds_ ex_y_being_set_st_S2[x,y] let x be set ; ::_thesis: ( x in X implies ex y being set st S2[x,y] ) assume x in X ; ::_thesis: ex y being set st S2[x,y] then ex y being set st ( y in dom F & ex f being Function st ( y = f & x = commute f ) ) by A2; then reconsider f = x as Function ; take y = F . (commute f); ::_thesis: S2[x,y] thus S2[x,y] ; ::_thesis: verum end; consider G being Function such that A4: dom G = X and A5: for x being set st x in X holds S2[x,G . x] from CLASSES1:sch_1(A3); take G ; ::_thesis: ( ( for x being set holds ( x in dom G iff ex f being Function st ( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom G holds G . f = F . (commute f) ) ) hereby ::_thesis: for f being Function st f in dom G holds G . f = F . (commute f) let x be set ; ::_thesis: ( ( x in dom G implies ex f being Function st ( f in dom F & x = commute f ) ) & ( ex f being Function st ( f in dom F & x = commute f ) implies x in dom G ) ) hereby ::_thesis: ( ex f being Function st ( f in dom F & x = commute f ) implies x in dom G ) assume x in dom G ; ::_thesis: ex f being Function st ( f in dom F & x = commute f ) then consider y being set such that A6: y in dom F and A7: ex f being Function st ( y = f & x = commute f ) by A2, A4; reconsider f = y as Function by A7; take f = f; ::_thesis: ( f in dom F & x = commute f ) thus ( f in dom F & x = commute f ) by A6, A7; ::_thesis: verum end; thus ( ex f being Function st ( f in dom F & x = commute f ) implies x in dom G ) by A2, A4; ::_thesis: verum end; thus for f being Function st f in dom G holds G . f = F . (commute f) by A4, A5; ::_thesis: verum end; uniqueness for b1, b2 being Function st ( for x being set holds ( x in dom b1 iff ex f being Function st ( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b1 holds b1 . f = F . (commute f) ) & ( for x being set holds ( x in dom b2 iff ex f being Function st ( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b2 holds b2 . f = F . (commute f) ) holds b1 = b2 proof let m, n be Function; ::_thesis: ( ( for x being set holds ( x in dom m iff ex f being Function st ( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom m holds m . f = F . (commute f) ) & ( for x being set holds ( x in dom n iff ex f being Function st ( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom n holds n . f = F . (commute f) ) implies m = n ) assume that A8: for x being set holds ( x in dom m iff ex f being Function st ( f in dom F & x = commute f ) ) and A9: for f being Function st f in dom m holds m . f = F . (commute f) and A10: for x being set holds ( x in dom n iff ex f being Function st ( f in dom F & x = commute f ) ) and A11: for f being Function st f in dom n holds n . f = F . (commute f) ; ::_thesis: m = n now__::_thesis:_for_x_being_set_holds_ (_x_in_dom_m_iff_x_in_dom_n_) let x be set ; ::_thesis: ( x in dom m iff x in dom n ) ( x in dom m iff ex f being Function st ( f in dom F & x = commute f ) ) by A8; hence ( x in dom m iff x in dom n ) by A10; ::_thesis: verum end; then A12: dom m = dom n by TARSKI:1; now__::_thesis:_for_x_being_set_st_x_in_dom_m_holds_ m_._x_=_n_._x let x be set ; ::_thesis: ( x in dom m implies m . x = n . x ) assume A13: x in dom m ; ::_thesis: m . x = n . x then consider g being Function such that g in dom F and A14: x = commute g by A10, A12; thus m . x = F . (commute (commute g)) by A9, A13, A14 .= n . x by A11, A12, A13, A14 ; ::_thesis: verum end; hence m = n by A12, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def1 defines Commute PRALG_2:def_1_:_ for F, b2 being Function holds ( b2 = Commute F iff ( ( for x being set holds ( x in dom b2 iff ex f being Function st ( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b2 holds b2 . f = F . (commute f) ) ) ); theorem :: PRALG_2:1 for F being Function st dom F = {{}} holds Commute F = F proof let F be Function; ::_thesis: ( dom F = {{}} implies Commute F = F ) assume A1: dom F = {{}} ; ::_thesis: Commute F = F A2: dom (Commute F) = {{}} proof thus dom (Commute F) c= {{}} :: according to XBOOLE_0:def_10 ::_thesis: {{}} c= dom (Commute F) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (Commute F) or x in {{}} ) assume x in dom (Commute F) ; ::_thesis: x in {{}} then ex f being Function st ( f in dom F & x = commute f ) by Def1; then x = {} by A1, FUNCT_6:58, TARSKI:def_1; hence x in {{}} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in dom (Commute F) ) assume x in {{}} ; ::_thesis: x in dom (Commute F) then A3: x = {} by TARSKI:def_1; {} in dom F by A1, TARSKI:def_1; hence x in dom (Commute F) by A3, Def1, FUNCT_6:58; ::_thesis: verum end; for x being set st x in {{}} holds (Commute F) . x = F . x proof let x be set ; ::_thesis: ( x in {{}} implies (Commute F) . x = F . x ) assume A4: x in {{}} ; ::_thesis: (Commute F) . x = F . x then x = {} by TARSKI:def_1; hence (Commute F) . x = F . x by A2, A4, Def1, FUNCT_6:58; ::_thesis: verum end; hence Commute F = F by A1, A2, FUNCT_1:2; ::_thesis: verum end; definition let f be Function-yielding Function; :: original: Frege redefine func Frege f -> ManySortedFunction of product (doms f) means :Def2: :: PRALG_2:def 2 for g being Function st g in product (doms f) holds it . g = f .. g; coherence Frege f is ManySortedFunction of product (doms f) proof A1: dom (Frege f) = product (doms f) by FUNCT_6:def_7; Frege f is Function-yielding proof let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not x in dom (Frege f) or (Frege f) . x is set ) assume A2: x in dom (Frege f) ; ::_thesis: (Frege f) . x is set then reconsider g = x as Function by A1; ex h being Function st ( (Frege f) . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) ) ) by A1, A2, FUNCT_6:def_7; hence (Frege f) . x is set ; ::_thesis: verum end; hence Frege f is ManySortedFunction of product (doms f) by A1, PARTFUN1:def_2, RELAT_1:def_18; ::_thesis: verum end; compatibility for b1 being ManySortedFunction of product (doms f) holds ( b1 = Frege f iff for g being Function st g in product (doms f) holds b1 . g = f .. g ) proof let F be ManySortedFunction of product (doms f); ::_thesis: ( F = Frege f iff for g being Function st g in product (doms f) holds F . g = f .. g ) for x being set holds ( x in rng f iff ( x in rng f & x is Function ) ) proof let y be set ; ::_thesis: ( y in rng f iff ( y in rng f & y is Function ) ) ( y in rng f implies y is Function ) proof assume y in rng f ; ::_thesis: y is Function then ex x being set st ( x in dom f & y = f . x ) by FUNCT_1:def_3; hence y is Function ; ::_thesis: verum end; hence ( y in rng f iff ( y in rng f & y is Function ) ) ; ::_thesis: verum end; then A3: SubFuncs (rng f) = rng f by FUNCT_6:def_1; thus ( F = Frege f implies for g being Function st g in product (doms f) holds F . g = f .. g ) ::_thesis: ( ( for g being Function st g in product (doms f) holds F . g = f .. g ) implies F = Frege f ) proof assume A4: F = Frege f ; ::_thesis: for g being Function st g in product (doms f) holds F . g = f .. g let g be Function; ::_thesis: ( g in product (doms f) implies F . g = f .. g ) assume A5: g in product (doms f) ; ::_thesis: F . g = f .. g then consider h being Function such that A6: F . g = h and A7: dom h = f " (SubFuncs (rng f)) and A8: for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) by A4, FUNCT_6:def_7; A9: dom h = dom f by A3, A7, RELAT_1:134; for x being set st x in dom f holds h . x = (f . x) . (g . x) proof let x be set ; ::_thesis: ( x in dom f implies h . x = (f . x) . (g . x) ) assume A10: x in dom f ; ::_thesis: h . x = (f . x) . (g . x) then x in dom (doms f) by A7, A9, FUNCT_6:def_2; then g . x in (doms f) . x by A5, CARD_3:9; then A11: g . x in dom (f . x) by A10, FUNCT_6:22; thus h . x = f .. (x,(g . x)) by A8, A9, A10 .= (f . x) . (g . x) by A10, A11, FUNCT_5:38 ; ::_thesis: verum end; hence F . g = f .. g by A6, A9, PRALG_1:def_17; ::_thesis: verum end; assume A12: for g being Function st g in product (doms f) holds F . g = f .. g ; ::_thesis: F = Frege f A13: for g being Function st g in product (doms f) holds ex h being Function st ( F . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) ) ) proof let g be Function; ::_thesis: ( g in product (doms f) implies ex h being Function st ( F . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) ) ) ) assume A14: g in product (doms f) ; ::_thesis: ex h being Function st ( F . g = h & dom h = f " (SubFuncs (rng f)) & ( for x being set st x in dom h holds h . x = (uncurry f) . (x,(g . x)) ) ) F . g = f .. g by A12, A14; then A15: dom (F . g) = dom f by PRALG_1:def_17; take F . g ; ::_thesis: ( F . g = F . g & dom (F . g) = f " (SubFuncs (rng f)) & ( for x being set st x in dom (F . g) holds (F . g) . x = (uncurry f) . (x,(g . x)) ) ) thus F . g = F . g ; ::_thesis: ( dom (F . g) = f " (SubFuncs (rng f)) & ( for x being set st x in dom (F . g) holds (F . g) . x = (uncurry f) . (x,(g . x)) ) ) thus A16: dom (F . g) = f " (SubFuncs (rng f)) by A3, A15, RELAT_1:134; ::_thesis: for x being set st x in dom (F . g) holds (F . g) . x = (uncurry f) . (x,(g . x)) let x be set ; ::_thesis: ( x in dom (F . g) implies (F . g) . x = (uncurry f) . (x,(g . x)) ) assume A17: x in dom (F . g) ; ::_thesis: (F . g) . x = (uncurry f) . (x,(g . x)) then x in dom (doms f) by A16, FUNCT_6:def_2; then g . x in (doms f) . x by A14, CARD_3:9; then A18: g . x in dom (f . x) by A15, A17, FUNCT_6:22; thus (F . g) . x = (f .. g) . x by A12, A14 .= (f . x) . (g . x) by A15, A17, PRALG_1:def_17 .= (uncurry f) . (x,(g . x)) by A15, A17, A18, FUNCT_5:38 ; ::_thesis: verum end; dom F = product (doms f) by PARTFUN1:def_2; hence F = Frege f by A13, FUNCT_6:def_7; ::_thesis: verum end; end; :: deftheorem Def2 defines Frege PRALG_2:def_2_:_ for f being Function-yielding Function for b2 being ManySortedFunction of product (doms f) holds ( b2 = Frege f iff for g being Function st g in product (doms f) holds b2 . g = f .. g ); registration let I be set ; let A, B be V2() ManySortedSet of I; cluster[|A,B|] -> V2() ; coherence [|A,B|] is non-empty proof now__::_thesis:_for_i_being_set_st_i_in_I_holds_ not_[|A,B|]_._i_is_empty let i be set ; ::_thesis: ( i in I implies not [|A,B|] . i is empty ) assume A1: i in I ; ::_thesis: not [|A,B|] . i is empty then [|A,B|] . i = [:(A . i),(B . i):] by PBOOLE:def_16; hence not [|A,B|] . i is empty by A1, ZFMISC_1:90; ::_thesis: verum end; hence [|A,B|] is non-empty by PBOOLE:def_13; ::_thesis: verum end; end; theorem :: PRALG_2:2 for I being non empty set for J being set for A, B being ManySortedSet of I for f being Function of J,I holds [|A,B|] * f = [|(A * f),(B * f)|] proof let I be non empty set ; ::_thesis: for J being set for A, B being ManySortedSet of I for f being Function of J,I holds [|A,B|] * f = [|(A * f),(B * f)|] let J be set ; ::_thesis: for A, B being ManySortedSet of I for f being Function of J,I holds [|A,B|] * f = [|(A * f),(B * f)|] let A, B be ManySortedSet of I; ::_thesis: for f being Function of J,I holds [|A,B|] * f = [|(A * f),(B * f)|] let f be Function of J,I; ::_thesis: [|A,B|] * f = [|(A * f),(B * f)|] for i being set st i in J holds ([|A,B|] * f) . i = [|(A * f),(B * f)|] . i proof A1: dom (B * f) = J by PARTFUN1:def_2; let i be set ; ::_thesis: ( i in J implies ([|A,B|] * f) . i = [|(A * f),(B * f)|] . i ) A2: dom (A * f) = J by PARTFUN1:def_2; assume A3: i in J ; ::_thesis: ([|A,B|] * f) . i = [|(A * f),(B * f)|] . i then A4: f . i in I by FUNCT_2:5; dom ([|A,B|] * f) = J by PARTFUN1:def_2; hence ([|A,B|] * f) . i = [|A,B|] . (f . i) by A3, FUNCT_1:12 .= [:(A . (f . i)),(B . (f . i)):] by A4, PBOOLE:def_16 .= [:((A * f) . i),(B . (f . i)):] by A3, A2, FUNCT_1:12 .= [:((A * f) . i),((B * f) . i):] by A3, A1, FUNCT_1:12 .= [|(A * f),(B * f)|] . i by A3, PBOOLE:def_16 ; ::_thesis: verum end; hence [|A,B|] * f = [|(A * f),(B * f)|] by PBOOLE:3; ::_thesis: verum end; definition let I be non empty set ; let A, B be V2() ManySortedSet of I; let pj be Element of I * ; let rj be Element of I; let f be Function of ((A #) . pj),(A . rj); let g be Function of ((B #) . pj),(B . rj); func[[:f,g:]] -> Function of (([|A,B|] #) . pj),([|A,B|] . rj) means :: PRALG_2:def 3 for h being Function st h in ([|A,B|] #) . pj holds it . h = [(f . (pr1 h)),(g . (pr2 h))]; existence ex b1 being Function of (([|A,B|] #) . pj),([|A,B|] . rj) st for h being Function st h in ([|A,B|] #) . pj holds b1 . h = [(f . (pr1 h)),(g . (pr2 h))] proof defpred S1[ set , set ] means for h being Function st h = $1 holds $2 = [(f . (pr1 h)),(g . (pr2 h))]; set Y = [|A,B|] . rj; set X = ([|A,B|] #) . pj; A1: ([|A,B|] #) . pj = product ([|A,B|] * pj) by FINSEQ_2:def_5; A2: for x being set st x in ([|A,B|] #) . pj holds ex y being set st ( y in [|A,B|] . rj & S1[x,y] ) proof let x be set ; ::_thesis: ( x in ([|A,B|] #) . pj implies ex y being set st ( y in [|A,B|] . rj & S1[x,y] ) ) A3: rng pj c= I by FINSEQ_1:def_4; assume x in ([|A,B|] #) . pj ; ::_thesis: ex y being set st ( y in [|A,B|] . rj & S1[x,y] ) then consider h1 being Function such that A4: h1 = x and A5: dom h1 = dom ([|A,B|] * pj) and A6: for z being set st z in dom ([|A,B|] * pj) holds h1 . z in ([|A,B|] * pj) . z by A1, CARD_3:def_5; A7: dom [|A,B|] = I by PARTFUN1:def_2; then A8: dom h1 = dom pj by A5, A3, RELAT_1:27; then A9: dom (pr1 h1) = dom pj by MCART_1:def_12; dom A = I by PARTFUN1:def_2; then A10: dom (pr1 h1) = dom (A * pj) by A3, A9, RELAT_1:27; for z being set st z in dom (A * pj) holds (pr1 h1) . z in (A * pj) . z proof let z be set ; ::_thesis: ( z in dom (A * pj) implies (pr1 h1) . z in (A * pj) . z ) assume A11: z in dom (A * pj) ; ::_thesis: (pr1 h1) . z in (A * pj) . z dom ([|A,B|] * pj) = dom pj by A7, A3, RELAT_1:27; then A12: ([|A,B|] * pj) . z = [|A,B|] . (pj . z) by A9, A10, A11, FUNCT_1:12; ( h1 . z in ([|A,B|] * pj) . z & pj . z in rng pj ) by A5, A6, A8, A9, A10, A11, FUNCT_1:def_3; then h1 . z in [:(A . (pj . z)),(B . (pj . z)):] by A3, A12, PBOOLE:def_16; then consider a, b being set such that A13: a in A . (pj . z) and b in B . (pj . z) and A14: h1 . z = [a,b] by ZFMISC_1:def_2; X: [a,b] `1 = a ; (pr1 h1) . z = (h1 . z) `1 by A8, A9, A10, A11, MCART_1:def_12 .= a by A14, X ; hence (pr1 h1) . z in (A * pj) . z by A11, A13, FUNCT_1:12; ::_thesis: verum end; then pr1 h1 in product (A * pj) by A10, CARD_3:9; then pr1 h1 in (A #) . pj by FINSEQ_2:def_5; then pr1 h1 in dom f by FUNCT_2:def_1; then A15: f . (pr1 h1) in rng f by FUNCT_1:3; take y = [(f . (pr1 h1)),(g . (pr2 h1))]; ::_thesis: ( y in [|A,B|] . rj & S1[x,y] ) ( rng f c= A . rj & rng g c= B . rj ) by RELAT_1:def_19; then A16: [:(rng f),(rng g):] c= [:(A . rj),(B . rj):] by ZFMISC_1:96; A17: dom (pr2 h1) = dom pj by A8, MCART_1:def_13; A18: dom B = I by PARTFUN1:def_2; then A19: dom (pr2 h1) = dom (B * pj) by A3, A17, RELAT_1:27; A20: for z being set st z in dom (B * pj) holds (pr2 h1) . z in (B * pj) . z proof let z be set ; ::_thesis: ( z in dom (B * pj) implies (pr2 h1) . z in (B * pj) . z ) assume A21: z in dom (B * pj) ; ::_thesis: (pr2 h1) . z in (B * pj) . z dom ([|A,B|] * pj) = dom pj by A7, A3, RELAT_1:27; then A22: ([|A,B|] * pj) . z = [|A,B|] . (pj . z) by A17, A19, A21, FUNCT_1:12; ( h1 . z in ([|A,B|] * pj) . z & pj . z in rng pj ) by A5, A6, A8, A17, A19, A21, FUNCT_1:def_3; then h1 . z in [:(A . (pj . z)),(B . (pj . z)):] by A3, A22, PBOOLE:def_16; then consider a, b being set such that a in A . (pj . z) and A23: b in B . (pj . z) and A24: h1 . z = [a,b] by ZFMISC_1:def_2; X: [a,b] `2 = b ; (pr2 h1) . z = (h1 . z) `2 by A8, A17, A19, A21, MCART_1:def_13 .= b by A24, X ; hence (pr2 h1) . z in (B * pj) . z by A21, A23, FUNCT_1:12; ::_thesis: verum end; dom (pr2 h1) = dom pj by A8, MCART_1:def_13; then dom (pr2 h1) = dom (B * pj) by A18, A3, RELAT_1:27; then pr2 h1 in product (B * pj) by A20, CARD_3:9; then pr2 h1 in (B #) . pj by FINSEQ_2:def_5; then pr2 h1 in dom g by FUNCT_2:def_1; then g . (pr2 h1) in rng g by FUNCT_1:3; then [(f . (pr1 h1)),(g . (pr2 h1))] in [:(rng f),(rng g):] by A15, ZFMISC_1:87; then [(f . (pr1 h1)),(g . (pr2 h1))] in [:(A . rj),(B . rj):] by A16; hence y in [|A,B|] . rj by PBOOLE:def_16; ::_thesis: S1[x,y] let h be Function; ::_thesis: ( h = x implies y = [(f . (pr1 h)),(g . (pr2 h))] ) assume x = h ; ::_thesis: y = [(f . (pr1 h)),(g . (pr2 h))] hence y = [(f . (pr1 h)),(g . (pr2 h))] by A4; ::_thesis: verum end; consider F being Function of (([|A,B|] #) . pj),([|A,B|] . rj) such that A25: for x being set st x in ([|A,B|] #) . pj holds S1[x,F . x] from FUNCT_2:sch_1(A2); take F ; ::_thesis: for h being Function st h in ([|A,B|] #) . pj holds F . h = [(f . (pr1 h)),(g . (pr2 h))] thus for h being Function st h in ([|A,B|] #) . pj holds F . h = [(f . (pr1 h)),(g . (pr2 h))] by A25; ::_thesis: verum end; uniqueness for b1, b2 being Function of (([|A,B|] #) . pj),([|A,B|] . rj) st ( for h being Function st h in ([|A,B|] #) . pj holds b1 . h = [(f . (pr1 h)),(g . (pr2 h))] ) & ( for h being Function st h in ([|A,B|] #) . pj holds b2 . h = [(f . (pr1 h)),(g . (pr2 h))] ) holds b1 = b2 proof let x, y be Function of (([|A,B|] #) . pj),([|A,B|] . rj); ::_thesis: ( ( for h being Function st h in ([|A,B|] #) . pj holds x . h = [(f . (pr1 h)),(g . (pr2 h))] ) & ( for h being Function st h in ([|A,B|] #) . pj holds y . h = [(f . (pr1 h)),(g . (pr2 h))] ) implies x = y ) assume that A26: for h being Function st h in ([|A,B|] #) . pj holds x . h = [(f . (pr1 h)),(g . (pr2 h))] and A27: for h being Function st h in ([|A,B|] #) . pj holds y . h = [(f . (pr1 h)),(g . (pr2 h))] ; ::_thesis: x = y let h be Element of ([|A,B|] #) . pj; :: according to FUNCT_2:def_8 ::_thesis: x . h = y . h h in ([|A,B|] #) . pj ; then h in product ([|A,B|] * pj) by FINSEQ_2:def_5; then consider h1 being Function such that A28: h1 = h and dom h1 = dom ([|A,B|] * pj) and for z being set st z in dom ([|A,B|] * pj) holds h1 . z in ([|A,B|] * pj) . z by CARD_3:def_5; x . h1 = [(f . (pr1 h1)),(g . (pr2 h1))] by A26, A28; hence x . h = y . h by A27, A28; ::_thesis: verum end; end; :: deftheorem defines [[: PRALG_2:def_3_:_ for I being non empty set for A, B being V2() ManySortedSet of I for pj being Element of I * for rj being Element of I for f being Function of ((A #) . pj),(A . rj) for g being Function of ((B #) . pj),(B . rj) for b8 being Function of (([|A,B|] #) . pj),([|A,B|] . rj) holds ( b8 = [[:f,g:]] iff for h being Function st h in ([|A,B|] #) . pj holds b8 . h = [(f . (pr1 h)),(g . (pr2 h))] ); definition let I be non empty set ; let J be set ; let A, B be V2() ManySortedSet of I; let p be Function of J,(I *); let r be Function of J,I; let F be ManySortedFunction of (A #) * p,A * r; let G be ManySortedFunction of (B #) * p,B * r; func[[:F,G:]] -> ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r means :: PRALG_2:def 4 for j being set st j in J holds for pj being Element of I * for rj being Element of I st pj = p . j & rj = r . j holds for f being Function of ((A #) . pj),(A . rj) for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds it . j = [[:f,g:]]; existence ex b1 being ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r st for j being set st j in J holds for pj being Element of I * for rj being Element of I st pj = p . j & rj = r . j holds for f being Function of ((A #) . pj),(A . rj) for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds b1 . j = [[:f,g:]] proof defpred S1[ set , set ] means for pj being Element of I * for rj being Element of I st pj = p . $1 & rj = r . $1 holds for f being Function of ((A #) . pj),(A . rj) for g being Function of ((B #) . pj),(B . rj) st f = F . $1 & g = G . $1 holds $2 = [[:f,g:]]; A1: for j being set st j in J holds ex i being set st S1[j,i] proof let j be set ; ::_thesis: ( j in J implies ex i being set st S1[j,i] ) assume A2: j in J ; ::_thesis: ex i being set st S1[j,i] then reconsider pj = p . j as Element of I * by FUNCT_2:5; reconsider rj = r . j as Element of I by A2, FUNCT_2:5; A3: j in dom r by A2, FUNCT_2:def_1; then A4: A . (r . j) = (A * r) . j by FUNCT_1:13; A5: B . (r . j) = (B * r) . j by A3, FUNCT_1:13; A6: j in dom p by A2, FUNCT_2:def_1; then (A #) . (p . j) = ((A #) * p) . j by FUNCT_1:13; then reconsider f = F . j as Function of ((A #) . pj),(A . rj) by A2, A4, PBOOLE:def_15; (B #) . (p . j) = ((B #) * p) . j by A6, FUNCT_1:13; then reconsider g = G . j as Function of ((B #) . pj),(B . rj) by A2, A5, PBOOLE:def_15; take [[:f,g:]] ; ::_thesis: S1[j,[[:f,g:]]] thus S1[j,[[:f,g:]]] ; ::_thesis: verum end; consider h being Function such that A7: ( dom h = J & ( for j being set st j in J holds S1[j,h . j] ) ) from CLASSES1:sch_1(A1); reconsider h = h as ManySortedSet of J by A7, PARTFUN1:def_2, RELAT_1:def_18; for j being set st j in dom h holds h . j is Function proof let j be set ; ::_thesis: ( j in dom h implies h . j is Function ) assume A8: j in dom h ; ::_thesis: h . j is Function then reconsider pj = p . j as Element of I * by A7, FUNCT_2:5; reconsider rj = r . j as Element of I by A7, A8, FUNCT_2:5; A9: j in dom r by A7, A8, FUNCT_2:def_1; then A10: A . (r . j) = (A * r) . j by FUNCT_1:13; A11: B . (r . j) = (B * r) . j by A9, FUNCT_1:13; A12: j in dom p by A7, A8, FUNCT_2:def_1; then (A #) . (p . j) = ((A #) * p) . j by FUNCT_1:13; then reconsider f = F . j as Function of ((A #) . pj),(A . rj) by A7, A8, A10, PBOOLE:def_15; (B #) . (p . j) = ((B #) * p) . j by A12, FUNCT_1:13; then reconsider g = G . j as Function of ((B #) . pj),(B . rj) by A7, A8, A11, PBOOLE:def_15; h . j = [[:f,g:]] by A7, A8; hence h . j is Function ; ::_thesis: verum end; then reconsider h = h as ManySortedFunction of J by FUNCOP_1:def_6; for j being set st j in J holds h . j is Function of ((([|A,B|] #) * p) . j),(([|A,B|] * r) . j) proof let j be set ; ::_thesis: ( j in J implies h . j is Function of ((([|A,B|] #) * p) . j),(([|A,B|] * r) . j) ) assume A13: j in J ; ::_thesis: h . j is Function of ((([|A,B|] #) * p) . j),(([|A,B|] * r) . j) then reconsider pj = p . j as Element of I * by FUNCT_2:5; reconsider rj = r . j as Element of I by A13, FUNCT_2:5; A14: j in dom p by A13, FUNCT_2:def_1; then A15: (([|A,B|] #) * p) . j = ([|A,B|] #) . (p . j) by FUNCT_1:13; A16: j in dom r by A13, FUNCT_2:def_1; then A17: A . (r . j) = (A * r) . j by FUNCT_1:13; A18: ([|A,B|] * r) . j = [|A,B|] . (r . j) by A16, FUNCT_1:13; A19: B . (r . j) = (B * r) . j by A16, FUNCT_1:13; (B #) . (p . j) = ((B #) * p) . j by A14, FUNCT_1:13; then reconsider g = G . j as Function of ((B #) . pj),(B . rj) by A13, A19, PBOOLE:def_15; (A #) . (p . j) = ((A #) * p) . j by A14, FUNCT_1:13; then reconsider f = F . j as Function of ((A #) . pj),(A . rj) by A13, A17, PBOOLE:def_15; h . j = [[:f,g:]] by A7, A13; hence h . j is Function of ((([|A,B|] #) * p) . j),(([|A,B|] * r) . j) by A15, A18; ::_thesis: verum end; then reconsider h = h as ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r by PBOOLE:def_15; take h ; ::_thesis: for j being set st j in J holds for pj being Element of I * for rj being Element of I st pj = p . j & rj = r . j holds for f being Function of ((A #) . pj),(A . rj) for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds h . j = [[:f,g:]] thus for j being set st j in J holds for pj being Element of I * for rj being Element of I st pj = p . j & rj = r . j holds for f being Function of ((A #) . pj),(A . rj) for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds h . j = [[:f,g:]] by A7; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r st ( for j being set st j in J holds for pj being Element of I * for rj being Element of I st pj = p . j & rj = r . j holds for f being Function of ((A #) . pj),(A . rj) for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds b1 . j = [[:f,g:]] ) & ( for j being set st j in J holds for pj being Element of I * for rj being Element of I st pj = p . j & rj = r . j holds for f being Function of ((A #) . pj),(A . rj) for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds b2 . j = [[:f,g:]] ) holds b1 = b2 proof let x, y be ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r; ::_thesis: ( ( for j being set st j in J holds for pj being Element of I * for rj being Element of I st pj = p . j & rj = r . j holds for f being Function of ((A #) . pj),(A . rj) for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds x . j = [[:f,g:]] ) & ( for j being set st j in J holds for pj being Element of I * for rj being Element of I st pj = p . j & rj = r . j holds for f being Function of ((A #) . pj),(A . rj) for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds y . j = [[:f,g:]] ) implies x = y ) assume that A20: for j being set st j in J holds for pj being Element of I * for rj being Element of I st pj = p . j & rj = r . j holds for f being Function of ((A #) . pj),(A . rj) for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds x . j = [[:f,g:]] and A21: for j being set st j in J holds for pj being Element of I * for rj being Element of I st pj = p . j & rj = r . j holds for f being Function of ((A #) . pj),(A . rj) for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds y . j = [[:f,g:]] ; ::_thesis: x = y for j being set st j in J holds x . j = y . j proof let j be set ; ::_thesis: ( j in J implies x . j = y . j ) assume A22: j in J ; ::_thesis: x . j = y . j then reconsider pj = p . j as Element of I * by FUNCT_2:5; reconsider rj = r . j as Element of I by A22, FUNCT_2:5; A23: j in dom r by A22, FUNCT_2:def_1; then A24: A . (r . j) = (A * r) . j by FUNCT_1:13; A25: B . (r . j) = (B * r) . j by A23, FUNCT_1:13; A26: j in dom p by A22, FUNCT_2:def_1; then (A #) . (p . j) = ((A #) * p) . j by FUNCT_1:13; then reconsider f = F . j as Function of ((A #) . pj),(A . rj) by A22, A24, PBOOLE:def_15; (B #) . (p . j) = ((B #) * p) . j by A26, FUNCT_1:13; then reconsider g = G . j as Function of ((B #) . pj),(B . rj) by A22, A25, PBOOLE:def_15; x . j = [[:f,g:]] by A20, A22; hence x . j = y . j by A21, A22; ::_thesis: verum end; hence x = y by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem defines [[: PRALG_2:def_4_:_ for I being non empty set for J being set for A, B being V2() ManySortedSet of I for p being Function of J,(I *) for r being Function of J,I for F being ManySortedFunction of (A #) * p,A * r for G being ManySortedFunction of (B #) * p,B * r for b9 being ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r holds ( b9 = [[:F,G:]] iff for j being set st j in J holds for pj being Element of I * for rj being Element of I st pj = p . j & rj = r . j holds for f being Function of ((A #) . pj),(A . rj) for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds b9 . j = [[:f,g:]] ); begin definition let I be set ; let S be non empty ManySortedSign ; mode MSAlgebra-Family of I,S -> ManySortedSet of I means :Def5: :: PRALG_2:def 5 for i being set st i in I holds it . i is non-empty MSAlgebra over S; existence ex b1 being ManySortedSet of I st for i being set st i in I holds b1 . i is non-empty MSAlgebra over S proof set A = the non-empty MSAlgebra over S; set f = I --> the non-empty MSAlgebra over S; reconsider f = I --> the non-empty MSAlgebra over S as ManySortedSet of I ; take f ; ::_thesis: for i being set st i in I holds f . i is non-empty MSAlgebra over S let i be set ; ::_thesis: ( i in I implies f . i is non-empty MSAlgebra over S ) assume i in I ; ::_thesis: f . i is non-empty MSAlgebra over S hence f . i is non-empty MSAlgebra over S by FUNCOP_1:7; ::_thesis: verum end; end; :: deftheorem Def5 defines MSAlgebra-Family PRALG_2:def_5_:_ for I being set for S being non empty ManySortedSign for b3 being ManySortedSet of I holds ( b3 is MSAlgebra-Family of I,S iff for i being set st i in I holds b3 . i is non-empty MSAlgebra over S ); definition let I be non empty set ; let S be non empty ManySortedSign ; let A be MSAlgebra-Family of I,S; let i be Element of I; :: original: . redefine funcA . i -> non-empty MSAlgebra over S; coherence A . i is non-empty MSAlgebra over S by Def5; end; definition let S be non empty ManySortedSign ; let U1 be MSAlgebra over S; func|.U1.| -> set equals :: PRALG_2:def 6 union (rng the Sorts of U1); coherence union (rng the Sorts of U1) is set ; end; :: deftheorem defines |. PRALG_2:def_6_:_ for S being non empty ManySortedSign for U1 being MSAlgebra over S holds |.U1.| = union (rng the Sorts of U1); registration let S be non empty ManySortedSign ; let U1 be non-empty MSAlgebra over S; cluster|.U1.| -> non empty ; coherence not |.U1.| is empty proof reconsider St = the Sorts of U1 as V2() ManySortedSet of the carrier of S ; set s = the SortSymbol of S; dom the Sorts of U1 = the carrier of S by PARTFUN1:def_2; then A1: the Sorts of U1 . the SortSymbol of S in rng the Sorts of U1 by FUNCT_1:def_3; ex x being set st x in St . the SortSymbol of S by XBOOLE_0:def_1; hence not |.U1.| is empty by A1, TARSKI:def_4; ::_thesis: verum end; end; definition let I be non empty set ; let S be non empty ManySortedSign ; let A be MSAlgebra-Family of I,S; func|.A.| -> set equals :: PRALG_2:def 7 union { |.(A . i).| where i is Element of I : verum } ; coherence union { |.(A . i).| where i is Element of I : verum } is set ; end; :: deftheorem defines |. PRALG_2:def_7_:_ for I being non empty set for S being non empty ManySortedSign for A being MSAlgebra-Family of I,S holds |.A.| = union { |.(A . i).| where i is Element of I : verum } ; registration let I be non empty set ; let S be non empty ManySortedSign ; let A be MSAlgebra-Family of I,S; cluster|.A.| -> non empty ; coherence not |.A.| is empty proof set a = the Element of I; set X = { |.(A . i).| where i is Element of I : verum } ; ( |.(A . the Element of I).| in { |.(A . i).| where i is Element of I : verum } & ex x being set st x in |.(A . the Element of I).| ) by XBOOLE_0:def_1; hence not |.A.| is empty by TARSKI:def_4; ::_thesis: verum end; end; begin theorem Th3: :: PRALG_2:3 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for o being OperSymbol of S holds ( Args (o,U0) = product ( the Sorts of U0 * (the_arity_of o)) & dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) & Result (o,U0) = the Sorts of U0 . (the_result_sort_of o) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for o being OperSymbol of S holds ( Args (o,U0) = product ( the Sorts of U0 * (the_arity_of o)) & dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) & Result (o,U0) = the Sorts of U0 . (the_result_sort_of o) ) let U0 be MSAlgebra over S; ::_thesis: for o being OperSymbol of S holds ( Args (o,U0) = product ( the Sorts of U0 * (the_arity_of o)) & dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) & Result (o,U0) = the Sorts of U0 . (the_result_sort_of o) ) let o be OperSymbol of S; ::_thesis: ( Args (o,U0) = product ( the Sorts of U0 * (the_arity_of o)) & dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) & Result (o,U0) = the Sorts of U0 . (the_result_sort_of o) ) set So = the Sorts of U0; set Ar = the Arity of S; set Rs = the ResultSort of S; set ar = the_arity_of o; set AS = ( the Sorts of U0 #) * the Arity of S; set RS = the Sorts of U0 * the ResultSort of S; set X = the carrier' of S; set Cr = the carrier of S; A1: dom the Arity of S = the carrier' of S by FUNCT_2:def_1; then A2: dom (( the Sorts of U0 #) * the Arity of S) = dom the Arity of S by PARTFUN1:def_2; thus Args (o,U0) = (( the Sorts of U0 #) * the Arity of S) . o by MSUALG_1:def_4 .= ( the Sorts of U0 #) . ( the Arity of S . o) by A1, A2, FUNCT_1:12 .= ( the Sorts of U0 #) . (the_arity_of o) by MSUALG_1:def_1 .= product ( the Sorts of U0 * (the_arity_of o)) by FINSEQ_2:def_5 ; ::_thesis: ( dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) & Result (o,U0) = the Sorts of U0 . (the_result_sort_of o) ) ( rng (the_arity_of o) c= the carrier of S & dom the Sorts of U0 = the carrier of S ) by FINSEQ_1:def_4, PARTFUN1:def_2; hence dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27; ::_thesis: Result (o,U0) = the Sorts of U0 . (the_result_sort_of o) A3: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1; then A4: dom ( the Sorts of U0 * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def_2; thus 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 A3, A4, FUNCT_1:12 .= the Sorts of U0 . (the_result_sort_of o) by MSUALG_1:def_2 ; ::_thesis: verum end; theorem Th4: :: PRALG_2:4 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 = {} holds Args (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 = {} holds Args (o,U0) = {{}} let U0 be MSAlgebra over S; ::_thesis: for o being OperSymbol of S st the_arity_of o = {} holds Args (o,U0) = {{}} let o be OperSymbol of S; ::_thesis: ( the_arity_of o = {} implies Args (o,U0) = {{}} ) assume A1: the_arity_of o = {} ; ::_thesis: Args (o,U0) = {{}} thus Args (o,U0) = product ( the Sorts of U0 * (the_arity_of o)) by Th3 .= {{}} by A1, CARD_3:10 ; ::_thesis: verum end; definition let S be non empty ManySortedSign ; let U1, U2 be non-empty MSAlgebra over S; func[:U1,U2:] -> MSAlgebra over S equals :: PRALG_2:def 8 MSAlgebra(# [| the Sorts of U1, the Sorts of U2|],[[: the Charact of U1, the Charact of U2:]] #); coherence MSAlgebra(# [| the Sorts of U1, the Sorts of U2|],[[: the Charact of U1, the Charact of U2:]] #) is MSAlgebra over S ; end; :: deftheorem defines [: PRALG_2:def_8_:_ for S being non empty ManySortedSign for U1, U2 being non-empty MSAlgebra over S holds [:U1,U2:] = MSAlgebra(# [| the Sorts of U1, the Sorts of U2|],[[: the Charact of U1, the Charact of U2:]] #); registration let S be non empty ManySortedSign ; let U1, U2 be non-empty MSAlgebra over S; cluster[:U1,U2:] -> strict ; coherence [:U1,U2:] is strict ; end; definition let I be set ; let S be non empty ManySortedSign ; let s be SortSymbol of S; let A be MSAlgebra-Family of I,S; func Carrier (A,s) -> ManySortedSet of I means :Def9: :: PRALG_2:def 9 for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & it . i = the Sorts of U0 . s ) if I <> {} otherwise it = {} ; existence ( ( I <> {} implies ex b1 being ManySortedSet of I st for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & b1 . i = the Sorts of U0 . s ) ) & ( not I <> {} implies ex b1 being ManySortedSet of I st b1 = {} ) ) proof hereby ::_thesis: ( not I <> {} implies ex b1 being ManySortedSet of I st b1 = {} ) assume I <> {} ; ::_thesis: ex f being ManySortedSet of I st for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & f . i = the Sorts of U0 . s ) then reconsider I9 = I as non empty set ; reconsider A9 = A as MSAlgebra-Family of I9,S ; deffunc H1( Element of I9) -> set = the Sorts of (A9 . $1) . s; consider f being Function such that A1: ( dom f = I9 & ( for i being Element of I9 holds f . i = H1(i) ) ) from FUNCT_1:sch_4(); reconsider f = f as ManySortedSet of I by A1, PARTFUN1:def_2, RELAT_1:def_18; take f = f; ::_thesis: for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & f . i = the Sorts of U0 . s ) let i be set ; ::_thesis: ( i in I implies ex U0 being MSAlgebra over S st ( U0 = A . i & f . i = the Sorts of U0 . s ) ) assume i in I ; ::_thesis: ex U0 being MSAlgebra over S st ( U0 = A . i & f . i = the Sorts of U0 . s ) then reconsider i9 = i as Element of I9 ; reconsider U0 = A9 . i9 as MSAlgebra over S ; take U0 = U0; ::_thesis: ( U0 = A . i & f . i = the Sorts of U0 . s ) thus ( U0 = A . i & f . i = the Sorts of U0 . s ) by A1; ::_thesis: verum end; assume A2: I = {} ; ::_thesis: ex b1 being ManySortedSet of I st b1 = {} take [[0]] I ; ::_thesis: [[0]] I = {} thus [[0]] I = {} by A2; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedSet of I holds ( ( I <> {} & ( for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & b1 . i = the Sorts of U0 . s ) ) & ( for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & b2 . i = the Sorts of U0 . s ) ) implies b1 = b2 ) & ( not I <> {} & b1 = {} & b2 = {} implies b1 = b2 ) ) proof let f, g be ManySortedSet of I; ::_thesis: ( ( I <> {} & ( for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & f . i = the Sorts of U0 . s ) ) & ( for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & g . i = the Sorts of U0 . s ) ) implies f = g ) & ( not I <> {} & f = {} & g = {} implies f = g ) ) hereby ::_thesis: ( not I <> {} & f = {} & g = {} implies f = g ) assume I <> {} ; ::_thesis: ( ( for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & f . i = the Sorts of U0 . s ) ) & ( for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & g . i = the Sorts of U0 . s ) ) implies f = g ) assume A3: ( ( for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & f . i = the Sorts of U0 . s ) ) & ( for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & g . i = the Sorts of U0 . s ) ) ) ; ::_thesis: f = g for x being set st x in I holds f . x = g . x proof let x be set ; ::_thesis: ( x in I implies f . x = g . x ) assume A4: x in I ; ::_thesis: f . x = g . x then reconsider i = x as Element of I ; ( ex U0 being MSAlgebra over S st ( U0 = A . i & f . i = the Sorts of U0 . s ) & ex U0 being MSAlgebra over S st ( U0 = A . i & g . i = the Sorts of U0 . s ) ) by A3, A4; hence f . x = g . x ; ::_thesis: verum end; hence f = g by PBOOLE:3; ::_thesis: verum end; thus ( not I <> {} & f = {} & g = {} implies f = g ) ; ::_thesis: verum end; correctness consistency for b1 being ManySortedSet of I holds verum; ; end; :: deftheorem Def9 defines Carrier PRALG_2:def_9_:_ for I being set for S being non empty ManySortedSign for s being SortSymbol of S for A being MSAlgebra-Family of I,S for b5 being ManySortedSet of I holds ( ( I <> {} implies ( b5 = Carrier (A,s) iff for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & b5 . i = the Sorts of U0 . s ) ) ) & ( not I <> {} implies ( b5 = Carrier (A,s) iff b5 = {} ) ) ); registration let I be set ; let S be non empty ManySortedSign ; let s be SortSymbol of S; let A be MSAlgebra-Family of I,S; cluster Carrier (A,s) -> V2() ; coherence Carrier (A,s) is non-empty proof let x be set ; :: according to PBOOLE:def_13 ::_thesis: ( not x in I or not (Carrier (A,s)) . x is empty ) assume A1: x in I ; ::_thesis: not (Carrier (A,s)) . x is empty then consider U0 being MSAlgebra over S such that A2: U0 = A . x and A3: (Carrier (A,s)) . x = the Sorts of U0 . s by Def9; U0 is non-empty MSAlgebra over S by A1, A2, Def5; hence not (Carrier (A,s)) . x is empty by A3; ::_thesis: verum end; end; definition let I be set ; let S be non empty ManySortedSign ; let A be MSAlgebra-Family of I,S; func SORTS A -> ManySortedSet of the carrier of S means :Def10: :: PRALG_2:def 10 for s being SortSymbol of S holds it . s = product (Carrier (A,s)); existence ex b1 being ManySortedSet of the carrier of S st for s being SortSymbol of S holds b1 . s = product (Carrier (A,s)) proof deffunc H1( SortSymbol of S) -> set = product (Carrier (A,$1)); consider f being Function such that A1: ( dom f = the carrier of S & ( for s being SortSymbol of S holds f . s = H1(s) ) ) from FUNCT_1:sch_4(); reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18; take f ; ::_thesis: for s being SortSymbol of S holds f . s = product (Carrier (A,s)) thus for s being SortSymbol of S holds f . s = product (Carrier (A,s)) by A1; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedSet of the carrier of S st ( for s being SortSymbol of S holds b1 . s = product (Carrier (A,s)) ) & ( for s being SortSymbol of S holds b2 . s = product (Carrier (A,s)) ) holds b1 = b2 proof let f, g be ManySortedSet of the carrier of S; ::_thesis: ( ( for s being SortSymbol of S holds f . s = product (Carrier (A,s)) ) & ( for s being SortSymbol of S holds g . s = product (Carrier (A,s)) ) implies f = g ) assume that A2: for s being SortSymbol of S holds f . s = product (Carrier (A,s)) and A3: for s being SortSymbol of S holds g . s = product (Carrier (A,s)) ; ::_thesis: f = g for x being set st x in the carrier of S holds f . x = g . x proof let x be set ; ::_thesis: ( x in the carrier of S implies f . x = g . x ) assume x in the carrier of S ; ::_thesis: f . x = g . x then reconsider x1 = x as SortSymbol of S ; f . x1 = product (Carrier (A,x1)) by A2; hence f . x = g . x by A3; ::_thesis: verum end; hence f = g by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def10 defines SORTS PRALG_2:def_10_:_ for I being set for S being non empty ManySortedSign for A being MSAlgebra-Family of I,S for b4 being ManySortedSet of the carrier of S holds ( b4 = SORTS A iff for s being SortSymbol of S holds b4 . s = product (Carrier (A,s)) ); registration let I be set ; let S be non empty ManySortedSign ; let A be MSAlgebra-Family of I,S; cluster SORTS A -> V2() ; coherence SORTS A is non-empty proof let x be set ; :: according to PBOOLE:def_13 ::_thesis: ( not x in the carrier of S or not (SORTS A) . x is empty ) assume x in the carrier of S ; ::_thesis: not (SORTS A) . x is empty then reconsider s = x as SortSymbol of S ; (SORTS A) . s = product (Carrier (A,s)) by Def10; hence not (SORTS A) . x is empty ; ::_thesis: verum end; end; definition let I be set ; let S be non empty ManySortedSign ; let A be MSAlgebra-Family of I,S; func OPER A -> ManySortedFunction of I means :Def11: :: PRALG_2:def 11 for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & it . i = the Charact of U0 ) if I <> {} otherwise it = {} ; existence ( ( I <> {} implies ex b1 being ManySortedFunction of I st for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & b1 . i = the Charact of U0 ) ) & ( not I <> {} implies ex b1 being ManySortedFunction of I st b1 = {} ) ) proof reconsider f = [[0]] I as ManySortedFunction of I ; hereby ::_thesis: ( not I <> {} implies ex b1 being ManySortedFunction of I st b1 = {} ) assume I <> {} ; ::_thesis: ex X being ManySortedFunction of I st for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & X . i = the Charact of U0 ) then reconsider I9 = I as non empty set ; reconsider A9 = A as MSAlgebra-Family of I9,S ; deffunc H1( Element of I9) -> ManySortedFunction of the Arity of S * ( the Sorts of (A9 . $1) #), the ResultSort of S * the Sorts of (A9 . $1) = the Charact of (A9 . $1); consider X being ManySortedSet of I9 such that A1: for i being Element of I9 holds X . i = H1(i) from PBOOLE:sch_5(); for x being set st x in dom X holds X . x is Function proof let x be set ; ::_thesis: ( x in dom X implies X . x is Function ) assume x in dom X ; ::_thesis: X . x is Function then reconsider i = x as Element of I9 by PARTFUN1:def_2; X . i = the Charact of (A9 . i) by A1; hence X . x is Function ; ::_thesis: verum end; then reconsider X = X as ManySortedFunction of I by FUNCOP_1:def_6; take X = X; ::_thesis: for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & X . i = the Charact of U0 ) let i be set ; ::_thesis: ( i in I implies ex U0 being MSAlgebra over S st ( U0 = A . i & X . i = the Charact of U0 ) ) assume i in I ; ::_thesis: ex U0 being MSAlgebra over S st ( U0 = A . i & X . i = the Charact of U0 ) then reconsider i9 = i as Element of I9 ; reconsider U0 = A9 . i9 as MSAlgebra over S ; take U0 = U0; ::_thesis: ( U0 = A . i & X . i = the Charact of U0 ) thus ( U0 = A . i & X . i = the Charact of U0 ) by A1; ::_thesis: verum end; assume A2: I = {} ; ::_thesis: ex b1 being ManySortedFunction of I st b1 = {} take f ; ::_thesis: f = {} thus f = {} by A2; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of I holds ( ( I <> {} & ( for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & b1 . i = the Charact of U0 ) ) & ( for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & b2 . i = the Charact of U0 ) ) implies b1 = b2 ) & ( not I <> {} & b1 = {} & b2 = {} implies b1 = b2 ) ) proof let f, g be ManySortedFunction of I; ::_thesis: ( ( I <> {} & ( for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & f . i = the Charact of U0 ) ) & ( for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & g . i = the Charact of U0 ) ) implies f = g ) & ( not I <> {} & f = {} & g = {} implies f = g ) ) hereby ::_thesis: ( not I <> {} & f = {} & g = {} implies f = g ) assume I <> {} ; ::_thesis: ( ( for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & f . i = the Charact of U0 ) ) & ( for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & g . i = the Charact of U0 ) ) implies f = g ) assume A3: ( ( for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & f . i = the Charact of U0 ) ) & ( for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & g . i = the Charact of U0 ) ) ) ; ::_thesis: f = g for x being set st x in I holds f . x = g . x proof let x be set ; ::_thesis: ( x in I implies f . x = g . x ) assume A4: x in I ; ::_thesis: f . x = g . x then reconsider i = x as Element of I ; ( ex U0 being MSAlgebra over S st ( U0 = A . i & f . i = the Charact of U0 ) & ex U0 being MSAlgebra over S st ( U0 = A . i & g . i = the Charact of U0 ) ) by A3, A4; hence f . x = g . x ; ::_thesis: verum end; hence f = g by PBOOLE:3; ::_thesis: verum end; thus ( not I <> {} & f = {} & g = {} implies f = g ) ; ::_thesis: verum end; correctness consistency for b1 being ManySortedFunction of I holds verum; ; end; :: deftheorem Def11 defines OPER PRALG_2:def_11_:_ for I being set for S being non empty ManySortedSign for A being MSAlgebra-Family of I,S for b4 being ManySortedFunction of I holds ( ( I <> {} implies ( b4 = OPER A iff for i being set st i in I holds ex U0 being MSAlgebra over S st ( U0 = A . i & b4 . i = the Charact of U0 ) ) ) & ( not I <> {} implies ( b4 = OPER A iff b4 = {} ) ) ); theorem Th5: :: PRALG_2:5 for I being set for S being non empty ManySortedSign for A being MSAlgebra-Family of I,S holds dom (uncurry (OPER A)) = [:I, the carrier' of S:] proof let I be set ; ::_thesis: for S being non empty ManySortedSign for A being MSAlgebra-Family of I,S holds dom (uncurry (OPER A)) = [:I, the carrier' of S:] let S be non empty ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S holds dom (uncurry (OPER A)) = [:I, the carrier' of S:] let A be MSAlgebra-Family of I,S; ::_thesis: dom (uncurry (OPER A)) = [:I, the carrier' of S:] percases ( I <> {} or I = {} ) ; supposeA1: I <> {} ; ::_thesis: dom (uncurry (OPER A)) = [:I, the carrier' of S:] thus dom (uncurry (OPER A)) c= [:I, the carrier' of S:] :: according to XBOOLE_0:def_10 ::_thesis: [:I, the carrier' of S:] c= dom (uncurry (OPER A)) proof let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in dom (uncurry (OPER A)) or t in [:I, the carrier' of S:] ) assume t in dom (uncurry (OPER A)) ; ::_thesis: t in [:I, the carrier' of S:] then consider x being set , g being Function, y being set such that A2: t = [x,y] and A3: x in dom (OPER A) and A4: ( g = (OPER A) . x & y in dom g ) by FUNCT_5:def_2; reconsider x = x as Element of I by A3, PARTFUN1:def_2; ex U0 being MSAlgebra over S st ( U0 = A . x & (OPER A) . x = the Charact of U0 ) by A1, Def11; then A5: y in the carrier' of S by A4, PARTFUN1:def_2; x in I by A3, PARTFUN1:def_2; hence t in [:I, the carrier' of S:] by A2, A5, ZFMISC_1:87; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:I, the carrier' of S:] or x in dom (uncurry (OPER A)) ) assume A6: x in [:I, the carrier' of S:] ; ::_thesis: x in dom (uncurry (OPER A)) then consider y, z being set such that A7: x = [y,z] by RELAT_1:def_1; A8: z in the carrier' of S by A6, A7, ZFMISC_1:87; reconsider y = y as Element of I by A6, A7, ZFMISC_1:87; consider U0 being MSAlgebra over S such that U0 = A . y and A9: (OPER A) . y = the Charact of U0 by A1, Def11; ( dom the Charact of U0 = the carrier' of S & dom (OPER A) = I ) by PARTFUN1:def_2; hence x in dom (uncurry (OPER A)) by A1, A7, A8, A9, FUNCT_5:def_2; ::_thesis: verum end; supposeA10: I = {} ; ::_thesis: dom (uncurry (OPER A)) = [:I, the carrier' of S:] then OPER A = {} ; hence dom (uncurry (OPER A)) = [:I, the carrier' of S:] by A10, FUNCT_5:43, RELAT_1:38, ZFMISC_1:90; ::_thesis: verum end; end; end; theorem Th6: :: PRALG_2:6 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 holds commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER 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 holds commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A)))))) let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for o being OperSymbol of S holds commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A)))))) let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S holds commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A)))))) let o be OperSymbol of S; ::_thesis: commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A)))))) set f = uncurry (OPER A); dom (uncurry (OPER A)) = [:I, the carrier' of S:] by Th5; then ( [:I, the carrier' of S:] <> {} & uncurry (OPER A) in Funcs ([:I, the carrier' of S:],(rng (uncurry (OPER A)))) ) by FUNCT_2:def_2, ZFMISC_1:90; hence commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A)))))) by FUNCT_6:10; ::_thesis: verum end; definition let I be set ; let S be non empty non void ManySortedSign ; let A be MSAlgebra-Family of I,S; let o be OperSymbol of S; funcA ?. o -> ManySortedFunction of I equals :: PRALG_2:def 12 (commute (OPER A)) . o; coherence (commute (OPER A)) . o is ManySortedFunction of I proof set f = uncurry (OPER A); set C = commute (OPER A); A1: dom (uncurry (OPER A)) = [:I, the carrier' of S:] by Th5; percases ( I <> {} or I = {} ) ; supposeA2: I <> {} ; ::_thesis: (commute (OPER A)) . o is ManySortedFunction of I then commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A)))))) by Th6; then A3: ex a being Function st ( a = commute (OPER A) & dom a = the carrier' of S & rng a 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 consider g being Function such that A4: g = (commute (OPER A)) . o and A5: dom g = I and rng g c= rng (uncurry (OPER A)) by A3, FUNCT_2:def_2; reconsider g = g as ManySortedSet of I by A5, PARTFUN1:def_2, RELAT_1:def_18; for x being set st x in dom g holds g . x is Function proof let x be set ; ::_thesis: ( x in dom g implies g . x is Function ) assume x in dom g ; ::_thesis: g . x is Function then reconsider i = x as Element of I by A5; A6: ( [i,o] `1 = i & [i,o] `2 = o ) ; consider U0 being MSAlgebra over S such that U0 = A . i and A7: (OPER A) . i = the Charact of U0 by A2, Def11; A8: [i,o] in dom (uncurry (OPER A)) by A1, A2, ZFMISC_1:87; then g . i = (uncurry (OPER A)) . (i,o) by A4, FUNCT_5:22; then g . i = the Charact of U0 . o by A8, A6, A7, FUNCT_5:def_2 .= Den (o,U0) by MSUALG_1:def_6 ; hence g . x is Function ; ::_thesis: verum end; hence (commute (OPER A)) . o is ManySortedFunction of I by A4, FUNCOP_1:def_6; ::_thesis: verum end; supposeA9: I = {} ; ::_thesis: (commute (OPER A)) . o is ManySortedFunction of I reconsider f = [[0]] I as ManySortedFunction of I ; f = {} by A9 .= (commute {}) . o by FUNCT_6:58 .= (commute (OPER A)) . o by A9 ; hence (commute (OPER A)) . o is ManySortedFunction of I ; ::_thesis: verum end; end; end; end; :: deftheorem defines ?. PRALG_2:def_12_:_ 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 holds A ?. o = (commute (OPER A)) . o; theorem Th7: :: PRALG_2:7 for I being non empty set for i being Element of I for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S holds (A ?. o) . i = Den (o,(A . i)) proof let I be non empty set ; ::_thesis: for i being Element of I for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S holds (A ?. o) . i = Den (o,(A . i)) let i be Element of I; ::_thesis: for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for o being OperSymbol of S holds (A ?. o) . i = Den (o,(A . i)) let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for o being OperSymbol of S holds (A ?. o) . i = Den (o,(A . i)) let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S holds (A ?. o) . i = Den (o,(A . i)) let o be OperSymbol of S; ::_thesis: (A ?. o) . i = Den (o,(A . i)) set O = the carrier' of S; set f = uncurry (OPER A); A1: ( [i,o] `1 = i & [i,o] `2 = o ) ; A2: ex U0 being MSAlgebra over S st ( U0 = A . i & (OPER A) . i = the Charact of U0 ) by Def11; A3: dom (uncurry (OPER A)) = [:I, the carrier' of S:] by Th5; then A4: [i,o] in dom (uncurry (OPER A)) by ZFMISC_1:87; [:I, the carrier' of S:] <> {} by ZFMISC_1:90; then consider g being Function such that A5: (curry' (uncurry (OPER A))) . o = g and dom g = I and rng g c= rng (uncurry (OPER A)) and A6: for x being set st x in I holds g . x = (uncurry (OPER A)) . (x,o) by A3, FUNCT_5:32; g . i = (uncurry (OPER A)) . (i,o) by A6; then g . i = the Charact of (A . i) . o by A4, A1, A2, FUNCT_5:def_2 .= Den (o,(A . i)) by MSUALG_1:def_6 ; hence (A ?. o) . i = Den (o,(A . i)) by A5; ::_thesis: verum end; theorem :: PRALG_2: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 for x being set st x in rng (Frege (A ?. o)) holds x is Function 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 set st x in rng (Frege (A ?. o)) holds x is Function 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 set st x in rng (Frege (A ?. o)) holds x is Function let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S for x being set st x in rng (Frege (A ?. o)) holds x is Function let o be OperSymbol of S; ::_thesis: for x being set st x in rng (Frege (A ?. o)) holds x is Function let x be set ; ::_thesis: ( x in rng (Frege (A ?. o)) implies x is Function ) assume x in rng (Frege (A ?. o)) ; ::_thesis: x is Function then ex y being set st ( y in dom (Frege (A ?. o)) & (Frege (A ?. o)) . y = x ) by FUNCT_1:def_3; hence x is Function ; ::_thesis: verum end; theorem Th9: :: PRALG_2:9 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 f in rng (Frege (A ?. o)) holds ( dom f = I & ( for i being Element of I holds f . i in Result (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 o being OperSymbol of S for f being Function st f in rng (Frege (A ?. o)) holds ( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . 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 f being Function st f in rng (Frege (A ?. o)) holds ( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) ) let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S for f being Function st f in rng (Frege (A ?. o)) holds ( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) ) let o be OperSymbol of S; ::_thesis: for f being Function st f in rng (Frege (A ?. o)) holds ( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) ) let f be Function; ::_thesis: ( f in rng (Frege (A ?. o)) implies ( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) ) ) A1: dom (A ?. o) = I by PARTFUN1:def_2; A2: SubFuncs (rng (A ?. o)) = rng (A ?. o) proof thus SubFuncs (rng (A ?. o)) c= rng (A ?. o) by FUNCT_6:18; :: according to XBOOLE_0:def_10 ::_thesis: rng (A ?. o) c= SubFuncs (rng (A ?. o)) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (A ?. o) or x in SubFuncs (rng (A ?. o)) ) assume A3: x in rng (A ?. o) ; ::_thesis: x in SubFuncs (rng (A ?. o)) then ex j being set st ( j in dom (A ?. o) & x = (A ?. o) . j ) by FUNCT_1:def_3; hence x in SubFuncs (rng (A ?. o)) by A3, FUNCT_6:def_1; ::_thesis: verum end; assume f in rng (Frege (A ?. o)) ; ::_thesis: ( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) ) then consider y being set such that A4: y in dom (Frege (A ?. o)) and A5: (Frege (A ?. o)) . y = f by FUNCT_1:def_3; A6: dom (Frege (A ?. o)) = product (doms (A ?. o)) by PARTFUN1:def_2; then consider g being Function such that A7: g = y and dom g = dom (doms (A ?. o)) and A8: for i being set st i in dom (doms (A ?. o)) holds g . i in (doms (A ?. o)) . i by A4, CARD_3:def_5; A9: f = (A ?. o) .. g by A4, A5, A6, A7, Def2; hence dom f = dom (A ?. o) by PRALG_1:def_17 .= I by PARTFUN1:def_2 ; ::_thesis: for i being Element of I holds f . i in Result (o,(A . i)) let i be Element of I; ::_thesis: f . i in Result (o,(A . i)) A10: (A ?. o) . i = Den (o,(A . i)) by Th7; dom (doms (A ?. o)) = (A ?. o) " (SubFuncs (rng (A ?. o))) by FUNCT_6:def_2 .= dom (A ?. o) by A2, RELAT_1:134 ; then g . i in (doms (A ?. o)) . i by A8, A1; then A11: g . i in dom (Den (o,(A . i))) by A1, A10, FUNCT_6:22; f . i = (Den (o,(A . i))) . (g . i) by A9, A1, A10, PRALG_1:def_17; then A12: f . i in rng (Den (o,(A . i))) by A11, FUNCT_1:def_3; rng (Den (o,(A . i))) c= Result (o,(A . i)) by RELAT_1:def_19; hence f . i in Result (o,(A . i)) by A12; ::_thesis: verum end; theorem Th10: :: PRALG_2: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 f in dom (Frege (A ?. o)) holds ( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.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 f in dom (Frege (A ?. o)) holds ( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.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 f in dom (Frege (A ?. o)) holds ( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) ) let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S for f being Function st f in dom (Frege (A ?. o)) holds ( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) ) let o be OperSymbol of S; ::_thesis: for f being Function st f in dom (Frege (A ?. o)) holds ( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) ) let f be Function; ::_thesis: ( f in dom (Frege (A ?. o)) implies ( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) ) ) assume A1: f in dom (Frege (A ?. o)) ; ::_thesis: ( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) ) A2: dom (A ?. o) = I by PARTFUN1:def_2; A3: SubFuncs (rng (A ?. o)) = rng (A ?. o) proof thus SubFuncs (rng (A ?. o)) c= rng (A ?. o) by FUNCT_6:18; :: according to XBOOLE_0:def_10 ::_thesis: rng (A ?. o) c= SubFuncs (rng (A ?. o)) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (A ?. o) or x in SubFuncs (rng (A ?. o)) ) assume A4: x in rng (A ?. o) ; ::_thesis: x in SubFuncs (rng (A ?. o)) then ex j being set st ( j in dom (A ?. o) & x = (A ?. o) . j ) by FUNCT_1:def_3; hence x in SubFuncs (rng (A ?. o)) by A4, FUNCT_6:def_1; ::_thesis: verum end; A5: dom (Frege (A ?. o)) = product (doms (A ?. o)) by PARTFUN1:def_2; A6: dom (doms (A ?. o)) = (A ?. o) " (SubFuncs (rng (A ?. o))) by FUNCT_6:def_2 .= dom (A ?. o) by A3, RELAT_1:134 ; hence dom f = I by A1, A5, A2, CARD_3:9; ::_thesis: ( ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) ) thus A7: for i being Element of I holds f . i in Args (o,(A . i)) ::_thesis: rng f c= Funcs ((dom (the_arity_of o)),|.A.|) proof let i be Element of I; ::_thesis: f . i in Args (o,(A . i)) ( (A ?. o) . i = Den (o,(A . i)) & f . i in (doms (A ?. o)) . i ) by A1, A5, A2, A6, Th7, CARD_3:9; then f . i in dom (Den (o,(A . i))) by A2, FUNCT_6:22; hence f . i in Args (o,(A . i)) by FUNCT_2:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in Funcs ((dom (the_arity_of o)),|.A.|) ) assume x in rng f ; ::_thesis: x in Funcs ((dom (the_arity_of o)),|.A.|) then consider y being set such that A8: y in dom f and A9: x = f . y by FUNCT_1:def_3; reconsider y = y as Element of I by A1, A5, A2, A6, A8, CARD_3:9; set X = the carrier' of S; set AS = ( the Sorts of (A . y) #) * the Arity of S; set Ar = the Arity of S; set Cr = the carrier of S; set So = the Sorts of (A . y); set a = the_arity_of o; A10: dom the Arity of S = the carrier' of S by FUNCT_2:def_1; then A11: dom (( the Sorts of (A . y) #) * the Arity of S) = dom the Arity of S by PARTFUN1:def_2; A12: Args (o,(A . y)) = (( the Sorts of (A . y) #) * the Arity of S) . o by MSUALG_1:def_4 .= ( the Sorts of (A . y) #) . ( the Arity of S . o) by A10, A11, FUNCT_1:12 .= ( the Sorts of (A . y) #) . (the_arity_of o) by MSUALG_1:def_1 .= product ( the Sorts of (A . y) * (the_arity_of o)) by FINSEQ_2:def_5 ; x in Args (o,(A . y)) by A7, A9; then consider g being Function such that A13: g = x and A14: dom g = dom ( the Sorts of (A . y) * (the_arity_of o)) and A15: for i being set st i in dom ( the Sorts of (A . y) * (the_arity_of o)) holds g . i in ( the Sorts of (A . y) * (the_arity_of o)) . i by A12, CARD_3:def_5; A16: ( rng (the_arity_of o) c= the carrier of S & dom the Sorts of (A . y) = the carrier of S ) by FINSEQ_1:def_4, PARTFUN1:def_2; then A17: dom ( the Sorts of (A . y) * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27; A18: rng g c= |.(A . y).| proof let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in rng g or i in |.(A . y).| ) assume i in rng g ; ::_thesis: i in |.(A . y).| then consider j being set such that A19: j in dom g and A20: g . j = i by FUNCT_1:def_3; (the_arity_of o) . j in rng (the_arity_of o) by A14, A17, A19, FUNCT_1:def_3; then A21: the Sorts of (A . y) . ((the_arity_of o) . j) in rng the Sorts of (A . y) by A16, FUNCT_1:def_3; i in ( the Sorts of (A . y) * (the_arity_of o)) . j by A14, A15, A19, A20; then i in the Sorts of (A . y) . ((the_arity_of o) . j) by A14, A19, FUNCT_1:12; hence i in |.(A . y).| by A21, TARSKI:def_4; ::_thesis: verum end; |.(A . y).| in { |.(A . i).| where i is Element of I : verum } ; then |.(A . y).| c= union { |.(A . i).| where i is Element of I : verum } by ZFMISC_1:74; then rng g c= |.A.| by A18, XBOOLE_1:1; hence x in Funcs ((dom (the_arity_of o)),|.A.|) by A13, A14, A17, FUNCT_2:def_2; ::_thesis: verum end; theorem Th11: :: PRALG_2:11 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 holds ( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = 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 o being OperSymbol of S holds ( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args (o,(A . i)) ) ) let S be non empty non void ManySortedSign ; ::_thesis: for A being MSAlgebra-Family of I,S for o being OperSymbol of S holds ( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args (o,(A . i)) ) ) let A be MSAlgebra-Family of I,S; ::_thesis: for o being OperSymbol of S holds ( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args (o,(A . i)) ) ) let o be OperSymbol of S; ::_thesis: ( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args (o,(A . i)) ) ) SubFuncs (rng (A ?. o)) = rng (A ?. o) proof thus SubFuncs (rng (A ?. o)) c= rng (A ?. o) by FUNCT_6:18; :: according to XBOOLE_0:def_10 ::_thesis: rng (A ?. o) c= SubFuncs (rng (A ?. o)) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (A ?. o) or x in SubFuncs (rng (A ?. o)) ) assume A1: x in rng (A ?. o) ; ::_thesis: x in SubFuncs (rng (A ?. o)) then ex j being set st ( j in dom (A ?. o) & x = (A ?. o) . j ) by FUNCT_1:def_3; hence x in SubFuncs (rng (A ?. o)) by A1, FUNCT_6:def_1; ::_thesis: verum end; then A2: (A ?. o) " (SubFuncs (rng (A ?. o))) = dom (A ?. o) by RELAT_1:134 .= I by PARTFUN1:def_2 ; A3: dom (A ?. o) = I by PARTFUN1:def_2; for i being Element of I holds (doms (A ?. o)) . i = Args (o,(A . i)) proof let i be Element of I; ::_thesis: (doms (A ?. o)) . i = Args (o,(A . i)) (A ?. o) . i = Den (o,(A . i)) by Th7; then (doms (A ?. o)) . i = dom (Den (o,(A . i))) by A3, FUNCT_6:22; hence (doms (A ?. o)) . i = Args (o,(A . i)) by FUNCT_2:def_1; ::_thesis: verum end; hence ( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args (o,(A . i)) ) ) by A2, FUNCT_6:def_2; ::_thesis: verum end; definition let I be set ; let S be non empty non void ManySortedSign ; let A be MSAlgebra-Family of I,S; func OPS A -> ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S means :: PRALG_2:def 13 for o being OperSymbol of S holds it . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) if I <> {} otherwise verum; existence ( ( I <> {} implies ex b1 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S st for o being OperSymbol of S holds b1 . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) & ( not I <> {} implies ex b1 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S st verum ) ) proof defpred S1[ set , set ] means for o being OperSymbol of S st $1 = o holds $2 = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))); set X = the carrier' of S; set AS = ((SORTS A) #) * the Arity of S; set RS = (SORTS A) * the ResultSort of S; A1: for x being set st x in the carrier' of S holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in the carrier' of S implies ex y being set st S1[x,y] ) assume x in the carrier' of S ; ::_thesis: ex y being set st S1[x,y] then reconsider o = x as OperSymbol of S ; take IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ; ::_thesis: S1[x, IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o))))] let o1 be OperSymbol of S; ::_thesis: ( x = o1 implies IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) = IFEQ ((the_arity_of o1),{},(commute (A ?. o1)),(Commute (Frege (A ?. o1)))) ) assume x = o1 ; ::_thesis: IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) = IFEQ ((the_arity_of o1),{},(commute (A ?. o1)),(Commute (Frege (A ?. o1)))) hence IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) = IFEQ ((the_arity_of o1),{},(commute (A ?. o1)),(Commute (Frege (A ?. o1)))) ; ::_thesis: verum end; consider f being Function such that A2: ( dom f = the carrier' of S & ( for x being set st x in the carrier' of S holds S1[x,f . x] ) ) from CLASSES1:sch_1(A1); reconsider f = f as ManySortedSet of the carrier' of S by A2, PARTFUN1:def_2, RELAT_1:def_18; for x being set st x in dom f holds f . x is Function proof let x be set ; ::_thesis: ( x in dom f implies f . x is Function ) assume x in dom f ; ::_thesis: f . x is Function then reconsider o = x as OperSymbol of S by A2; percases ( the_arity_of o = {} or the_arity_of o <> {} ) ; supposeA3: the_arity_of o = {} ; ::_thesis: f . x is Function f . x = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by A2 .= commute (A ?. o) by A3, FUNCOP_1:def_8 ; hence f . x is Function ; ::_thesis: verum end; supposeA4: the_arity_of o <> {} ; ::_thesis: f . x is Function f . x = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by A2 .= Commute (Frege (A ?. o)) by A4, FUNCOP_1:def_8 ; hence f . x is Function ; ::_thesis: verum end; end; end; then reconsider f = f as ManySortedFunction of the carrier' of S by FUNCOP_1:def_6; hereby ::_thesis: ( not I <> {} implies ex b1 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S st verum ) assume I <> {} ; ::_thesis: ex f being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S st for o being OperSymbol of S holds f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) then reconsider I9 = I as non empty set ; reconsider A9 = A as MSAlgebra-Family of I9,S ; for x being set st x in the carrier' of S holds f . x is Function of ((((SORTS A) #) * the Arity of S) . x),(((SORTS A) * the ResultSort of S) . x) proof let x be set ; ::_thesis: ( x in the carrier' of S implies f . x is Function of ((((SORTS A) #) * the Arity of S) . x),(((SORTS A) * the ResultSort of S) . x) ) assume x in the carrier' of S ; ::_thesis: f . x is Function of ((((SORTS A) #) * the Arity of S) . x),(((SORTS A) * the ResultSort of S) . x) then reconsider o = x as OperSymbol of S ; set ar = the_arity_of o; set C = Commute (Frege (A ?. o)); set F = Frege (A ?. o); set Ar = the Arity of S; set Rs = the ResultSort of S; set Cr = the carrier of S; set co = commute (A ?. o); A5: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4; A6: dom the Arity of S = the carrier' of S by FUNCT_2:def_1; then dom (((SORTS A) #) * the Arity of S) = dom the Arity of S by PARTFUN1:def_2; then A7: (((SORTS A) #) * the Arity of S) . o = ((SORTS A) #) . ( the Arity of S . o) by A6, FUNCT_1:12 .= ((SORTS A) #) . (the_arity_of o) by MSUALG_1:def_1 .= product ((SORTS A) * (the_arity_of o)) by FINSEQ_2:def_5 ; A8: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1; then dom ((SORTS A) * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def_2; then A9: ((SORTS A) * the ResultSort of S) . o = (SORTS A) . ( the ResultSort of S . o) by A8, FUNCT_1:12 .= (SORTS A) . (the_result_sort_of o) by MSUALG_1:def_2 .= product (Carrier (A,(the_result_sort_of o))) by Def10 ; dom (SORTS A) = the carrier of S by PARTFUN1:def_2; then A10: dom ((SORTS A) * (the_arity_of o)) = dom (the_arity_of o) by A5, RELAT_1:27; percases ( the_arity_of o = {} or the_arity_of o <> {} ) ; supposeA11: the_arity_of o = {} ; ::_thesis: f . x is Function of ((((SORTS A) #) * the Arity of S) . x),(((SORTS A) * the ResultSort of S) . x) set rs = the_result_sort_of o; A12: rng (A ?. o) c= Funcs ({{}},|.A9.|) proof let j be set ; :: according to TARSKI:def_3 ::_thesis: ( not j in rng (A ?. o) or j in Funcs ({{}},|.A9.|) ) assume j in rng (A ?. o) ; ::_thesis: j in Funcs ({{}},|.A9.|) then consider a being set such that A13: a in dom (A ?. o) and A14: (A ?. o) . a = j by FUNCT_1:def_3; reconsider i = a as Element of I9 by A13, PARTFUN1:def_2; set So = the Sorts of (A9 . i); |.(A9 . i).| in { |.(A9 . d).| where d is Element of I9 : verum } ; then A15: |.(A9 . i).| c= union { |.(A9 . d).| where d is Element of I9 : verum } by ZFMISC_1:74; dom the Sorts of (A9 . i) = the carrier of S by PARTFUN1:def_2; then the Sorts of (A9 . i) . (the_result_sort_of o) in rng the Sorts of (A9 . i) by FUNCT_1:def_3; then A16: the Sorts of (A9 . i) . (the_result_sort_of o) c= union (rng the Sorts of (A9 . i)) by ZFMISC_1:74; ( rng (Den (o,(A9 . i))) c= Result (o,(A9 . i)) & Result (o,(A9 . i)) = the Sorts of (A9 . i) . (the_result_sort_of o) ) by Th3, RELAT_1:def_19; then rng (Den (o,(A9 . i))) c= |.(A9 . i).| by A16, XBOOLE_1:1; then A17: rng (Den (o,(A9 . i))) c= |.A9.| by A15, XBOOLE_1:1; A18: ( dom (Den (o,(A9 . i))) = Args (o,(A9 . i)) & Args (o,(A9 . i)) = {{}} ) by A11, Th4, FUNCT_2:def_1; j = Den (o,(A9 . i)) by A14, Th7; hence j in Funcs ({{}},|.A9.|) by A18, A17, FUNCT_2:def_2; ::_thesis: verum end; dom (A ?. o) = I by PARTFUN1:def_2; then A19: A ?. o in Funcs (I,(Funcs ({{}},|.A9.|))) by A12, FUNCT_2:def_2; then commute (A ?. o) in Funcs ({{}},(Funcs (I,|.A9.|))) by FUNCT_6:55; then A20: ex h being Function st ( h = commute (A ?. o) & dom h = {{}} & rng h c= Funcs (I,|.A9.|) ) by FUNCT_2:def_2; A21: rng (commute (A ?. o)) c= ((SORTS A) * the ResultSort of S) . o proof let j be set ; :: according to TARSKI:def_3 ::_thesis: ( not j in rng (commute (A ?. o)) or j in ((SORTS A) * the ResultSort of S) . o ) A22: dom (Carrier (A,(the_result_sort_of o))) = I by PARTFUN1:def_2; assume A23: j in rng (commute (A ?. o)) ; ::_thesis: j in ((SORTS A) * the ResultSort of S) . o then consider a being set such that A24: a in dom (commute (A ?. o)) and A25: (commute (A ?. o)) . a = j by FUNCT_1:def_3; reconsider h = j as Function by A25; A26: for b being set st b in dom (Carrier (A,(the_result_sort_of o))) holds h . b in (Carrier (A,(the_result_sort_of o))) . b proof let b be set ; ::_thesis: ( b in dom (Carrier (A,(the_result_sort_of o))) implies h . b in (Carrier (A,(the_result_sort_of o))) . b ) assume b in dom (Carrier (A,(the_result_sort_of o))) ; ::_thesis: h . b in (Carrier (A,(the_result_sort_of o))) . b then reconsider i = b as Element of I9 by PARTFUN1:def_2; A27: ex U0 being MSAlgebra over S st ( U0 = A . i & (Carrier (A,(the_result_sort_of o))) . i = the Sorts of U0 . (the_result_sort_of o) ) by Def9; dom (Den (o,(A9 . i))) = Args (o,(A9 . i)) by FUNCT_2:def_1 .= {{}} by A11, Th4 ; then A28: (Den (o,(A9 . i))) . a in rng (Den (o,(A9 . i))) by A20, A24, FUNCT_1:def_3; (A ?. o) . i = Den (o,(A9 . i)) by Th7; then A29: (Den (o,(A9 . i))) . a = h . i by A19, A20, A24, A25, FUNCT_6:56; rng (Den (o,(A9 . i))) c= Result (o,(A9 . i)) by RELAT_1:def_19; then h . i in Result (o,(A9 . i)) by A29, A28; hence h . b in (Carrier (A,(the_result_sort_of o))) . b by A27, Th3; ::_thesis: verum end; ex k being Function st ( k = h & dom k = I & rng k c= |.A9.| ) by A20, A23, FUNCT_2:def_2; hence j in ((SORTS A) * the ResultSort of S) . o by A9, A22, A26, CARD_3:9; ::_thesis: verum end; A30: (((SORTS A) #) * the Arity of S) . o = {{}} by A7, A11, CARD_3:10; f . x = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by A2 .= commute (A ?. o) by A11, FUNCOP_1:def_8 ; hence f . x is Function of ((((SORTS A) #) * the Arity of S) . x),(((SORTS A) * the ResultSort of S) . x) by A30, A20, A21, FUNCT_2:2; ::_thesis: verum end; supposeA31: the_arity_of o <> {} ; ::_thesis: f . x is Function of ((((SORTS A) #) * the Arity of S) . x),(((SORTS A) * the ResultSort of S) . x) A32: dom (Commute (Frege (A ?. o))) = (((SORTS A) #) * the Arity of S) . o proof thus dom (Commute (Frege (A ?. o))) c= (((SORTS A) #) * the Arity of S) . o :: according to XBOOLE_0:def_10 ::_thesis: (((SORTS A) #) * the Arity of S) . o c= dom (Commute (Frege (A ?. o))) proof let j be set ; :: according to TARSKI:def_3 ::_thesis: ( not j in dom (Commute (Frege (A ?. o))) or j in (((SORTS A) #) * the Arity of S) . o ) assume j in dom (Commute (Frege (A ?. o))) ; ::_thesis: j in (((SORTS A) #) * the Arity of S) . o then consider g being Function such that A33: g in dom (Frege (A ?. o)) and A34: j = commute g by Def1; set cg = commute g; A35: rng g c= Funcs ((dom (the_arity_of o)),|.A9.|) by A33, Th10; A36: dom g = I9 by A33, Th10; then A37: g in Funcs (I,(Funcs ((dom (the_arity_of o)),|.A9.|))) by A35, FUNCT_2:def_2; then commute g in Funcs ((dom (the_arity_of o)),(Funcs (I,|.A9.|))) by A31, FUNCT_6:55; then A38: ex h being Function st ( h = commute g & dom h = dom (the_arity_of o) & rng h c= Funcs (I,|.A9.|) ) by FUNCT_2:def_2; for y being set st y in dom ((SORTS A) * (the_arity_of o)) holds (commute g) . y in ((SORTS A) * (the_arity_of o)) . y proof let y be set ; ::_thesis: ( y in dom ((SORTS A) * (the_arity_of o)) implies (commute g) . y in ((SORTS A) * (the_arity_of o)) . y ) assume A39: y in dom ((SORTS A) * (the_arity_of o)) ; ::_thesis: (commute g) . y in ((SORTS A) * (the_arity_of o)) . y then (the_arity_of o) . y in rng (the_arity_of o) by A10, FUNCT_1:def_3; then reconsider s = (the_arity_of o) . y as SortSymbol of S by A5; (commute g) . y in rng (commute g) by A10, A38, A39, FUNCT_1:def_3; then consider h being Function such that A40: h = (commute g) . y and A41: dom h = I and rng h c= |.A9.| by A38, FUNCT_2:def_2; A42: for z being set st z in dom (Carrier (A,s)) holds h . z in (Carrier (A,s)) . z proof let z be set ; ::_thesis: ( z in dom (Carrier (A,s)) implies h . z in (Carrier (A,s)) . z ) assume z in dom (Carrier (A,s)) ; ::_thesis: h . z in (Carrier (A,s)) . z then reconsider i = z as Element of I9 by PARTFUN1:def_2; A43: dom (( the Sorts of (A9 . i) #) * the Arity of S) = the carrier' of S by PARTFUN1:def_2; A44: Args (o,(A9 . i)) = (( the Sorts of (A9 . i) #) * the Arity of S) . o by MSUALG_1:def_4 .= ( the Sorts of (A9 . i) #) . ( the Arity of S . o) by A43, FUNCT_1:12 .= ( the Sorts of (A9 . i) #) . (the_arity_of o) by MSUALG_1:def_1 .= product ( the Sorts of (A9 . i) * (the_arity_of o)) by FINSEQ_2:def_5 ; g . i in rng g by A36, FUNCT_1:def_3; then consider f being Function such that A45: f = g . i and dom f = dom (the_arity_of o) and rng f c= |.A9.| by A35, FUNCT_2:def_2; A46: ex U0 being MSAlgebra over S st ( U0 = A . i & (Carrier (A,s)) . i = the Sorts of U0 . s ) by Def9; dom the Sorts of (A9 . i) = the carrier of S by PARTFUN1:def_2; then A47: dom ( the Sorts of (A9 . i) * (the_arity_of o)) = dom (the_arity_of o) by A5, RELAT_1:27; then A48: ( the Sorts of (A9 . i) * (the_arity_of o)) . y = the Sorts of (A9 . i) . s by A10, A39, FUNCT_1:12; g . i in Args (o,(A9 . i)) by A33, Th10; then f . y in ( the Sorts of (A9 . i) * (the_arity_of o)) . y by A10, A39, A45, A44, A47, CARD_3:9; hence h . z in (Carrier (A,s)) . z by A10, A37, A39, A40, A46, A45, A48, FUNCT_6:56; ::_thesis: verum end; A49: dom (Carrier (A,s)) = I by PARTFUN1:def_2; ((SORTS A) * (the_arity_of o)) . y = (SORTS A) . s by A39, FUNCT_1:12 .= product (Carrier (A,s)) by Def10 ; hence (commute g) . y in ((SORTS A) * (the_arity_of o)) . y by A49, A40, A41, A42, CARD_3:9; ::_thesis: verum end; hence j in (((SORTS A) #) * the Arity of S) . o by A7, A10, A34, A38, CARD_3:9; ::_thesis: verum end; let i be set ; :: according to TARSKI:def_3 ::_thesis: ( not i in (((SORTS A) #) * the Arity of S) . o or i in dom (Commute (Frege (A ?. o))) ) assume i in (((SORTS A) #) * the Arity of S) . o ; ::_thesis: i in dom (Commute (Frege (A ?. o))) then consider g being Function such that A50: g = i and A51: dom g = dom ((SORTS A) * (the_arity_of o)) and A52: for x being set st x in dom ((SORTS A) * (the_arity_of o)) holds g . x in ((SORTS A) * (the_arity_of o)) . x by A7, CARD_3:def_5; A53: rng g c= Funcs (I,|.A9.|) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng g or a in Funcs (I,|.A9.|) ) assume a in rng g ; ::_thesis: a in Funcs (I,|.A9.|) then consider b being set such that A54: b in dom g and A55: g . b = a by FUNCT_1:def_3; (the_arity_of o) . b in rng (the_arity_of o) by A10, A51, A54, FUNCT_1:def_3; then reconsider cr = (the_arity_of o) . b as SortSymbol of S by A5; A56: ((SORTS A) * (the_arity_of o)) . b = (SORTS A) . cr by A51, A54, FUNCT_1:12 .= product (Carrier (A,cr)) by Def10 ; a in ((SORTS A) * (the_arity_of o)) . b by A51, A52, A54, A55; then consider h being Function such that A57: h = a and A58: dom h = dom (Carrier (A,cr)) and A59: for j being set st j in dom (Carrier (A,cr)) holds h . j in (Carrier (A,cr)) . j by A56, CARD_3:def_5; A60: rng h c= |.A9.| proof let j be set ; :: according to TARSKI:def_3 ::_thesis: ( not j in rng h or j in |.A9.| ) assume j in rng h ; ::_thesis: j in |.A9.| then consider c being set such that A61: c in dom h and A62: h . c = j by FUNCT_1:def_3; reconsider i = c as Element of I9 by A58, A61, PARTFUN1:def_2; ( ex U0 being MSAlgebra over S st ( U0 = A . i & (Carrier (A,cr)) . i = the Sorts of U0 . cr ) & dom the Sorts of (A9 . i) = the carrier of S ) by Def9, PARTFUN1:def_2; then A63: (Carrier (A,cr)) . i in rng the Sorts of (A9 . i) by FUNCT_1:def_3; h . i in (Carrier (A,cr)) . i by A58, A59, A61; then A64: h . i in |.(A9 . i).| by A63, TARSKI:def_4; |.(A9 . i).| in { |.(A9 . d).| where d is Element of I9 : verum } ; hence j in |.A9.| by A62, A64, TARSKI:def_4; ::_thesis: verum end; dom (Carrier (A,cr)) = I by PARTFUN1:def_2; hence a in Funcs (I,|.A9.|) by A57, A58, A60, FUNCT_2:def_2; ::_thesis: verum end; then A65: g in Funcs ((dom (the_arity_of o)),(Funcs (I,|.A9.|))) by A10, A51, FUNCT_2:def_2; then A66: commute (commute g) = g by A31, FUNCT_6:57; commute g in Funcs (I,(Funcs ((dom (the_arity_of o)),|.A9.|))) by A31, A65, FUNCT_6:55; then A67: ex h being Function st ( h = commute g & dom h = I & rng h c= Funcs ((dom (the_arity_of o)),|.A9.|) ) by FUNCT_2:def_2; A68: for j being set st j in dom (doms (A ?. o)) holds (commute g) . j in (doms (A ?. o)) . j proof set cg = commute g; let j be set ; ::_thesis: ( j in dom (doms (A ?. o)) implies (commute g) . j in (doms (A ?. o)) . j ) assume j in dom (doms (A ?. o)) ; ::_thesis: (commute g) . j in (doms (A ?. o)) . j then reconsider ii = j as Element of I9 by Th11; set So = the Sorts of (A9 . ii); reconsider h = (commute g) . ii as Function ; h in rng (commute g) by A67, FUNCT_1:def_3; then A69: ex s being Function st ( s = h & dom s = dom (the_arity_of o) & rng s c= |.A9.| ) by A67, FUNCT_2:def_2; A70: dom ( the Sorts of (A9 . ii) * (the_arity_of o)) = dom (the_arity_of o) by Th3; A71: for a being set st a in dom ( the Sorts of (A9 . ii) * (the_arity_of o)) holds h . a in ( the Sorts of (A9 . ii) * (the_arity_of o)) . a proof let a be set ; ::_thesis: ( a in dom ( the Sorts of (A9 . ii) * (the_arity_of o)) implies h . a in ( the Sorts of (A9 . ii) * (the_arity_of o)) . a ) assume A72: a in dom ( the Sorts of (A9 . ii) * (the_arity_of o)) ; ::_thesis: h . a in ( the Sorts of (A9 . ii) * (the_arity_of o)) . a then (the_arity_of o) . a in rng (the_arity_of o) by A70, FUNCT_1:def_3; then reconsider s = (the_arity_of o) . a as SortSymbol of S by A5; A73: ( the Sorts of (A9 . ii) * (the_arity_of o)) . a = the Sorts of (A9 . ii) . s by A72, FUNCT_1:12; g . a in rng g by A10, A51, A70, A72, FUNCT_1:def_3; then consider k being Function such that A74: k = g . a and dom k = I and rng k c= |.A9.| by A53, FUNCT_2:def_2; A75: ( ex U0 being MSAlgebra over S st ( U0 = A9 . ii & (Carrier (A,s)) . ii = the Sorts of U0 . s ) & dom (Carrier (A,s)) = I ) by Def9, PARTFUN1:def_2; A76: ((SORTS A) * (the_arity_of o)) . a = (SORTS A) . s by A10, A70, A72, FUNCT_1:12 .= product (Carrier (A,s)) by Def10 ; ( k . ii = h . a & k in ((SORTS A) * (the_arity_of o)) . a ) by A10, A52, A65, A70, A72, A74, FUNCT_6:56; hence h . a in ( the Sorts of (A9 . ii) * (the_arity_of o)) . a by A73, A76, A75, CARD_3:9; ::_thesis: verum end; ( (doms (A ?. o)) . ii = Args (o,(A9 . ii)) & Args (o,(A9 . ii)) = product ( the Sorts of (A9 . ii) * (the_arity_of o)) ) by Th3, Th11; hence (commute g) . j in (doms (A ?. o)) . j by A70, A69, A71, CARD_3:9; ::_thesis: verum end; ( dom (Frege (A ?. o)) = product (doms (A ?. o)) & dom (doms (A ?. o)) = I9 ) by Th11, PARTFUN1:def_2; then commute g in dom (Frege (A ?. o)) by A67, A68, CARD_3:9; hence i in dom (Commute (Frege (A ?. o))) by A50, A66, Def1; ::_thesis: verum end; set rs = the_result_sort_of o; set CA = Carrier (A,(the_result_sort_of o)); A77: rng (Commute (Frege (A ?. o))) c= ((SORTS A) * the ResultSort of S) . o proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (Commute (Frege (A ?. o))) or x in ((SORTS A) * the ResultSort of S) . o ) A78: dom (Carrier (A,(the_result_sort_of o))) = I by PARTFUN1:def_2; assume x in rng (Commute (Frege (A ?. o))) ; ::_thesis: x in ((SORTS A) * the ResultSort of S) . o then consider g being set such that A79: g in dom (Commute (Frege (A ?. o))) and A80: (Commute (Frege (A ?. o))) . g = x by FUNCT_1:def_3; consider f being Function such that A81: f in dom (Frege (A ?. o)) and A82: g = commute f by A79, Def1; reconsider g = g as Function by A82; ( dom f = I9 & rng f c= Funcs ((dom (the_arity_of o)),|.A9.|) ) by A81, Th10; then f in Funcs (I,(Funcs ((dom (the_arity_of o)),|.A9.|))) by FUNCT_2:def_2; then commute g = f by A31, A82, FUNCT_6:57; then A83: x = (Frege (A ?. o)) . f by A79, A80, Def1; then reconsider h = x as Function ; A84: (Frege (A ?. o)) . f in rng (Frege (A ?. o)) by A81, FUNCT_1:def_3; A85: for j being set st j in dom (Carrier (A,(the_result_sort_of o))) holds h . j in (Carrier (A,(the_result_sort_of o))) . j proof let j be set ; ::_thesis: ( j in dom (Carrier (A,(the_result_sort_of o))) implies h . j in (Carrier (A,(the_result_sort_of o))) . j ) assume j in dom (Carrier (A,(the_result_sort_of o))) ; ::_thesis: h . j in (Carrier (A,(the_result_sort_of o))) . j then reconsider i = j as Element of I9 by PARTFUN1:def_2; A86: dom ( the Sorts of (A9 . i) * the ResultSort of S) = dom the ResultSort of S by A8, PARTFUN1:def_2; A87: ex U0 being MSAlgebra over S st ( U0 = A9 . i & (Carrier (A,(the_result_sort_of o))) . i = the Sorts of U0 . (the_result_sort_of o) ) by Def9; Result (o,(A9 . i)) = ( the Sorts of (A9 . i) * the ResultSort of S) . o by MSUALG_1:def_5 .= the Sorts of (A9 . i) . ( the ResultSort of S . o) by A8, A86, FUNCT_1:12 .= (Carrier (A,(the_result_sort_of o))) . i by A87, MSUALG_1:def_2 ; hence h . j in (Carrier (A,(the_result_sort_of o))) . j by A83, A84, Th9; ::_thesis: verum end; dom h = I9 by A83, A84, Th9; hence x in ((SORTS A) * the ResultSort of S) . o by A9, A78, A85, CARD_3:9; ::_thesis: verum end; f . x = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by A2 .= Commute (Frege (A ?. o)) by A31, FUNCOP_1:def_8 ; hence f . x is Function of ((((SORTS A) #) * the Arity of S) . x),(((SORTS A) * the ResultSort of S) . x) by A32, A77, FUNCT_2:2; ::_thesis: verum end; end; end; then reconsider f = f as ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S by PBOOLE:def_15; take f = f; ::_thesis: for o being OperSymbol of S holds f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) let o be OperSymbol of S; ::_thesis: f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) thus f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by A2; ::_thesis: verum end; assume I = {} ; ::_thesis: ex b1 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S st verum set f = the ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S; take the ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S ; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S holds ( ( I <> {} & ( for o being OperSymbol of S holds b1 . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) & ( for o being OperSymbol of S holds b2 . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) implies b1 = b2 ) & ( not I <> {} implies b1 = b2 ) ) proof let f, g be ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S; ::_thesis: ( ( I <> {} & ( for o being OperSymbol of S holds f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) & ( for o being OperSymbol of S holds g . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) implies f = g ) & ( not I <> {} implies f = g ) ) hereby ::_thesis: ( not I <> {} implies f = g ) assume I <> {} ; ::_thesis: ( ( for o being OperSymbol of S holds f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) & ( for o being OperSymbol of S holds g . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) implies f = g ) assume that A88: for o being OperSymbol of S holds f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) and A89: for o being OperSymbol of S holds g . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ; ::_thesis: f = g for i being set st i in the carrier' of S holds f . i = g . i proof let i be set ; ::_thesis: ( i in the carrier' of S implies f . i = g . i ) assume i in the carrier' of S ; ::_thesis: f . i = g . i then reconsider o = i as Element of the carrier' of S ; f . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) by A88; hence f . i = g . i by A89; ::_thesis: verum end; hence f = g by PBOOLE:3; ::_thesis: verum end; assume A90: I = {} ; ::_thesis: f = g A91: now__::_thesis:_for_o_being_set_st_o_in_the_carrier'_of_S_holds_ f_._o_=_g_._o let o be set ; ::_thesis: ( o in the carrier' of S implies f . o = g . o ) assume A92: o in the carrier' of S ; ::_thesis: f . o = g . o then reconsider s = the ResultSort of S . o as SortSymbol of S by FUNCT_2:5; o in dom the ResultSort of S by A92, FUNCT_2:def_1; then A93: ((SORTS A) * the ResultSort of S) . o = (SORTS A) . s by FUNCT_1:13 .= product (Carrier (A,s)) by Def10 .= {{}} by A90, CARD_3:10 ; ( f . o is Function of ((((SORTS A) #) * the Arity of S) . o),(((SORTS A) * the ResultSort of S) . o) & g . o is Function of ((((SORTS A) #) * the Arity of S) . o),(((SORTS A) * the ResultSort of S) . o) ) by A92, PBOOLE:def_15; hence f . o = g . o by A93, FUNCT_2:51; ::_thesis: verum end; ( dom f = the carrier' of S & dom g = the carrier' of S ) by PARTFUN1:def_2; hence f = g by A91, FUNCT_1:2; ::_thesis: verum end; correctness consistency for b1 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S holds verum; ; end; :: deftheorem defines OPS PRALG_2:def_13_:_ for I being set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S for b4 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S holds ( ( I <> {} implies ( b4 = OPS A iff for o being OperSymbol of S holds b4 . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) ) & ( not I <> {} implies ( b4 = OPS A iff verum ) ) ); definition let I be set ; let S be non empty non void ManySortedSign ; let A be MSAlgebra-Family of I,S; func product A -> MSAlgebra over S equals :: PRALG_2:def 14 MSAlgebra(# (SORTS A),(OPS A) #); coherence MSAlgebra(# (SORTS A),(OPS A) #) is MSAlgebra over S ; end; :: deftheorem defines product PRALG_2:def_14_:_ for I being set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S holds product A = MSAlgebra(# (SORTS A),(OPS A) #); registration let I be set ; let S be non empty non void ManySortedSign ; let A be MSAlgebra-Family of I,S; cluster product A -> strict ; coherence product A is strict ; end; theorem :: PRALG_2:12 for I being set for S being non empty non void ManySortedSign for A being MSAlgebra-Family of I,S holds ( the Sorts of (product A) = SORTS A & the Charact of (product A) = OPS A ) ;