:: PRALG_1 semantic presentation begin definition let A, B be non empty set ; let h1 be FinSequence of [:A,B:]; :: original: pr1 redefine func pr1 h1 -> FinSequence of A means :Def1: :: PRALG_1:def 1 ( len it = len h1 & ( for n being Nat st n in dom it holds it . n = (h1 . n) `1 ) ); compatibility for b1 being FinSequence of A holds ( b1 = pr1 h1 iff ( len b1 = len h1 & ( for n being Nat st n in dom b1 holds b1 . n = (h1 . n) `1 ) ) ) proof let f1 be FinSequence of A; ::_thesis: ( f1 = pr1 h1 iff ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds f1 . n = (h1 . n) `1 ) ) ) hereby ::_thesis: ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds f1 . n = (h1 . n) `1 ) implies f1 = pr1 h1 ) assume A1: f1 = pr1 h1 ; ::_thesis: ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds f1 . n = (h1 . n) `1 ) ) then A2: dom f1 = dom h1 by MCART_1:def_12; hence len f1 = len h1 by FINSEQ_3:29; ::_thesis: for n being Nat st n in dom f1 holds f1 . n = (h1 . n) `1 let n be Nat; ::_thesis: ( n in dom f1 implies f1 . n = (h1 . n) `1 ) thus ( n in dom f1 implies f1 . n = (h1 . n) `1 ) by A1, A2, MCART_1:def_12; ::_thesis: verum end; assume ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds f1 . n = (h1 . n) `1 ) ) ; ::_thesis: f1 = pr1 h1 then ( dom f1 = dom h1 & ( for n being set st n in dom f1 holds f1 . n = (h1 . n) `1 ) ) by FINSEQ_3:29; hence f1 = pr1 h1 by MCART_1:def_12; ::_thesis: verum end; coherence pr1 h1 is FinSequence of A proof thus pr1 h1 is FinSequence of A ; ::_thesis: verum end; :: original: pr2 redefine func pr2 h1 -> FinSequence of B means :Def2: :: PRALG_1:def 2 ( len it = len h1 & ( for n being Nat st n in dom it holds it . n = (h1 . n) `2 ) ); compatibility for b1 being FinSequence of B holds ( b1 = pr2 h1 iff ( len b1 = len h1 & ( for n being Nat st n in dom b1 holds b1 . n = (h1 . n) `2 ) ) ) proof let f1 be FinSequence of B; ::_thesis: ( f1 = pr2 h1 iff ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds f1 . n = (h1 . n) `2 ) ) ) hereby ::_thesis: ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds f1 . n = (h1 . n) `2 ) implies f1 = pr2 h1 ) assume A3: f1 = pr2 h1 ; ::_thesis: ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds f1 . n = (h1 . n) `2 ) ) then A4: dom f1 = dom h1 by MCART_1:def_13; hence len f1 = len h1 by FINSEQ_3:29; ::_thesis: for n being Nat st n in dom f1 holds f1 . n = (h1 . n) `2 let n be Nat; ::_thesis: ( n in dom f1 implies f1 . n = (h1 . n) `2 ) thus ( n in dom f1 implies f1 . n = (h1 . n) `2 ) by A3, A4, MCART_1:def_13; ::_thesis: verum end; assume ( len f1 = len h1 & ( for n being Nat st n in dom f1 holds f1 . n = (h1 . n) `2 ) ) ; ::_thesis: f1 = pr2 h1 then ( dom f1 = dom h1 & ( for n being set st n in dom f1 holds f1 . n = (h1 . n) `2 ) ) by FINSEQ_3:29; hence f1 = pr2 h1 by MCART_1:def_13; ::_thesis: verum end; coherence pr2 h1 is FinSequence of B proof thus pr2 h1 is FinSequence of B ; ::_thesis: verum end; end; :: deftheorem Def1 defines pr1 PRALG_1:def_1_:_ for A, B being non empty set for h1 being FinSequence of [:A,B:] for b4 being FinSequence of A holds ( b4 = pr1 h1 iff ( len b4 = len h1 & ( for n being Nat st n in dom b4 holds b4 . n = (h1 . n) `1 ) ) ); :: deftheorem Def2 defines pr2 PRALG_1:def_2_:_ for A, B being non empty set for h1 being FinSequence of [:A,B:] for b4 being FinSequence of B holds ( b4 = pr2 h1 iff ( len b4 = len h1 & ( for n being Nat st n in dom b4 holds b4 . n = (h1 . n) `2 ) ) ); definition let A, B be non empty set ; let f1 be non empty homogeneous quasi_total PartFunc of (A *),A; let f2 be non empty homogeneous quasi_total PartFunc of (B *),B; assume A1: arity f1 = arity f2 ; func[[:f1,f2:]] -> non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] means :Def3: :: PRALG_1:def 3 ( dom it = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom it holds it . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) ); existence ex b1 being non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] st ( dom b1 = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b1 holds b1 . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) ) proof set ar = (arity f1) -tuples_on [:A,B:]; set ab = { s where s is Element of [:A,B:] * : len s = arity f1 } ; defpred S1[ set , set ] means for h being FinSequence of [:A,B:] st $1 = h holds $2 = [(f1 . (pr1 h)),(f2 . (pr2 h))]; A2: dom f2 = (arity f2) -tuples_on B by MARGREL1:22; A3: ( rng f1 c= A & rng f2 c= B ) by RELAT_1:def_19; A4: dom f1 = (arity f1) -tuples_on A by MARGREL1:22; A5: for x, y being set st x in (arity f1) -tuples_on [:A,B:] & S1[x,y] holds y in [:A,B:] proof let x, y be set ; ::_thesis: ( x in (arity f1) -tuples_on [:A,B:] & S1[x,y] implies y in [:A,B:] ) assume that A6: x in (arity f1) -tuples_on [:A,B:] and A7: S1[x,y] ; ::_thesis: y in [:A,B:] consider s being Element of [:A,B:] * such that A8: x = s and A9: len s = arity f1 by A6; reconsider s1 = pr1 s as Element of A * by FINSEQ_1:def_11; len (pr1 s) = len s by Def1; then s1 in { s3 where s3 is Element of A * : len s3 = arity f1 } by A9; then A10: f1 . s1 in rng f1 by A4, FUNCT_1:def_3; reconsider s2 = pr2 s as Element of B * by FINSEQ_1:def_11; len (pr2 s) = len s by Def2; then s2 in { s3 where s3 is Element of B * : len s3 = arity f2 } by A1, A9; then A11: f2 . s2 in rng f2 by A2, FUNCT_1:def_3; y = [(f1 . (pr1 s)),(f2 . (pr2 s))] by A7, A8; hence y in [:A,B:] by A3, A10, A11, ZFMISC_1:87; ::_thesis: verum end; A12: for x, y, z being set st x in (arity f1) -tuples_on [:A,B:] & S1[x,y] & S1[x,z] holds y = z proof let x, y, z be set ; ::_thesis: ( x in (arity f1) -tuples_on [:A,B:] & S1[x,y] & S1[x,z] implies y = z ) assume that A13: x in (arity f1) -tuples_on [:A,B:] and A14: S1[x,y] and A15: S1[x,z] ; ::_thesis: y = z consider s being Element of [:A,B:] * such that A16: x = s and len s = arity f1 by A13; y = [(f1 . (pr1 s)),(f2 . (pr2 s))] by A14, A16; hence y = z by A15, A16; ::_thesis: verum end; consider f being PartFunc of ((arity f1) -tuples_on [:A,B:]),[:A,B:] such that A17: for x being set holds ( x in dom f iff ( x in (arity f1) -tuples_on [:A,B:] & ex y being set st S1[x,y] ) ) and A18: for x being set st x in dom f holds S1[x,f . x] from PARTFUN1:sch_2(A5, A12); A19: dom f = (arity f1) -tuples_on [:A,B:] proof thus dom f c= (arity f1) -tuples_on [:A,B:] :: according to XBOOLE_0:def_10 ::_thesis: (arity f1) -tuples_on [:A,B:] c= dom f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in (arity f1) -tuples_on [:A,B:] ) assume x in dom f ; ::_thesis: x in (arity f1) -tuples_on [:A,B:] hence x in (arity f1) -tuples_on [:A,B:] by A17; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (arity f1) -tuples_on [:A,B:] or x in dom f ) assume A20: x in (arity f1) -tuples_on [:A,B:] ; ::_thesis: x in dom f then consider s being Element of [:A,B:] * such that A21: x = s and len s = arity f1 ; now__::_thesis:_ex_y_being_set_st_ for_h_being_FinSequence_of_[:A,B:]_st_h_=_x_holds_ y_=_[(f1_._(pr1_h)),(f2_._(pr2_h))] take y = [(f1 . (pr1 s)),(f2 . (pr2 s))]; ::_thesis: for h being FinSequence of [:A,B:] st h = x holds y = [(f1 . (pr1 h)),(f2 . (pr2 h))] let h be FinSequence of [:A,B:]; ::_thesis: ( h = x implies y = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) assume h = x ; ::_thesis: y = [(f1 . (pr1 h)),(f2 . (pr2 h))] hence y = [(f1 . (pr1 h)),(f2 . (pr2 h))] by A21; ::_thesis: verum end; hence x in dom f by A17, A20; ::_thesis: verum end; (arity f1) -tuples_on [:A,B:] in { (i -tuples_on [:A,B:]) where i is Element of NAT : verum } ; then (arity f1) -tuples_on [:A,B:] c= union { (i -tuples_on [:A,B:]) where i is Element of NAT : verum } by ZFMISC_1:74; then (arity f1) -tuples_on [:A,B:] c= [:A,B:] * by FINSEQ_2:108; then reconsider f = f as PartFunc of ([:A,B:] *),[:A,B:] by RELSET_1:7; A22: f is quasi_total proof let x, y be FinSequence of [:A,B:]; :: according to MARGREL1:def_22 ::_thesis: ( not len x = len y or not x in proj1 f or y in proj1 f ) assume that A23: len x = len y and A24: x in dom f ; ::_thesis: y in proj1 f reconsider y9 = y as Element of [:A,B:] * by FINSEQ_1:def_11; ex s1 being Element of [:A,B:] * st ( s1 = x & len s1 = arity f1 ) by A19, A24; then y9 in { s where s is Element of [:A,B:] * : len s = arity f1 } by A23; hence y in proj1 f by A19; ::_thesis: verum end; f is homogeneous proof let x, y be FinSequence; :: according to MARGREL1:def_1,MARGREL1:def_21 ::_thesis: ( not x in proj1 f or not y in proj1 f or len x = len y ) assume ( x in dom f & y in dom f ) ; ::_thesis: len x = len y then ( ex s1 being Element of [:A,B:] * st ( s1 = x & len s1 = arity f1 ) & ex s2 being Element of [:A,B:] * st ( s2 = y & len s2 = arity f1 ) ) by A19; hence len x = len y ; ::_thesis: verum end; then reconsider f = f as non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] by A19, A22; take f ; ::_thesis: ( dom f = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom f holds f . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) ) thus dom f = (arity f1) -tuples_on [:A,B:] by A19; ::_thesis: for h being FinSequence of [:A,B:] st h in dom f holds f . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] let h be FinSequence of [:A,B:]; ::_thesis: ( h in dom f implies f . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) assume h in dom f ; ::_thesis: f . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] hence f . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] by A18; ::_thesis: verum end; uniqueness for b1, b2 being non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] st dom b1 = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b1 holds b1 . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) & dom b2 = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b2 holds b2 . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) holds b1 = b2 proof let x, y be non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:]; ::_thesis: ( dom x = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom x holds x . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) & dom y = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom y holds y . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) implies x = y ) assume that A25: dom x = (arity f1) -tuples_on [:A,B:] and A26: for h being FinSequence of [:A,B:] st h in dom x holds x . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] and A27: dom y = (arity f1) -tuples_on [:A,B:] and A28: for h being FinSequence of [:A,B:] st h in dom y holds y . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ; ::_thesis: x = y now__::_thesis:_for_c_being_Element_of_[:A,B:]_*_st_c_in_dom_x_holds_ x_._c_=_y_._c let c be Element of [:A,B:] * ; ::_thesis: ( c in dom x implies x . c = y . c ) reconsider c9 = c as FinSequence of [:A,B:] ; assume A29: c in dom x ; ::_thesis: x . c = y . c then x . c9 = [(f1 . (pr1 c9)),(f2 . (pr2 c9))] by A26; hence x . c = y . c by A25, A27, A28, A29; ::_thesis: verum end; hence x = y by A25, A27, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem Def3 defines [[: PRALG_1:def_3_:_ for A, B being non empty set for f1 being non empty homogeneous quasi_total PartFunc of (A *),A for f2 being non empty homogeneous quasi_total PartFunc of (B *),B st arity f1 = arity f2 holds for b5 being non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] holds ( b5 = [[:f1,f2:]] iff ( dom b5 = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b5 holds b5 . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) ) ); definition let U1, U2 be Universal_Algebra; assume A1: U1,U2 are_similar ; func Opers (U1,U2) -> PFuncFinSequence of [: the carrier of U1, the carrier of U2:] means :Def4: :: PRALG_1:def 4 ( len it = len the charact of U1 & ( for n being Nat st n in dom it holds for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds it . n = [[:h1,h2:]] ) ); existence ex b1 being PFuncFinSequence of [: the carrier of U1, the carrier of U2:] st ( len b1 = len the charact of U1 & ( for n being Nat st n in dom b1 holds for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds b1 . n = [[:h1,h2:]] ) ) proof defpred S1[ Nat, set ] means for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . $1 & h2 = the charact of U2 . $1 holds $2 = [[:h1,h2:]]; set l = len the charact of U1; set c = [: the carrier of U1, the carrier of U2:]; A2: dom the charact of U2 = Seg (len the charact of U2) by FINSEQ_1:def_3; A3: Seg (len the charact of U1) = dom the charact of U1 by FINSEQ_1:def_3; A4: for m being Nat st m in Seg (len the charact of U1) holds ex x being Element of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) st S1[m,x] proof let m be Nat; ::_thesis: ( m in Seg (len the charact of U1) implies ex x being Element of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) st S1[m,x] ) assume A5: m in Seg (len the charact of U1) ; ::_thesis: ex x being Element of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) st S1[m,x] then reconsider f1 = the charact of U1 . m as non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 by A3, MARGREL1:def_24, UNIALG_1:1; len the charact of U1 = len the charact of U2 by A1, UNIALG_2:1; then reconsider f2 = the charact of U2 . m as non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 by A2, A5, MARGREL1:def_24, UNIALG_1:1; reconsider F = [[:f1,f2:]] as Element of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) by PARTFUN1:45; take F ; ::_thesis: S1[m,F] let h1 be non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1; ::_thesis: for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . m & h2 = the charact of U2 . m holds F = [[:h1,h2:]] let h2 be non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2; ::_thesis: ( h1 = the charact of U1 . m & h2 = the charact of U2 . m implies F = [[:h1,h2:]] ) assume ( h1 = the charact of U1 . m & h2 = the charact of U2 . m ) ; ::_thesis: F = [[:h1,h2:]] hence F = [[:h1,h2:]] ; ::_thesis: verum end; consider p being FinSequence of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) such that A6: dom p = Seg (len the charact of U1) and A7: for m being Nat st m in Seg (len the charact of U1) holds S1[m,p . m] from FINSEQ_1:sch_5(A4); reconsider p = p as PFuncFinSequence of [: the carrier of U1, the carrier of U2:] ; take p ; ::_thesis: ( len p = len the charact of U1 & ( for n being Nat st n in dom p holds for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds p . n = [[:h1,h2:]] ) ) thus len p = len the charact of U1 by A6, FINSEQ_1:def_3; ::_thesis: for n being Nat st n in dom p holds for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds p . n = [[:h1,h2:]] let n be Nat; ::_thesis: ( n in dom p implies for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds p . n = [[:h1,h2:]] ) assume n in dom p ; ::_thesis: for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds p . n = [[:h1,h2:]] hence for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds p . n = [[:h1,h2:]] by A6, A7; ::_thesis: verum end; uniqueness for b1, b2 being PFuncFinSequence of [: the carrier of U1, the carrier of U2:] st len b1 = len the charact of U1 & ( for n being Nat st n in dom b1 holds for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds b1 . n = [[:h1,h2:]] ) & len b2 = len the charact of U1 & ( for n being Nat st n in dom b2 holds for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds b2 . n = [[:h1,h2:]] ) holds b1 = b2 proof let x, y be PFuncFinSequence of [: the carrier of U1, the carrier of U2:]; ::_thesis: ( len x = len the charact of U1 & ( for n being Nat st n in dom x holds for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds x . n = [[:h1,h2:]] ) & len y = len the charact of U1 & ( for n being Nat st n in dom y holds for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds y . n = [[:h1,h2:]] ) implies x = y ) assume that A8: len x = len the charact of U1 and A9: for n being Nat st n in dom x holds for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds x . n = [[:h1,h2:]] and A10: len y = len the charact of U1 and A11: for n being Nat st n in dom y holds for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds y . n = [[:h1,h2:]] ; ::_thesis: x = y A12: dom x = Seg (len the charact of U1) by A8, FINSEQ_1:def_3; now__::_thesis:_for_m_being_Nat_st_m_in_dom_x_holds_ x_._m_=_y_._m let m be Nat; ::_thesis: ( m in dom x implies x . m = y . m ) assume A13: m in dom x ; ::_thesis: x . m = y . m then m in dom the charact of U1 by A12, FINSEQ_1:def_3; then reconsider h1 = the charact of U1 . m as non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 by MARGREL1:def_24, UNIALG_1:1; Seg (len the charact of U2) = Seg (len the charact of U1) by A1, UNIALG_2:1; then m in dom the charact of U2 by A12, A13, FINSEQ_1:def_3; then reconsider h2 = the charact of U2 . m as non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 by MARGREL1:def_24, UNIALG_1:1; ( m in dom y & x . m = [[:h1,h2:]] ) by A9, A10, A12, A13, FINSEQ_1:def_3; hence x . m = y . m by A11; ::_thesis: verum end; hence x = y by A8, A10, FINSEQ_2:9; ::_thesis: verum end; end; :: deftheorem Def4 defines Opers PRALG_1:def_4_:_ for U1, U2 being Universal_Algebra st U1,U2 are_similar holds for b3 being PFuncFinSequence of [: the carrier of U1, the carrier of U2:] holds ( b3 = Opers (U1,U2) iff ( len b3 = len the charact of U1 & ( for n being Nat st n in dom b3 holds for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds b3 . n = [[:h1,h2:]] ) ) ); theorem Th1: :: PRALG_1:1 for U1, U2 being Universal_Algebra st U1,U2 are_similar holds UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is strict Universal_Algebra proof let U1, U2 be Universal_Algebra; ::_thesis: ( U1,U2 are_similar implies UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is strict Universal_Algebra ) set C = UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #); A1: dom (Opers (U1,U2)) = Seg (len (Opers (U1,U2))) by FINSEQ_1:def_3; assume A2: U1,U2 are_similar ; ::_thesis: UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is strict Universal_Algebra then A3: ( dom the charact of U2 = Seg (len the charact of U2) & len the charact of U2 = len the charact of U1 ) by FINSEQ_1:def_3, UNIALG_2:1; A4: len (Opers (U1,U2)) = len the charact of U1 by A2, Def4; A5: dom the charact of U1 = Seg (len the charact of U1) by FINSEQ_1:def_3; A6: the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is quasi_total proof let n be Nat; :: according to MARGREL1:def_24 ::_thesis: for b1 being Element of bool [:( the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) *), the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #):] holds ( not n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) or not b1 = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n or b1 is quasi_total ) let h be PartFunc of ( the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) *), the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #); ::_thesis: ( not n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) or not h = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n or h is quasi_total ) assume that A7: n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) and A8: h = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n ; ::_thesis: h is quasi_total reconsider h2 = the charact of U2 . n as non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 by A1, A4, A3, A7, MARGREL1:def_24, UNIALG_1:1; reconsider h1 = the charact of U1 . n as non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 by A1, A5, A4, A7, MARGREL1:def_24, UNIALG_1:1; h = [[:h1,h2:]] by A2, A7, A8, Def4; hence h is quasi_total ; ::_thesis: verum end; A9: the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is non-empty proof let n be set ; :: according to FUNCT_1:def_9 ::_thesis: ( not n in proj1 the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) or not the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n is empty ) set h = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n; assume A10: n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) ; ::_thesis: not the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n is empty then reconsider m = n as Element of NAT ; reconsider h2 = the charact of U2 . m as non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 by A1, A4, A3, A10, MARGREL1:def_24, UNIALG_1:1; reconsider h1 = the charact of U1 . m as non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 by A1, A5, A4, A10, MARGREL1:def_24, UNIALG_1:1; the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n = [[:h1,h2:]] by A2, A10, Def4; hence not the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n is empty ; ::_thesis: verum end; A11: the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is homogeneous proof let n be Nat; :: according to MARGREL1:def_23 ::_thesis: for b1 being Element of bool [:( the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) *), the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #):] holds ( not n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) or not b1 = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n or b1 is homogeneous ) let h be PartFunc of ( the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) *), the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #); ::_thesis: ( not n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) or not h = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n or h is homogeneous ) assume that A12: n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) and A13: h = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n ; ::_thesis: h is homogeneous reconsider h2 = the charact of U2 . n as non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 by A1, A4, A3, A12, MARGREL1:def_24, UNIALG_1:1; reconsider h1 = the charact of U1 . n as non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 by A1, A5, A4, A12, MARGREL1:def_24, UNIALG_1:1; h = [[:h1,h2:]] by A2, A12, A13, Def4; hence h is homogeneous ; ::_thesis: verum end; the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) <> {} by A4; hence UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is strict Universal_Algebra by A6, A11, A9, UNIALG_1:def_1, UNIALG_1:def_2, UNIALG_1:def_3; ::_thesis: verum end; definition let U1, U2 be Universal_Algebra; assume A1: U1,U2 are_similar ; func[:U1,U2:] -> strict Universal_Algebra equals :Def5: :: PRALG_1:def 5 UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #); coherence UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is strict Universal_Algebra by A1, Th1; end; :: deftheorem Def5 defines [: PRALG_1:def_5_:_ for U1, U2 being Universal_Algebra st U1,U2 are_similar holds [:U1,U2:] = UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #); definition let A, B be non empty set ; func Inv (A,B) -> Function of [:A,B:],[:B,A:] means :Def6: :: PRALG_1:def 6 for a being Element of [:A,B:] holds it . a = [(a `2),(a `1)]; existence ex b1 being Function of [:A,B:],[:B,A:] st for a being Element of [:A,B:] holds b1 . a = [(a `2),(a `1)] proof deffunc H1( Element of [:A,B:]) -> Element of [:B,A:] = [($1 `2),($1 `1)]; thus ex I being Function of [:A,B:],[:B,A:] st for a being Element of [:A,B:] holds I . a = H1(a) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Function of [:A,B:],[:B,A:] st ( for a being Element of [:A,B:] holds b1 . a = [(a `2),(a `1)] ) & ( for a being Element of [:A,B:] holds b2 . a = [(a `2),(a `1)] ) holds b1 = b2 proof let f, g be Function of [:A,B:],[:B,A:]; ::_thesis: ( ( for a being Element of [:A,B:] holds f . a = [(a `2),(a `1)] ) & ( for a being Element of [:A,B:] holds g . a = [(a `2),(a `1)] ) implies f = g ) assume that A1: for a being Element of [:A,B:] holds f . a = [(a `2),(a `1)] and A2: for a being Element of [:A,B:] holds g . a = [(a `2),(a `1)] ; ::_thesis: f = g now__::_thesis:_for_a_being_Element_of_[:A,B:]_holds_f_._a_=_g_._a let a be Element of [:A,B:]; ::_thesis: f . a = g . a f . a = [(a `2),(a `1)] by A1; hence f . a = g . a by A2; ::_thesis: verum end; hence f = g by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def6 defines Inv PRALG_1:def_6_:_ for A, B being non empty set for b3 being Function of [:A,B:],[:B,A:] holds ( b3 = Inv (A,B) iff for a being Element of [:A,B:] holds b3 . a = [(a `2),(a `1)] ); theorem :: PRALG_1:2 for A, B being non empty set holds rng (Inv (A,B)) = [:B,A:] proof let A, B be non empty set ; ::_thesis: rng (Inv (A,B)) = [:B,A:] thus rng (Inv (A,B)) c= [:B,A:] ; :: according to XBOOLE_0:def_10 ::_thesis: [:B,A:] c= rng (Inv (A,B)) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:B,A:] or x in rng (Inv (A,B)) ) A1: dom (Inv (A,B)) = [:A,B:] by FUNCT_2:def_1; assume x in [:B,A:] ; ::_thesis: x in rng (Inv (A,B)) then reconsider y = x as Element of [:B,A:] ; (Inv (A,B)) . [(y `2),(y `1)] = [([(y `2),(y `1)] `2),([(y `2),(y `1)] `1)] by Def6 .= [(y `1),([(y `2),(y `1)] `1)] .= [(y `1),(y `2)] .= y by MCART_1:21 ; hence x in rng (Inv (A,B)) by A1, FUNCT_1:def_3; ::_thesis: verum end; theorem :: PRALG_1:3 for A, B being non empty set holds Inv (A,B) is one-to-one proof let A, B be non empty set ; ::_thesis: Inv (A,B) is one-to-one let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in proj1 (Inv (A,B)) or not b1 in proj1 (Inv (A,B)) or not (Inv (A,B)) . x = (Inv (A,B)) . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in proj1 (Inv (A,B)) or not y in proj1 (Inv (A,B)) or not (Inv (A,B)) . x = (Inv (A,B)) . y or x = y ) assume that A1: ( x in dom (Inv (A,B)) & y in dom (Inv (A,B)) ) and A2: (Inv (A,B)) . x = (Inv (A,B)) . y ; ::_thesis: x = y reconsider x1 = x, y1 = y as Element of [:A,B:] by A1, FUNCT_2:def_1; ( (Inv (A,B)) . x1 = [(x1 `2),(x1 `1)] & (Inv (A,B)) . y1 = [(y1 `2),(y1 `1)] ) by Def6; then ( x1 `1 = y1 `1 & x1 `2 = y1 `2 ) by A2, XTUPLE_0:1; hence x = y by DOMAIN_1:2; ::_thesis: verum end; theorem :: PRALG_1:4 for U1, U2 being Universal_Algebra st U1,U2 are_similar holds Inv ( the carrier of U1, the carrier of U2) is Function of the carrier of [:U1,U2:], the carrier of [:U2,U1:] proof let U1, U2 be Universal_Algebra; ::_thesis: ( U1,U2 are_similar implies Inv ( the carrier of U1, the carrier of U2) is Function of the carrier of [:U1,U2:], the carrier of [:U2,U1:] ) assume U1,U2 are_similar ; ::_thesis: Inv ( the carrier of U1, the carrier of U2) is Function of the carrier of [:U1,U2:], the carrier of [:U2,U1:] then ( [:U1,U2:] = UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) & [:U2,U1:] = UAStr(# [: the carrier of U2, the carrier of U1:],(Opers (U2,U1)) #) ) by Def5; hence Inv ( the carrier of U1, the carrier of U2) is Function of the carrier of [:U1,U2:], the carrier of [:U2,U1:] ; ::_thesis: verum end; theorem Th5: :: PRALG_1:5 for U1, U2 being Universal_Algebra st U1,U2 are_similar holds for o1 being operation of U1 for o2 being operation of U2 for o being operation of [:U1,U2:] for n being Nat st o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 holds ( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] ) proof let U1, U2 be Universal_Algebra; ::_thesis: ( U1,U2 are_similar implies for o1 being operation of U1 for o2 being operation of U2 for o being operation of [:U1,U2:] for n being Nat st o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 holds ( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] ) ) assume A1: U1,U2 are_similar ; ::_thesis: for o1 being operation of U1 for o2 being operation of U2 for o being operation of [:U1,U2:] for n being Nat st o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 holds ( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] ) A2: dom (Opers (U1,U2)) = Seg (len (Opers (U1,U2))) by FINSEQ_1:def_3; A3: dom the charact of U1 = Seg (len the charact of U1) by FINSEQ_1:def_3; let o1 be operation of U1; ::_thesis: for o2 being operation of U2 for o being operation of [:U1,U2:] for n being Nat st o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 holds ( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] ) let o2 be operation of U2; ::_thesis: for o being operation of [:U1,U2:] for n being Nat st o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 holds ( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] ) let o be operation of [:U1,U2:]; ::_thesis: for n being Nat st o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 holds ( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] ) let n be Nat; ::_thesis: ( o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 implies ( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] ) ) assume that A4: o1 = the charact of U1 . n and A5: o2 = the charact of U2 . n and A6: o = the charact of [:U1,U2:] . n and A7: n in dom the charact of U1 ; ::_thesis: ( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] ) A8: ( dom (signature U1) = Seg (len (signature U1)) & len (signature U1) = len the charact of U1 ) by FINSEQ_1:def_3, UNIALG_1:def_4; then A9: (signature U1) . n = arity o1 by A4, A7, A3, UNIALG_1:def_4; A10: signature U1 = signature U2 by A1, UNIALG_2:def_1; then A11: (signature U2) . n = arity o2 by A5, A7, A3, A8, UNIALG_1:def_4; A12: ( [:U1,U2:] = UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) & len the charact of U1 = len (Opers (U1,U2)) ) by A1, Def4, Def5; then o = [[:o1,o2:]] by A1, A4, A5, A6, A7, A3, A2, Def4; then A13: dom o = (arity o1) -tuples_on [: the carrier of U1, the carrier of U2:] by A10, A9, A11, Def3; ( ex x being FinSequence st x in dom o & ( for x being FinSequence st x in dom o holds len x = arity o1 ) ) proof set a = the Element of (arity o1) -tuples_on [: the carrier of U1, the carrier of U2:]; the Element of (arity o1) -tuples_on [: the carrier of U1, the carrier of U2:] in dom o by A13; hence ex x being FinSequence st x in dom o ; ::_thesis: for x being FinSequence st x in dom o holds len x = arity o1 let x be FinSequence; ::_thesis: ( x in dom o implies len x = arity o1 ) assume x in dom o ; ::_thesis: len x = arity o1 then ex s being Element of [: the carrier of U1, the carrier of U2:] * st ( s = x & len s = arity o1 ) by A13; hence len x = arity o1 ; ::_thesis: verum end; hence ( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] ) by A1, A4, A5, A6, A7, A3, A2, A12, A10, A9, A11, Def4, MARGREL1:def_25; ::_thesis: verum end; theorem :: PRALG_1:6 for U1, U2 being Universal_Algebra st U1,U2 are_similar holds [:U1,U2:],U1 are_similar proof let U1, U2 be Universal_Algebra; ::_thesis: ( U1,U2 are_similar implies [:U1,U2:],U1 are_similar ) A1: dom (signature U1) = Seg (len (signature U1)) by FINSEQ_1:def_3; A2: dom (signature U1) = Seg (len (signature U1)) by FINSEQ_1:def_3; A3: dom the charact of [:U1,U2:] = Seg (len the charact of [:U1,U2:]) by FINSEQ_1:def_3; A4: dom the charact of U2 = Seg (len the charact of U2) by FINSEQ_1:def_3; A5: dom the charact of U1 = Seg (len the charact of U1) by FINSEQ_1:def_3; assume A6: U1,U2 are_similar ; ::_thesis: [:U1,U2:],U1 are_similar then [:U1,U2:] = UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) by Def5; then len the charact of [:U1,U2:] = len the charact of U1 by A6, Def4; then A7: len (signature [:U1,U2:]) = len the charact of U1 by UNIALG_1:def_4 .= len (signature U1) by UNIALG_1:def_4 ; A8: dom (signature [:U1,U2:]) = Seg (len (signature [:U1,U2:])) by FINSEQ_1:def_3; now__::_thesis:_for_n_being_Nat_st_n_in_dom_(signature_U1)_holds_ (signature_U1)_._n_=_(signature_[:U1,U2:])_._n let n be Nat; ::_thesis: ( n in dom (signature U1) implies (signature U1) . n = (signature [:U1,U2:]) . n ) assume A9: n in dom (signature U1) ; ::_thesis: (signature U1) . n = (signature [:U1,U2:]) . n then n in dom the charact of [:U1,U2:] by A7, A1, A3, UNIALG_1:def_4; then reconsider o12 = the charact of [:U1,U2:] . n as operation of [:U1,U2:] by FUNCT_1:def_3; len (signature U1) = len (signature U2) by A6, UNIALG_2:def_1 .= len the charact of U2 by UNIALG_1:def_4 ; then reconsider o2 = the charact of U2 . n as operation of U2 by A1, A4, A9, FUNCT_1:def_3; A10: o2 = the charact of U2 . n ; A11: n in Seg (len the charact of U1) by A2, A9, UNIALG_1:def_4; then n in dom the charact of U1 by FINSEQ_1:def_3; then reconsider o1 = the charact of U1 . n as operation of U1 by FUNCT_1:def_3; ( (signature U1) . n = arity o1 & (signature [:U1,U2:]) . n = arity o12 ) by A7, A1, A8, A9, UNIALG_1:def_4; hence (signature U1) . n = (signature [:U1,U2:]) . n by A6, A5, A11, A10, Th5; ::_thesis: verum end; then signature U1 = signature [:U1,U2:] by A7, FINSEQ_2:9; hence [:U1,U2:],U1 are_similar by UNIALG_2:def_1; ::_thesis: verum end; theorem :: PRALG_1:7 for U1, U2, U3, U4 being Universal_Algebra st U1 is SubAlgebra of U2 & U3 is SubAlgebra of U4 & U2,U4 are_similar holds [:U1,U3:] is SubAlgebra of [:U2,U4:] proof let U1, U2, U3, U4 be Universal_Algebra; ::_thesis: ( U1 is SubAlgebra of U2 & U3 is SubAlgebra of U4 & U2,U4 are_similar implies [:U1,U3:] is SubAlgebra of [:U2,U4:] ) assume that A1: U1 is SubAlgebra of U2 and A2: U3 is SubAlgebra of U4 and A3: U2,U4 are_similar ; ::_thesis: [:U1,U3:] is SubAlgebra of [:U2,U4:] A4: [:U2,U4:] = UAStr(# [: the carrier of U2, the carrier of U4:],(Opers (U2,U4)) #) by A3, Def5; A5: U1,U2 are_similar by A1, UNIALG_2:13; then A6: U1,U4 are_similar by A3, UNIALG_2:2; A7: U3,U4 are_similar by A2, UNIALG_2:13; then A8: [:U1,U3:] = UAStr(# [: the carrier of U1, the carrier of U3:],(Opers (U1,U3)) #) by A6, Def5, UNIALG_2:2; A9: ( the carrier of U1 is Subset of U2 & the carrier of U3 is Subset of U4 ) by A1, A2, UNIALG_2:def_7; hence the carrier of [:U1,U3:] is Subset of [:U2,U4:] by A8, A4, ZFMISC_1:96; :: according to UNIALG_2:def_7 ::_thesis: for b1 being Element of bool the carrier of [:U2,U4:] holds ( not b1 = the carrier of [:U1,U3:] or ( the charact of [:U1,U3:] = Opers ([:U2,U4:],b1) & b1 is opers_closed ) ) let B be non empty Subset of [:U2,U4:]; ::_thesis: ( not B = the carrier of [:U1,U3:] or ( the charact of [:U1,U3:] = Opers ([:U2,U4:],B) & B is opers_closed ) ) assume A10: B = the carrier of [:U1,U3:] ; ::_thesis: ( the charact of [:U1,U3:] = Opers ([:U2,U4:],B) & B is opers_closed ) signature U4 = signature U2 by A3, UNIALG_2:def_1; then len the charact of U4 = len (signature U2) by UNIALG_1:def_4; then A11: ( dom the charact of U4 = Seg (len the charact of U4) & len the charact of U4 = len the charact of U2 ) by FINSEQ_1:def_3, UNIALG_1:def_4; A12: dom the charact of U1 = Seg (len the charact of U1) by FINSEQ_1:def_3; A13: dom the charact of U2 = Seg (len the charact of U2) by FINSEQ_1:def_3; A14: U1,U3 are_similar by A7, A6, UNIALG_2:2; then A15: len the charact of [:U1,U3:] = len the charact of U1 by A8, Def4; signature U1 = signature U3 by A14, UNIALG_2:def_1; then len the charact of U1 = len (signature U3) by UNIALG_1:def_4; then A16: ( dom the charact of U3 = Seg (len the charact of U3) & len the charact of U1 = len the charact of U3 ) by FINSEQ_1:def_3, UNIALG_1:def_4; A17: dom (Opers ([:U2,U4:],B)) = Seg (len (Opers ([:U2,U4:],B))) by FINSEQ_1:def_3; A18: dom the charact of [:U2,U4:] = dom (Opers ([:U2,U4:],B)) by UNIALG_2:def_6; then len the charact of [:U2,U4:] = len (Opers ([:U2,U4:],B)) by FINSEQ_3:29; then A19: len the charact of U2 = len (Opers ([:U2,U4:],B)) by A3, A4, Def4; signature U1 = signature U2 by A5, UNIALG_2:def_1; then len the charact of U1 = len (signature U2) by UNIALG_1:def_4; then A20: len the charact of [:U1,U3:] = len (Opers ([:U2,U4:],B)) by A19, A15, UNIALG_1:def_4; reconsider B3 = the carrier of U3 as non empty Subset of U4 by A2, UNIALG_2:def_7; A21: B3 is opers_closed by A2, UNIALG_2:def_7; reconsider B1 = the carrier of U1 as non empty Subset of U2 by A1, UNIALG_2:def_7; A22: B1 is opers_closed by A1, UNIALG_2:def_7; A23: [: the carrier of U1, the carrier of U3:] c= [: the carrier of U2, the carrier of U4:] by A9, ZFMISC_1:96; A24: for o being operation of [:U2,U4:] holds B is_closed_on o proof let o be operation of [:U2,U4:]; ::_thesis: B is_closed_on o let s be FinSequence of B; :: according to UNIALG_2:def_3 ::_thesis: ( not len s = arity o or o . s in B ) reconsider s0 = s as Element of [: the carrier of U1, the carrier of U3:] * by A8, A10, FINSEQ_1:def_11; consider n being Nat such that A25: n in dom the charact of [:U2,U4:] and A26: the charact of [:U2,U4:] . n = o by FINSEQ_2:10; reconsider s3 = pr2 s0 as Element of B3 * by FINSEQ_1:def_11; reconsider s1 = pr1 s0 as Element of B1 * by FINSEQ_1:def_11; A27: len the charact of [:U2,U4:] = len the charact of U2 by A3, A4, Def4; A28: n in Seg (len the charact of [:U2,U4:]) by A25, FINSEQ_1:def_3; then A29: n in dom the charact of U2 by A27, FINSEQ_1:def_3; then reconsider o2 = the charact of U2 . n as operation of U2 by FUNCT_1:def_3; len the charact of U4 = len the charact of U2 by A3, UNIALG_2:1; then n in dom the charact of U4 by A28, A27, FINSEQ_1:def_3; then reconsider o4 = the charact of U4 . n as operation of U4 by FUNCT_1:def_3; A30: o = [[:o2,o4:]] by A3, A26, A29, Th5; o4 = the charact of U4 . n ; then A31: arity o = arity o2 by A3, A26, A29, Th5; rng s0 c= [: the carrier of U1, the carrier of U3:] by FINSEQ_1:def_4; then rng s0 c= [: the carrier of U2, the carrier of U4:] by A23, XBOOLE_1:1; then s0 is FinSequence of [: the carrier of U2, the carrier of U4:] by FINSEQ_1:def_4; then reconsider ss = s0 as Element of [: the carrier of U2, the carrier of U4:] * by FINSEQ_1:def_11; o2 = the charact of U2 . n ; then A32: arity o = arity o4 by A3, A26, A29, Th5; assume A33: len s = arity o ; ::_thesis: o . s in B then A34: ss in { w where w is Element of [: the carrier of U2, the carrier of U4:] * : len w = arity o2 } by A31; ( B3 is_closed_on o4 & len s3 = len s0 ) by A21, Def2, UNIALG_2:def_4; then A35: o4 . s3 in B3 by A33, A32, UNIALG_2:def_3; ( B1 is_closed_on o2 & len s1 = len s0 ) by A22, Def1, UNIALG_2:def_4; then A36: o2 . s1 in B1 by A33, A31, UNIALG_2:def_3; dom [[:o2,o4:]] = (arity o2) -tuples_on [: the carrier of U2, the carrier of U4:] by A31, A32, Def3; then o . s = [(o2 . (pr1 ss)),(o4 . (pr2 ss))] by A31, A32, A30, A34, Def3; hence o . s in B by A8, A10, A36, A35, ZFMISC_1:87; ::_thesis: verum end; A37: dom the charact of U4 = dom (Opers (U4,B3)) by UNIALG_2:def_6; A38: dom the charact of [:U1,U3:] = Seg (len the charact of [:U1,U3:]) by FINSEQ_1:def_3; A39: dom the charact of U2 = dom (Opers (U2,B1)) by UNIALG_2:def_6; for n being Nat st n in dom the charact of [:U1,U3:] holds the charact of [:U1,U3:] . n = (Opers ([:U2,U4:],B)) . n proof let n be Nat; ::_thesis: ( n in dom the charact of [:U1,U3:] implies the charact of [:U1,U3:] . n = (Opers ([:U2,U4:],B)) . n ) assume A40: n in dom the charact of [:U1,U3:] ; ::_thesis: the charact of [:U1,U3:] . n = (Opers ([:U2,U4:],B)) . n then reconsider o2 = the charact of U2 . n as operation of U2 by A19, A20, A13, A38, FUNCT_1:def_3; reconsider o4 = the charact of U4 . n as operation of U4 by A19, A20, A38, A11, A40, FUNCT_1:def_3; reconsider o24 = the charact of [:U2,U4:] . n as operation of [:U2,U4:] by A18, A20, A38, A17, A40, FUNCT_1:def_3; A41: o24 = [[:o2,o4:]] by A3, A19, A20, A13, A38, A40, Th5; reconsider o3 = the charact of U3 . n as operation of U3 by A15, A38, A16, A40, FUNCT_1:def_3; (Opers (U4,B3)) . n = o4 /. B3 by A19, A20, A38, A11, A37, A40, UNIALG_2:def_6; then A42: o3 = o4 /. B3 by A2, UNIALG_2:def_7; o2 = the charact of U2 . n ; then A43: arity o24 = arity o4 by A3, A19, A20, A13, A38, A40, Th5; reconsider o1 = the charact of U1 . n as operation of U1 by A15, A12, A38, A40, FUNCT_1:def_3; (Opers (U2,B1)) . n = o2 /. B1 by A19, A20, A13, A38, A39, A40, UNIALG_2:def_6; then A44: o1 = o2 /. B1 by A1, UNIALG_2:def_7; A45: B3 is_closed_on o4 by A21, UNIALG_2:def_4; then A46: arity (o4 /. B3) = arity o4 by UNIALG_2:5; o4 = the charact of U4 . n ; then A47: arity o24 = arity o2 by A3, A19, A20, A13, A38, A40, Th5; then A48: dom ([[:o2,o4:]] | ((arity o24) -tuples_on B)) = (dom [[:o2,o4:]]) /\ ((arity o2) -tuples_on B) by RELAT_1:61 .= ((arity o2) -tuples_on the carrier of [:U2,U4:]) /\ ((arity o2) -tuples_on B) by A4, A43, A47, Def3 .= (arity o2) -tuples_on B by MARGREL1:21 ; A49: B1 is_closed_on o2 by A22, UNIALG_2:def_4; then A50: arity (o2 /. B1) = arity o2 by UNIALG_2:5; then A51: dom [[:(o2 /. B1),(o4 /. B3):]] = (arity o2) -tuples_on B by A8, A10, A43, A47, A46, Def3; A52: now__::_thesis:_for_x_being_set_st_x_in_(arity_o2)_-tuples_on_B_holds_ [[:(o2_/._B1),(o4_/._B3):]]_._x_=_([[:o2,o4:]]_|_((arity_o24)_-tuples_on_B))_._x let x be set ; ::_thesis: ( x in (arity o2) -tuples_on B implies [[:(o2 /. B1),(o4 /. B3):]] . x = ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x ) A53: dom ([[:o2,o4:]] | ((arity o24) -tuples_on B)) c= dom [[:o2,o4:]] by RELAT_1:60; assume A54: x in (arity o2) -tuples_on B ; ::_thesis: [[:(o2 /. B1),(o4 /. B3):]] . x = ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x then consider s being Element of B * such that A55: s = x and A56: len s = arity o2 ; rng s c= B by FINSEQ_1:def_4; then rng s c= [: the carrier of U2, the carrier of U4:] by A4, XBOOLE_1:1; then reconsider s0 = s as FinSequence of [: the carrier of U2, the carrier of U4:] by FINSEQ_1:def_4; A57: ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x = [[:o2,o4:]] . s0 by A48, A54, A55, FUNCT_1:47 .= [(o2 . (pr1 s0)),(o4 . (pr2 s0))] by A43, A47, A48, A54, A55, A53, Def3 ; reconsider s1 = s as FinSequence of [:B1,B3:] by A8, A10; reconsider s11 = pr1 s1 as Element of B1 * by FINSEQ_1:def_11; len (pr1 s1) = len s1 by Def1; then A58: s11 in { a where a is Element of B1 * : len a = arity o2 } by A56; reconsider s12 = pr2 s1 as Element of B3 * by FINSEQ_1:def_11; len (pr2 s1) = len s1 by Def2; then A59: s12 in { b where b is Element of B3 * : len b = arity o4 } by A43, A47, A56; A60: dom (o4 | ((arity o4) -tuples_on B3)) = (dom o4) /\ ((arity o4) -tuples_on B3) by RELAT_1:61 .= ((arity o4) -tuples_on the carrier of U4) /\ ((arity o4) -tuples_on B3) by MARGREL1:22 .= (arity o4) -tuples_on B3 by MARGREL1:21 ; A61: dom (o2 | ((arity o2) -tuples_on B1)) = (dom o2) /\ ((arity o2) -tuples_on B1) by RELAT_1:61 .= ((arity o2) -tuples_on the carrier of U2) /\ ((arity o2) -tuples_on B1) by MARGREL1:22 .= (arity o2) -tuples_on B1 by MARGREL1:21 ; [[:(o2 /. B1),(o4 /. B3):]] . x = [((o2 /. B1) . (pr1 s1)),((o4 /. B3) . (pr2 s1))] by A43, A47, A50, A46, A51, A54, A55, Def3 .= [((o2 | ((arity o2) -tuples_on B1)) . s11),((o4 /. B3) . (pr2 s1))] by A49, UNIALG_2:def_5 .= [(o2 . (pr1 s1)),((o4 /. B3) . (pr2 s1))] by A58, A61, FUNCT_1:47 .= [(o2 . (pr1 s1)),((o4 | ((arity o4) -tuples_on B3)) . (pr2 s1))] by A45, UNIALG_2:def_5 .= [(o2 . (pr1 s1)),(o4 . (pr2 s1))] by A59, A60, FUNCT_1:47 ; hence [[:(o2 /. B1),(o4 /. B3):]] . x = ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x by A57; ::_thesis: verum end; thus (Opers ([:U2,U4:],B)) . n = o24 /. B by A20, A38, A17, A40, UNIALG_2:def_6 .= [[:o2,o4:]] | ((arity o24) -tuples_on B) by A24, A41, UNIALG_2:def_5 .= [[:(o2 /. B1),(o4 /. B3):]] by A51, A48, A52, FUNCT_1:2 .= the charact of [:U1,U3:] . n by A14, A8, A40, A44, A42, Def4 ; ::_thesis: verum end; hence ( the charact of [:U1,U3:] = Opers ([:U2,U4:],B) & B is opers_closed ) by A24, A20, FINSEQ_2:9, UNIALG_2:def_4; ::_thesis: verum end; begin definition let k be Nat; func TrivialOp k -> PartFunc of ({{}} *),{{}} means :Def7: :: PRALG_1:def 7 ( dom it = {(k |-> {})} & rng it = {{}} ); existence ex b1 being PartFunc of ({{}} *),{{}} st ( dom b1 = {(k |-> {})} & rng b1 = {{}} ) proof consider f being Function such that A1: dom f = {(k |-> {})} and A2: rng f = {{}} by FUNCT_1:5; dom f c= {{}} * proof reconsider a = {} as Element of {{}} by TARSKI:def_1; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in {{}} * ) assume x in dom f ; ::_thesis: x in {{}} * then x = k |-> a by A1, TARSKI:def_1; hence x in {{}} * by FINSEQ_1:def_11; ::_thesis: verum end; then reconsider f = f as PartFunc of ({{}} *),{{}} by A2, RELSET_1:4; take f ; ::_thesis: ( dom f = {(k |-> {})} & rng f = {{}} ) thus ( dom f = {(k |-> {})} & rng f = {{}} ) by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of ({{}} *),{{}} st dom b1 = {(k |-> {})} & rng b1 = {{}} & dom b2 = {(k |-> {})} & rng b2 = {{}} holds b1 = b2 by FUNCT_1:7; end; :: deftheorem Def7 defines TrivialOp PRALG_1:def_7_:_ for k being Nat for b2 being PartFunc of ({{}} *),{{}} holds ( b2 = TrivialOp k iff ( dom b2 = {(k |-> {})} & rng b2 = {{}} ) ); registration let k be Nat; cluster TrivialOp k -> non empty homogeneous quasi_total ; coherence ( TrivialOp k is homogeneous & TrivialOp k is quasi_total & not TrivialOp k is empty ) proof set f = TrivialOp k; A1: dom (TrivialOp k) = {(k |-> {})} by Def7; thus TrivialOp k is homogeneous ::_thesis: ( TrivialOp k is quasi_total & not TrivialOp k is empty ) proof let x, y be FinSequence; :: according to MARGREL1:def_1,MARGREL1:def_21 ::_thesis: ( not x in proj1 (TrivialOp k) or not y in proj1 (TrivialOp k) or len x = len y ) assume that A2: x in dom (TrivialOp k) and A3: y in dom (TrivialOp k) ; ::_thesis: len x = len y x = k |-> {} by A1, A2, TARSKI:def_1; hence len x = len y by A1, A3, TARSKI:def_1; ::_thesis: verum end; now__::_thesis:_for_x,_y_being_FinSequence_of_{{}}_st_len_x_=_len_y_&_x_in_dom_(TrivialOp_k)_holds_ y_in_dom_(TrivialOp_k) let x, y be FinSequence of {{}}; ::_thesis: ( len x = len y & x in dom (TrivialOp k) implies y in dom (TrivialOp k) ) assume that A4: len x = len y and A5: x in dom (TrivialOp k) ; ::_thesis: y in dom (TrivialOp k) A6: dom x = Seg (len x) by FINSEQ_1:def_3; A7: x = k |-> {} by A1, A5, TARSKI:def_1; now__::_thesis:_for_n_being_Nat_st_n_in_dom_x_holds_ x_._n_=_y_._n let n be Nat; ::_thesis: ( n in dom x implies x . n = y . n ) assume n in dom x ; ::_thesis: x . n = y . n then n in dom y by A4, A6, FINSEQ_1:def_3; then A8: y . n in {{}} by FINSEQ_2:11; x . n = {} by A7; hence x . n = y . n by A8, TARSKI:def_1; ::_thesis: verum end; hence y in dom (TrivialOp k) by A4, A5, FINSEQ_2:9; ::_thesis: verum end; hence ( TrivialOp k is quasi_total & not TrivialOp k is empty ) by A1, MARGREL1:def_22; ::_thesis: verum end; end; theorem :: PRALG_1:8 for k being Nat holds arity (TrivialOp k) = k proof let k be Nat; ::_thesis: arity (TrivialOp k) = k now__::_thesis:_(_ex_x_being_FinSequence_st_x_in_dom_(TrivialOp_k)_&_(_for_x_being_FinSequence_st_x_in_dom_(TrivialOp_k)_holds_ len_x_=_k_)_) dom (TrivialOp k) = {(k |-> {})} by Def7; then k |-> {} in dom (TrivialOp k) by TARSKI:def_1; hence ex x being FinSequence st x in dom (TrivialOp k) ; ::_thesis: for x being FinSequence st x in dom (TrivialOp k) holds len x = k let x be FinSequence; ::_thesis: ( x in dom (TrivialOp k) implies len x = k ) assume x in dom (TrivialOp k) ; ::_thesis: len x = k then x in {(k |-> {})} by Def7; then x = k |-> {} by TARSKI:def_1; hence len x = k by CARD_1:def_7; ::_thesis: verum end; hence arity (TrivialOp k) = k by MARGREL1:def_25; ::_thesis: verum end; definition let f be FinSequence of NAT ; func TrivialOps f -> PFuncFinSequence of {{}} means :Def8: :: PRALG_1:def 8 ( len it = len f & ( for n being Nat st n in dom it holds for m being Nat st m = f . n holds it . n = TrivialOp m ) ); existence ex b1 being PFuncFinSequence of {{}} st ( len b1 = len f & ( for n being Nat st n in dom b1 holds for m being Nat st m = f . n holds b1 . n = TrivialOp m ) ) proof defpred S1[ set , set ] means for m being Nat st m = f . $1 holds $2 = TrivialOp m; A1: for k being Nat st k in Seg (len f) holds ex x being Element of PFuncs (({{}} *),{{}}) st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len f) implies ex x being Element of PFuncs (({{}} *),{{}}) st S1[k,x] ) assume k in Seg (len f) ; ::_thesis: ex x being Element of PFuncs (({{}} *),{{}}) st S1[k,x] then k in dom f by FINSEQ_1:def_3; then reconsider k1 = f . k as Element of NAT by FINSEQ_2:11; reconsider A = TrivialOp k1 as Element of PFuncs (({{}} *),{{}}) by PARTFUN1:45; take A ; ::_thesis: S1[k,A] let m be Nat; ::_thesis: ( m = f . k implies A = TrivialOp m ) assume m = f . k ; ::_thesis: A = TrivialOp m hence A = TrivialOp m ; ::_thesis: verum end; consider p being FinSequence of PFuncs (({{}} *),{{}}) such that A2: ( dom p = Seg (len f) & ( for k being Nat st k in Seg (len f) holds S1[k,p . k] ) ) from FINSEQ_1:sch_5(A1); reconsider p = p as PFuncFinSequence of {{}} ; take p ; ::_thesis: ( len p = len f & ( for n being Nat st n in dom p holds for m being Nat st m = f . n holds p . n = TrivialOp m ) ) thus len p = len f by A2, FINSEQ_1:def_3; ::_thesis: for n being Nat st n in dom p holds for m being Nat st m = f . n holds p . n = TrivialOp m let n be Nat; ::_thesis: ( n in dom p implies for m being Nat st m = f . n holds p . n = TrivialOp m ) assume n in dom p ; ::_thesis: for m being Nat st m = f . n holds p . n = TrivialOp m hence for m being Nat st m = f . n holds p . n = TrivialOp m by A2; ::_thesis: verum end; uniqueness for b1, b2 being PFuncFinSequence of {{}} st len b1 = len f & ( for n being Nat st n in dom b1 holds for m being Nat st m = f . n holds b1 . n = TrivialOp m ) & len b2 = len f & ( for n being Nat st n in dom b2 holds for m being Nat st m = f . n holds b2 . n = TrivialOp m ) holds b1 = b2 proof let x, y be PFuncFinSequence of {{}}; ::_thesis: ( len x = len f & ( for n being Nat st n in dom x holds for m being Nat st m = f . n holds x . n = TrivialOp m ) & len y = len f & ( for n being Nat st n in dom y holds for m being Nat st m = f . n holds y . n = TrivialOp m ) implies x = y ) assume that A3: len x = len f and A4: for n being Nat st n in dom x holds for m being Nat st m = f . n holds x . n = TrivialOp m and A5: len y = len f and A6: for n being Nat st n in dom y holds for m being Nat st m = f . n holds y . n = TrivialOp m ; ::_thesis: x = y A7: dom x = Seg (len f) by A3, FINSEQ_1:def_3; now__::_thesis:_for_n_being_Nat_st_n_in_dom_x_holds_ x_._n_=_y_._n let n be Nat; ::_thesis: ( n in dom x implies x . n = y . n ) assume A8: n in dom x ; ::_thesis: x . n = y . n then n in dom f by A7, FINSEQ_1:def_3; then reconsider m = f . n as Element of NAT by FINSEQ_2:11; ( n in dom y & x . n = TrivialOp m ) by A4, A5, A7, A8, FINSEQ_1:def_3; hence x . n = y . n by A6; ::_thesis: verum end; hence x = y by A3, A5, FINSEQ_2:9; ::_thesis: verum end; end; :: deftheorem Def8 defines TrivialOps PRALG_1:def_8_:_ for f being FinSequence of NAT for b2 being PFuncFinSequence of {{}} holds ( b2 = TrivialOps f iff ( len b2 = len f & ( for n being Nat st n in dom b2 holds for m being Nat st m = f . n holds b2 . n = TrivialOp m ) ) ); theorem Th9: :: PRALG_1:9 for f being FinSequence of NAT holds ( TrivialOps f is homogeneous & TrivialOps f is quasi_total & TrivialOps f is non-empty ) proof let f be FinSequence of NAT ; ::_thesis: ( TrivialOps f is homogeneous & TrivialOps f is quasi_total & TrivialOps f is non-empty ) A1: for n being Nat for h being PartFunc of ({{}} *),{{}} st n in dom (TrivialOps f) & h = (TrivialOps f) . n holds h is quasi_total proof let n be Nat; ::_thesis: for h being PartFunc of ({{}} *),{{}} st n in dom (TrivialOps f) & h = (TrivialOps f) . n holds h is quasi_total let h be PartFunc of ({{}} *),{{}}; ::_thesis: ( n in dom (TrivialOps f) & h = (TrivialOps f) . n implies h is quasi_total ) assume that A2: n in dom (TrivialOps f) and A3: (TrivialOps f) . n = h ; ::_thesis: h is quasi_total dom (TrivialOps f) = Seg (len (TrivialOps f)) by FINSEQ_1:def_3 .= Seg (len f) by Def8 .= dom f by FINSEQ_1:def_3 ; then reconsider m = f . n as Element of NAT by A2, FINSEQ_2:11; (TrivialOps f) . n = TrivialOp m by A2, Def8; hence h is quasi_total by A3; ::_thesis: verum end; A4: for n being set st n in dom (TrivialOps f) holds not (TrivialOps f) . n is empty proof let n be set ; ::_thesis: ( n in dom (TrivialOps f) implies not (TrivialOps f) . n is empty ) assume A5: n in dom (TrivialOps f) ; ::_thesis: not (TrivialOps f) . n is empty then reconsider k = n as Element of NAT ; dom (TrivialOps f) = Seg (len (TrivialOps f)) by FINSEQ_1:def_3 .= Seg (len f) by Def8 .= dom f by FINSEQ_1:def_3 ; then reconsider m = f . k as Element of NAT by A5, FINSEQ_2:11; (TrivialOps f) . k = TrivialOp m by A5, Def8; hence not (TrivialOps f) . n is empty ; ::_thesis: verum end; for n being Nat for h being PartFunc of ({{}} *),{{}} st n in dom (TrivialOps f) & h = (TrivialOps f) . n holds h is homogeneous proof let n be Nat; ::_thesis: for h being PartFunc of ({{}} *),{{}} st n in dom (TrivialOps f) & h = (TrivialOps f) . n holds h is homogeneous let h be PartFunc of ({{}} *),{{}}; ::_thesis: ( n in dom (TrivialOps f) & h = (TrivialOps f) . n implies h is homogeneous ) assume that A6: n in dom (TrivialOps f) and A7: (TrivialOps f) . n = h ; ::_thesis: h is homogeneous dom (TrivialOps f) = Seg (len (TrivialOps f)) by FINSEQ_1:def_3 .= Seg (len f) by Def8 .= dom f by FINSEQ_1:def_3 ; then reconsider m = f . n as Element of NAT by A6, FINSEQ_2:11; (TrivialOps f) . n = TrivialOp m by A6, Def8; hence h is homogeneous by A7; ::_thesis: verum end; hence ( TrivialOps f is homogeneous & TrivialOps f is quasi_total & TrivialOps f is non-empty ) by A1, A4, FUNCT_1:def_9, MARGREL1:def_23, MARGREL1:def_24; ::_thesis: verum end; theorem Th10: :: PRALG_1:10 for f being FinSequence of NAT st f <> {} holds UAStr(# {{}},(TrivialOps f) #) is strict Universal_Algebra proof let f be FinSequence of NAT ; ::_thesis: ( f <> {} implies UAStr(# {{}},(TrivialOps f) #) is strict Universal_Algebra ) assume A1: f <> {} ; ::_thesis: UAStr(# {{}},(TrivialOps f) #) is strict Universal_Algebra set U0 = UAStr(# {{}},(TrivialOps f) #); A2: ( the charact of UAStr(# {{}},(TrivialOps f) #) is homogeneous & the charact of UAStr(# {{}},(TrivialOps f) #) is quasi_total & the charact of UAStr(# {{}},(TrivialOps f) #) is non-empty ) by Th9; len the charact of UAStr(# {{}},(TrivialOps f) #) = len f by Def8; then the charact of UAStr(# {{}},(TrivialOps f) #) <> {} by A1; hence UAStr(# {{}},(TrivialOps f) #) is strict Universal_Algebra by A2, UNIALG_1:def_1, UNIALG_1:def_2, UNIALG_1:def_3; ::_thesis: verum end; registration let D be non empty set ; cluster Relation-like NAT -defined D -valued Function-like non empty V31() countable FinSequence-like FinSubsequence-like for Element of D * ; existence not for b1 being Element of D * holds b1 is empty proof set d = the Element of D; reconsider e = <* the Element of D*> as Element of D * by FINSEQ_1:def_11; take e ; ::_thesis: not e is empty thus not e is empty ; ::_thesis: verum end; end; definition let f be non empty FinSequence of NAT ; func Trivial_Algebra f -> strict Universal_Algebra equals :: PRALG_1:def 9 UAStr(# {{}},(TrivialOps f) #); coherence UAStr(# {{}},(TrivialOps f) #) is strict Universal_Algebra by Th10; end; :: deftheorem defines Trivial_Algebra PRALG_1:def_9_:_ for f being non empty FinSequence of NAT holds Trivial_Algebra f = UAStr(# {{}},(TrivialOps f) #); begin definition let IT be Function; attrIT is Univ_Alg-yielding means :Def10: :: PRALG_1:def 10 for x being set st x in dom IT holds IT . x is Universal_Algebra; end; :: deftheorem Def10 defines Univ_Alg-yielding PRALG_1:def_10_:_ for IT being Function holds ( IT is Univ_Alg-yielding iff for x being set st x in dom IT holds IT . x is Universal_Algebra ); definition let IT be Function; attrIT is 1-sorted-yielding means :Def11: :: PRALG_1:def 11 for x being set st x in dom IT holds IT . x is 1-sorted ; end; :: deftheorem Def11 defines 1-sorted-yielding PRALG_1:def_11_:_ for IT being Function holds ( IT is 1-sorted-yielding iff for x being set st x in dom IT holds IT . x is 1-sorted ); registration cluster Relation-like Function-like Univ_Alg-yielding for set ; existence ex b1 being Function st b1 is Univ_Alg-yielding proof reconsider f = {} as Function ; take f ; ::_thesis: f is Univ_Alg-yielding let x be set ; :: according to PRALG_1:def_10 ::_thesis: ( x in dom f implies f . x is Universal_Algebra ) thus ( x in dom f implies f . x is Universal_Algebra ) ; ::_thesis: verum end; end; registration cluster Relation-like Function-like Univ_Alg-yielding -> 1-sorted-yielding for set ; coherence for b1 being Function st b1 is Univ_Alg-yielding holds b1 is 1-sorted-yielding proof let F be Function; ::_thesis: ( F is Univ_Alg-yielding implies F is 1-sorted-yielding ) assume F is Univ_Alg-yielding ; ::_thesis: F is 1-sorted-yielding then for x being set st x in dom F holds F . x is 1-sorted by Def10; hence F is 1-sorted-yielding by Def11; ::_thesis: verum end; end; registration let I be set ; cluster Relation-like I -defined Function-like total 1-sorted-yielding for set ; existence ex b1 being ManySortedSet of I st b1 is 1-sorted-yielding proof set A = the 1-sorted ; set f = I --> the 1-sorted ; A1: dom (I --> the 1-sorted ) = I by FUNCOP_1:13; reconsider f = I --> the 1-sorted as ManySortedSet of I ; take f ; ::_thesis: f is 1-sorted-yielding for i being set st i in dom f holds f . i is 1-sorted by A1, FUNCOP_1:7; hence f is 1-sorted-yielding by Def11; ::_thesis: verum end; end; definition let IT be Function; attrIT is equal-signature means :Def12: :: PRALG_1:def 12 for x, y being set st x in dom IT & y in dom IT holds for U1, U2 being Universal_Algebra st U1 = IT . x & U2 = IT . y holds signature U1 = signature U2; end; :: deftheorem Def12 defines equal-signature PRALG_1:def_12_:_ for IT being Function holds ( IT is equal-signature iff for x, y being set st x in dom IT & y in dom IT holds for U1, U2 being Universal_Algebra st U1 = IT . x & U2 = IT . y holds signature U1 = signature U2 ); registration let J be non empty set ; cluster Relation-like J -defined Function-like non empty total Univ_Alg-yielding equal-signature for set ; existence ex b1 being ManySortedSet of J st ( b1 is equal-signature & b1 is Univ_Alg-yielding ) proof set U1 = the Universal_Algebra; set f = J --> the Universal_Algebra; A1: dom (J --> the Universal_Algebra) = J by FUNCOP_1:13; reconsider f = J --> the Universal_Algebra as ManySortedSet of J ; take f ; ::_thesis: ( f is equal-signature & f is Univ_Alg-yielding ) for x, y being set st x in dom f & y in dom f holds for U1, U2 being Universal_Algebra st U1 = f . x & U2 = f . y holds signature U1 = signature U2 proof let x, y be set ; ::_thesis: ( x in dom f & y in dom f implies for U1, U2 being Universal_Algebra st U1 = f . x & U2 = f . y holds signature U1 = signature U2 ) assume that A2: x in dom f and A3: y in dom f ; ::_thesis: for U1, U2 being Universal_Algebra st U1 = f . x & U2 = f . y holds signature U1 = signature U2 let U2, U3 be Universal_Algebra; ::_thesis: ( U2 = f . x & U3 = f . y implies signature U2 = signature U3 ) assume A4: ( U2 = f . x & U3 = f . y ) ; ::_thesis: signature U2 = signature U3 f . x = the Universal_Algebra by A1, A2, FUNCOP_1:7; hence signature U2 = signature U3 by A1, A3, A4, FUNCOP_1:7; ::_thesis: verum end; hence f is equal-signature by Def12; ::_thesis: f is Univ_Alg-yielding for x being set st x in dom f holds f . x is Universal_Algebra by A1, FUNCOP_1:7; hence f is Univ_Alg-yielding by Def10; ::_thesis: verum end; end; definition let J be non empty set ; let A be 1-sorted-yielding ManySortedSet of J; let j be Element of J; :: original: . redefine funcA . j -> 1-sorted ; coherence A . j is 1-sorted proof dom A = J by PARTFUN1:def_2; hence A . j is 1-sorted by Def11; ::_thesis: verum end; end; definition let J be non empty set ; let A be Univ_Alg-yielding ManySortedSet of J; let j be Element of J; :: original: . redefine funcA . j -> Universal_Algebra; coherence A . j is Universal_Algebra proof dom A = J by PARTFUN1:def_2; hence A . j is Universal_Algebra by Def10; ::_thesis: verum end; end; definition let J be set ; let A be 1-sorted-yielding ManySortedSet of J; func Carrier A -> ManySortedSet of J means :Def13: :: PRALG_1:def 13 for j being set st j in J holds ex R being 1-sorted st ( R = A . j & it . j = the carrier of R ); existence ex b1 being ManySortedSet of J st for j being set st j in J holds ex R being 1-sorted st ( R = A . j & b1 . j = the carrier of R ) proof defpred S1[ set , set ] means ex R being 1-sorted st ( R = A . $1 & $2 = the carrier of R ); A1: for i being set st i in J holds ex j being set st S1[i,j] proof let i be set ; ::_thesis: ( i in J implies ex j being set st S1[i,j] ) assume A2: i in J ; ::_thesis: ex j being set st S1[i,j] then reconsider J = J as non empty set ; reconsider i9 = i as Element of J by A2; reconsider B = A as 1-sorted-yielding ManySortedSet of J ; take the carrier of (B . i9) ; ::_thesis: S1[i, the carrier of (B . i9)] take B . i9 ; ::_thesis: ( B . i9 = A . i & the carrier of (B . i9) = the carrier of (B . i9) ) thus ( B . i9 = A . i & the carrier of (B . i9) = the carrier of (B . i9) ) ; ::_thesis: verum end; consider M being Function such that A3: dom M = J and A4: for i being set st i in J holds S1[i,M . i] from CLASSES1:sch_1(A1); reconsider M = M as ManySortedSet of J by A3, PARTFUN1:def_2, RELAT_1:def_18; take M ; ::_thesis: for j being set st j in J holds ex R being 1-sorted st ( R = A . j & M . j = the carrier of R ) thus for j being set st j in J holds ex R being 1-sorted st ( R = A . j & M . j = the carrier of R ) by A4; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedSet of J st ( for j being set st j in J holds ex R being 1-sorted st ( R = A . j & b1 . j = the carrier of R ) ) & ( for j being set st j in J holds ex R being 1-sorted st ( R = A . j & b2 . j = the carrier of R ) ) holds b1 = b2 proof let X, Y be ManySortedSet of J; ::_thesis: ( ( for j being set st j in J holds ex R being 1-sorted st ( R = A . j & X . j = the carrier of R ) ) & ( for j being set st j in J holds ex R being 1-sorted st ( R = A . j & Y . j = the carrier of R ) ) implies X = Y ) assume A5: ( ( for j being set st j in J holds ex R being 1-sorted st ( R = A . j & X . j = the carrier of R ) ) & ( for j being set st j in J holds ex R being 1-sorted st ( R = A . j & Y . j = the carrier of R ) ) ) ; ::_thesis: X = Y for i being set st i in J holds X . i = Y . i proof let i be set ; ::_thesis: ( i in J implies X . i = Y . i ) assume i in J ; ::_thesis: X . i = Y . i then ( ex R being 1-sorted st ( R = A . i & X . i = the carrier of R ) & ex R being 1-sorted st ( R = A . i & Y . i = the carrier of R ) ) by A5; hence X . i = Y . i ; ::_thesis: verum end; hence X = Y by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def13 defines Carrier PRALG_1:def_13_:_ for J being set for A being 1-sorted-yielding ManySortedSet of J for b3 being ManySortedSet of J holds ( b3 = Carrier A iff for j being set st j in J holds ex R being 1-sorted st ( R = A . j & b3 . j = the carrier of R ) ); registration let J be non empty set ; let A be Univ_Alg-yielding ManySortedSet of J; cluster Carrier A -> V2() ; coherence Carrier A is non-empty proof let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in J or not (Carrier A) . i is empty ) assume A1: i in J ; ::_thesis: not (Carrier A) . i is empty then consider R being 1-sorted such that A2: R = A . i and A3: (Carrier A) . i = the carrier of R by Def13; dom A = J by PARTFUN1:def_2; then R is Universal_Algebra by A1, A2, Def10; hence not (Carrier A) . i is empty by A3; ::_thesis: verum end; end; definition let J be non empty set ; let A be Univ_Alg-yielding equal-signature ManySortedSet of J; func ComSign A -> FinSequence of NAT means :Def14: :: PRALG_1:def 14 for j being Element of J holds it = signature (A . j); existence ex b1 being FinSequence of NAT st for j being Element of J holds b1 = signature (A . j) proof set j = the Element of J; reconsider U0 = A . the Element of J as Universal_Algebra ; take signature U0 ; ::_thesis: for j being Element of J holds signature U0 = signature (A . j) let j1 be Element of J; ::_thesis: signature U0 = signature (A . j1) dom A = J by PARTFUN1:def_2; hence signature U0 = signature (A . j1) by Def12; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of NAT st ( for j being Element of J holds b1 = signature (A . j) ) & ( for j being Element of J holds b2 = signature (A . j) ) holds b1 = b2 proof set j = the Element of J; let X, Y be FinSequence of NAT ; ::_thesis: ( ( for j being Element of J holds X = signature (A . j) ) & ( for j being Element of J holds Y = signature (A . j) ) implies X = Y ) assume that A1: for j being Element of J holds X = signature (A . j) and A2: for j being Element of J holds Y = signature (A . j) ; ::_thesis: X = Y reconsider U0 = A . the Element of J as Universal_Algebra ; X = signature U0 by A1; hence X = Y by A2; ::_thesis: verum end; end; :: deftheorem Def14 defines ComSign PRALG_1:def_14_:_ for J being non empty set for A being Univ_Alg-yielding equal-signature ManySortedSet of J for b3 being FinSequence of NAT holds ( b3 = ComSign A iff for j being Element of J holds b3 = signature (A . j) ); registration let J be non empty set ; let B be V2() ManySortedSet of J; cluster product B -> non empty ; coherence not product B is empty ; end; definition let J be non empty set ; let B be V2() ManySortedSet of J; mode ManySortedOperation of B -> ManySortedFunction of J means :Def15: :: PRALG_1:def 15 for j being Element of J holds it . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j); existence ex b1 being ManySortedFunction of J st for j being Element of J holds b1 . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j) proof defpred S1[ set , set ] means $2 in B . $1; A1: for x being set st x in J holds ex y being set st S1[x,y] by XBOOLE_0:def_1; consider f being Function such that A2: ( dom f = J & ( for x being set st x in J holds S1[x,f . x] ) ) from CLASSES1:sch_1(A1); deffunc H1( set ) -> set = (<*> (B . $1)) .--> (f . $1); consider F being Function such that A3: ( dom F = J & ( for x being set st x in J holds F . x = H1(x) ) ) from FUNCT_1:sch_3(); reconsider F = F as ManySortedSet of J by A3, 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 F . x = (<*> (B . x)) .--> (f . x) by A3; hence F . x is Function ; ::_thesis: verum end; then reconsider F = F as ManySortedFunction of J by FUNCOP_1:def_6; take F ; ::_thesis: for j being Element of J holds F . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j) let j be Element of J; ::_thesis: F . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j) reconsider b = f . j as Element of B . j by A2; F . j = (<*> (B . j)) .--> b by A3; hence F . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j) by MARGREL1:18; ::_thesis: verum end; end; :: deftheorem Def15 defines ManySortedOperation PRALG_1:def_15_:_ for J being non empty set for B being V2() ManySortedSet of J for b3 being ManySortedFunction of J holds ( b3 is ManySortedOperation of B iff for j being Element of J holds b3 . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j) ); definition let J be non empty set ; let B be V2() ManySortedSet of J; let O be ManySortedOperation of B; let j be Element of J; :: original: . redefine funcO . j -> non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j); coherence O . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j) by Def15; end; definition let IT be Function; attrIT is equal-arity means :Def16: :: PRALG_1:def 16 for x, y being set st x in dom IT & y in dom IT holds for f, g being Function st IT . x = f & IT . y = g holds for n, m being Nat for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds for o1 being non empty homogeneous quasi_total PartFunc of (X *),X for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds arity o1 = arity o2; end; :: deftheorem Def16 defines equal-arity PRALG_1:def_16_:_ for IT being Function holds ( IT is equal-arity iff for x, y being set st x in dom IT & y in dom IT holds for f, g being Function st IT . x = f & IT . y = g holds for n, m being Nat for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds for o1 being non empty homogeneous quasi_total PartFunc of (X *),X for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds arity o1 = arity o2 ); registration let J be non empty set ; let B be V2() ManySortedSet of J; cluster Relation-like J -defined Function-like non empty total Function-yielding V45() equal-arity for ManySortedOperation of B; existence ex b1 being ManySortedOperation of B st b1 is equal-arity proof defpred S1[ set , set ] means B in B . J; A1: for x being set st x in J holds ex y being set st S1[x,y] by XBOOLE_0:def_1; consider f being Function such that A2: ( dom f = J & ( for x being set st x in J holds S1[x,f . x] ) ) from CLASSES1:sch_1(A1); deffunc H1( set ) -> set = (<*> (B . J)) .--> (f . J); consider F being Function such that A3: ( dom F = J & ( for x being set st x in J holds F . x = H1(x) ) ) from FUNCT_1:sch_3(); reconsider F = F as ManySortedSet of J by A3, 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 F . x = (<*> (B . x)) .--> (f . x) by A3; hence F . x is Function ; ::_thesis: verum end; then reconsider F = F as ManySortedFunction of J by FUNCOP_1:def_6; now__::_thesis:_for_j_being_Element_of_J_holds_F_._j_is_non_empty_homogeneous_quasi_total_PartFunc_of_((B_._j)_*),(B_._j) let j be Element of J; ::_thesis: F . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j) reconsider b = f . j as Element of B . j by A2; F . j = (<*> (B . j)) .--> b by A3; hence F . j is non empty homogeneous quasi_total PartFunc of ((B . j) *),(B . j) by MARGREL1:18; ::_thesis: verum end; then reconsider F = F as ManySortedOperation of B by Def15; take F ; ::_thesis: F is equal-arity for x, y being set st x in dom F & y in dom F holds for f, g being Function st F . x = f & F . y = g holds for n, m being Nat for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds for o1 being non empty homogeneous quasi_total PartFunc of (X *),X for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds arity o1 = arity o2 proof let x, y be set ; ::_thesis: ( x in dom F & y in dom F implies for f, g being Function st F . x = f & F . y = g holds for n, m being Nat for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds for o1 being non empty homogeneous quasi_total PartFunc of (X *),X for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds arity o1 = arity o2 ) assume that A4: x in dom F and A5: y in dom F ; ::_thesis: for f, g being Function st F . x = f & F . y = g holds for n, m being Nat for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds for o1 being non empty homogeneous quasi_total PartFunc of (X *),X for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds arity o1 = arity o2 reconsider x1 = x, y1 = y as Element of J by A3, A4, A5; let g, h be Function; ::_thesis: ( F . x = g & F . y = h implies for n, m being Nat for X, Y being non empty set st dom g = n -tuples_on X & dom h = m -tuples_on Y holds for o1 being non empty homogeneous quasi_total PartFunc of (X *),X for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st g = o1 & h = o2 holds arity o1 = arity o2 ) assume that A6: F . x = g and A7: F . y = h ; ::_thesis: for n, m being Nat for X, Y being non empty set st dom g = n -tuples_on X & dom h = m -tuples_on Y holds for o1 being non empty homogeneous quasi_total PartFunc of (X *),X for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st g = o1 & h = o2 holds arity o1 = arity o2 reconsider fx = f . x1 as Element of B . x1 by A2; let n, m be Nat; ::_thesis: for X, Y being non empty set st dom g = n -tuples_on X & dom h = m -tuples_on Y holds for o1 being non empty homogeneous quasi_total PartFunc of (X *),X for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st g = o1 & h = o2 holds arity o1 = arity o2 let X, Y be non empty set ; ::_thesis: ( dom g = n -tuples_on X & dom h = m -tuples_on Y implies for o1 being non empty homogeneous quasi_total PartFunc of (X *),X for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st g = o1 & h = o2 holds arity o1 = arity o2 ) assume that dom g = n -tuples_on X and dom h = m -tuples_on Y ; ::_thesis: for o1 being non empty homogeneous quasi_total PartFunc of (X *),X for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st g = o1 & h = o2 holds arity o1 = arity o2 let o1 be non empty homogeneous quasi_total PartFunc of (X *),X; ::_thesis: for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st g = o1 & h = o2 holds arity o1 = arity o2 let o2 be non empty homogeneous quasi_total PartFunc of (Y *),Y; ::_thesis: ( g = o1 & h = o2 implies arity o1 = arity o2 ) assume that A8: g = o1 and A9: h = o2 ; ::_thesis: arity o1 = arity o2 reconsider o1x = (<*> (B . x1)) .--> fx as non empty homogeneous quasi_total PartFunc of ((B . x1) *),(B . x1) by MARGREL1:18; A10: dom o1x = {({} (B . x1))} by FUNCOP_1:13; consider p1 being set such that A11: p1 in dom o1 by XBOOLE_0:def_1; dom o1 c= X * by RELAT_1:def_18; then reconsider p1 = p1 as Element of X * by A11; o1 = (<*> (B . x)) .--> (f . x) by A3, A4, A6, A8; then p1 = <*> (B . x1) by A10, A11, TARSKI:def_1; then len p1 = 0 ; then A12: arity o1 = 0 by A11, MARGREL1:def_25; reconsider fy = f . y1 as Element of B . y1 by A2; reconsider o2y = (<*> (B . y1)) .--> fy as non empty homogeneous quasi_total PartFunc of ((B . y1) *),(B . y1) by MARGREL1:18; A13: dom o2y = {({} (B . y1))} by FUNCOP_1:13; consider p2 being set such that A14: p2 in dom o2 by XBOOLE_0:def_1; dom o2 c= Y * by RELAT_1:def_18; then reconsider p2 = p2 as Element of Y * by A14; o2 = (<*> (B . y)) .--> (f . y) by A3, A5, A7, A9; then p2 = <*> (B . y1) by A13, A14, TARSKI:def_1; then len p2 = 0 ; hence arity o1 = arity o2 by A12, A14, MARGREL1:def_25; ::_thesis: verum end; hence F is equal-arity by Def16; ::_thesis: verum end; end; theorem Th11: :: PRALG_1:11 for J being non empty set for B being V2() ManySortedSet of J for O being ManySortedOperation of B holds ( O is equal-arity iff for i, j being Element of J holds arity (O . i) = arity (O . j) ) proof let J be non empty set ; ::_thesis: for B being V2() ManySortedSet of J for O being ManySortedOperation of B holds ( O is equal-arity iff for i, j being Element of J holds arity (O . i) = arity (O . j) ) let B be V2() ManySortedSet of J; ::_thesis: for O being ManySortedOperation of B holds ( O is equal-arity iff for i, j being Element of J holds arity (O . i) = arity (O . j) ) let O be ManySortedOperation of B; ::_thesis: ( O is equal-arity iff for i, j being Element of J holds arity (O . i) = arity (O . j) ) thus ( O is equal-arity implies for i, j being Element of J holds arity (O . i) = arity (O . j) ) ::_thesis: ( ( for i, j being Element of J holds arity (O . i) = arity (O . j) ) implies O is equal-arity ) proof assume A1: O is equal-arity ; ::_thesis: for i, j being Element of J holds arity (O . i) = arity (O . j) let i, j be Element of J; ::_thesis: arity (O . i) = arity (O . j) A2: dom (O . j) = (arity (O . j)) -tuples_on (B . j) by MARGREL1:22; ( dom O = J & dom (O . i) = (arity (O . i)) -tuples_on (B . i) ) by MARGREL1:22, PARTFUN1:def_2; hence arity (O . i) = arity (O . j) by A1, A2, Def16; ::_thesis: verum end; assume A3: for i, j being Element of J holds arity (O . i) = arity (O . j) ; ::_thesis: O is equal-arity let x, y be set ; :: according to PRALG_1:def_16 ::_thesis: ( x in dom O & y in dom O implies for f, g being Function st O . x = f & O . y = g holds for n, m being Nat for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds for o1 being non empty homogeneous quasi_total PartFunc of (X *),X for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds arity o1 = arity o2 ) assume ( x in dom O & y in dom O ) ; ::_thesis: for f, g being Function st O . x = f & O . y = g holds for n, m being Nat for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds for o1 being non empty homogeneous quasi_total PartFunc of (X *),X for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds arity o1 = arity o2 then reconsider x1 = x, y1 = y as Element of J by PARTFUN1:def_2; let f, g be Function; ::_thesis: ( O . x = f & O . y = g implies for n, m being Nat for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds for o1 being non empty homogeneous quasi_total PartFunc of (X *),X for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds arity o1 = arity o2 ) assume that A4: O . x = f and A5: O . y = g ; ::_thesis: for n, m being Nat for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds for o1 being non empty homogeneous quasi_total PartFunc of (X *),X for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds arity o1 = arity o2 arity (O . x1) = arity (O . y1) by A3; then A6: dom g = (arity (O . x1)) -tuples_on (B . y1) by A5, MARGREL1:22; let n, m be Nat; ::_thesis: for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds for o1 being non empty homogeneous quasi_total PartFunc of (X *),X for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds arity o1 = arity o2 let X, Y be non empty set ; ::_thesis: ( dom f = n -tuples_on X & dom g = m -tuples_on Y implies for o1 being non empty homogeneous quasi_total PartFunc of (X *),X for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds arity o1 = arity o2 ) assume that A7: dom f = n -tuples_on X and A8: dom g = m -tuples_on Y ; ::_thesis: for o1 being non empty homogeneous quasi_total PartFunc of (X *),X for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds arity o1 = arity o2 dom f = (arity (O . x1)) -tuples_on (B . x1) by A4, MARGREL1:22; then A9: n = arity (O . x1) by A7, FINSEQ_2:110; set p = the Element of n -tuples_on X; set q = the Element of m -tuples_on Y; let o1 be non empty homogeneous quasi_total PartFunc of (X *),X; ::_thesis: for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds arity o1 = arity o2 let o2 be non empty homogeneous quasi_total PartFunc of (Y *),Y; ::_thesis: ( f = o1 & g = o2 implies arity o1 = arity o2 ) assume that A10: f = o1 and A11: g = o2 ; ::_thesis: arity o1 = arity o2 A12: arity o2 = len the Element of m -tuples_on Y by A8, A11, MARGREL1:def_25 .= m by CARD_1:def_7 ; arity o1 = len the Element of n -tuples_on X by A7, A10, MARGREL1:def_25 .= n by CARD_1:def_7 ; hence arity o1 = arity o2 by A8, A6, A9, A12, FINSEQ_2:110; ::_thesis: verum end; definition let F be Function-yielding Function; let f be Function; funcF .. f -> Function means :Def17: :: PRALG_1:def 17 ( dom it = dom F & ( for x being set st x in dom F holds it . x = (F . x) . (f . x) ) ); existence ex b1 being Function st ( dom b1 = dom F & ( for x being set st x in dom F holds b1 . x = (F . x) . (f . x) ) ) proof set I = dom F; defpred S1[ set , set ] means $2 = (F . $1) . (f . $1); A1: for i being set st i in dom F holds ex y being set st S1[i,y] ; consider F being Function such that A2: ( dom F = dom F & ( for i being set st i in dom F holds S1[i,F . i] ) ) from CLASSES1:sch_1(A1); take F ; ::_thesis: ( dom F = dom F & ( for x being set st x in dom F holds F . x = (F . x) . (f . x) ) ) thus ( dom F = dom F & ( for x being set st x in dom F holds F . x = (F . x) . (f . x) ) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = dom F & ( for x being set st x in dom F holds b1 . x = (F . x) . (f . x) ) & dom b2 = dom F & ( for x being set st x in dom F holds b2 . x = (F . x) . (f . x) ) holds b1 = b2 proof let m, n be Function; ::_thesis: ( dom m = dom F & ( for x being set st x in dom F holds m . x = (F . x) . (f . x) ) & dom n = dom F & ( for x being set st x in dom F holds n . x = (F . x) . (f . x) ) implies m = n ) assume that A3: dom m = dom F and A4: for x being set st x in dom F holds m . x = (F . x) . (f . x) and A5: dom n = dom F and A6: for x being set st x in dom F holds n . x = (F . x) . (f . x) ; ::_thesis: m = n for x being set st x in dom m holds m . x = n . x proof let x be set ; ::_thesis: ( x in dom m implies m . x = n . x ) consider g being set such that A7: g = F . x ; reconsider g = g as Function by A7; assume A8: x in dom m ; ::_thesis: m . x = n . x then m . x = g . (f . x) by A3, A4, A7; hence m . x = n . x by A3, A6, A8, A7; ::_thesis: verum end; hence m = n by A3, A5, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def17 defines .. PRALG_1:def_17_:_ for F being Function-yielding Function for f, b3 being Function holds ( b3 = F .. f iff ( dom b3 = dom F & ( for x being set st x in dom F holds b3 . x = (F . x) . (f . x) ) ) ); registration let I be set ; let f be ManySortedFunction of I; let x be ManySortedSet of I; clusterf .. x -> I -defined ; coherence f .. x is I -defined proof dom (f .. x) = dom f by Def17 .= I by PARTFUN1:def_2 ; hence f .. x is I -defined by RELAT_1:def_18; ::_thesis: verum end; end; registration let I be set ; let f be ManySortedFunction of I; let x be ManySortedSet of I; clusterf .. x -> I -defined total for I -defined Function; coherence for b1 being I -defined Function st b1 = f .. x holds b1 is total proof dom (f .. x) = dom f by Def17 .= I by PARTFUN1:def_2 ; hence for b1 being I -defined Function st b1 = f .. x holds b1 is total by PARTFUN1:def_2; ::_thesis: verum end; end; definition let I be set ; let f be ManySortedFunction of I; let x be ManySortedSet of I; :: original: .. redefine funcf .. x -> Function means :Def18: :: PRALG_1:def 18 ( dom it = I & ( for i being set st i in I holds for g being Function st g = f . i holds it . i = g . (x . i) ) ); compatibility for b1 being Function holds ( b1 = f .. x iff ( dom b1 = I & ( for i being set st i in I holds for g being Function st g = f . i holds b1 . i = g . (x . i) ) ) ) proof let M be Function; ::_thesis: ( M = f .. x iff ( dom M = I & ( for i being set st i in I holds for g being Function st g = f . i holds M . i = g . (x . i) ) ) ) hereby ::_thesis: ( dom M = I & ( for i being set st i in I holds for g being Function st g = f . i holds M . i = g . (x . i) ) implies M = f .. x ) assume A1: M = f .. x ; ::_thesis: ( dom M = I & ( for i being set st i in I holds for g being Function st g = f . i holds M . i = g . (x . i) ) ) hence A2: dom M = I by PARTFUN1:def_2; ::_thesis: for i being set st i in I holds for g being Function st g = f . i holds M . i = g . (x . i) dom M = dom f by A1, Def17; hence for i being set st i in I holds for g being Function st g = f . i holds M . i = g . (x . i) by A1, A2, Def17; ::_thesis: verum end; assume that A3: dom M = I and A4: for i being set st i in I holds for g being Function st g = f . i holds M . i = g . (x . i) ; ::_thesis: M = f .. x A5: dom f = I by PARTFUN1:def_2; then for i being set st i in dom f holds M . i = (f . i) . (x . i) by A4; hence M = f .. x by A3, A5, Def17; ::_thesis: verum end; end; :: deftheorem Def18 defines .. PRALG_1:def_18_:_ for I being set for f being ManySortedFunction of I for x being ManySortedSet of I for b4 being Function holds ( b4 = f .. x iff ( dom b4 = I & ( for i being set st i in I holds for g being Function st g = f . i holds b4 . i = g . (x . i) ) ) ); registration let J be non empty set ; let B be V2() ManySortedSet of J; let p be FinSequence of product B; cluster uncurry p -> [:(dom p),J:] -defined ; coherence uncurry p is [:(dom p),J:] -defined proof now__::_thesis:_uncurry_p_is_[:(dom_p),J:]_-defined set j = the Element of J; dom B = J by PARTFUN1:def_2; then B . the Element of J in rng B by FUNCT_1:def_3; then reconsider S = union (rng B) as non empty set by XBOOLE_1:3, ZFMISC_1:74; rng p c= Funcs (J,S) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in Funcs (J,S) ) A1: rng p c= product B by FINSEQ_1:def_4; assume x in rng p ; ::_thesis: x in Funcs (J,S) then consider f being Function such that A2: x = f and A3: dom f = dom B and A4: for y being set st y in dom B holds f . y in B . y by A1, CARD_3:def_5; A5: rng f c= S proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in S ) assume z in rng f ; ::_thesis: z in S then consider y being set such that A6: y in dom f and A7: z = f . y by FUNCT_1:def_3; B . y in rng B by A3, A6, FUNCT_1:def_3; then A8: B . y c= union (rng B) by ZFMISC_1:74; z in B . y by A3, A4, A6, A7; hence z in S by A8; ::_thesis: verum end; dom B = J by PARTFUN1:def_2; hence x in Funcs (J,S) by A2, A3, A5, FUNCT_2:def_2; ::_thesis: verum end; then dom (uncurry p) = [:(dom p),J:] by FUNCT_5:26; hence uncurry p is [:(dom p),J:] -defined by RELAT_1:def_18; ::_thesis: verum end; hence uncurry p is [:(dom p),J:] -defined ; ::_thesis: verum end; end; registration let J be non empty set ; let B be V2() ManySortedSet of J; let p be FinSequence of product B; cluster uncurry p -> [:(dom p),J:] -defined total for [:(dom p),J:] -defined Function; coherence for b1 being [:(dom p),J:] -defined Function st b1 = uncurry p holds b1 is total proof now__::_thesis:_for_b1_being_[:(dom_p),J:]_-defined_Function_st_b1_=_uncurry_p_holds_ b1_is_total set j = the Element of J; dom B = J by PARTFUN1:def_2; then B . the Element of J in rng B by FUNCT_1:def_3; then reconsider S = union (rng B) as non empty set by XBOOLE_1:3, ZFMISC_1:74; rng p c= Funcs (J,S) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in Funcs (J,S) ) A1: rng p c= product B by FINSEQ_1:def_4; assume x in rng p ; ::_thesis: x in Funcs (J,S) then consider f being Function such that A2: x = f and A3: dom f = dom B and A4: for y being set st y in dom B holds f . y in B . y by A1, CARD_3:def_5; A5: rng f c= S proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in S ) assume z in rng f ; ::_thesis: z in S then consider y being set such that A6: y in dom f and A7: z = f . y by FUNCT_1:def_3; B . y in rng B by A3, A6, FUNCT_1:def_3; then A8: B . y c= union (rng B) by ZFMISC_1:74; z in B . y by A3, A4, A6, A7; hence z in S by A8; ::_thesis: verum end; dom B = J by PARTFUN1:def_2; hence x in Funcs (J,S) by A2, A3, A5, FUNCT_2:def_2; ::_thesis: verum end; then dom (uncurry p) = [:(dom p),J:] by FUNCT_5:26; hence for b1 being [:(dom p),J:] -defined Function st b1 = uncurry p holds b1 is total by PARTFUN1:def_2; ::_thesis: verum end; hence for b1 being [:(dom p),J:] -defined Function st b1 = uncurry p holds b1 is total ; ::_thesis: verum end; end; registration let I, J be set ; let X be ManySortedSet of [:I,J:]; cluster ~ X -> [:J,I:] -defined ; coherence ~ X is [:J,I:] -defined proof dom X = [:I,J:] by PARTFUN1:def_2; then dom (~ X) = [:J,I:] by FUNCT_4:46; hence ~ X is [:J,I:] -defined by RELAT_1:def_18; ::_thesis: verum end; end; registration let I, J be set ; let X be ManySortedSet of [:I,J:]; cluster ~ X -> [:J,I:] -defined total for [:J,I:] -defined Function; coherence for b1 being [:J,I:] -defined Function st b1 = ~ X holds b1 is total proof dom X = [:I,J:] by PARTFUN1:def_2; then dom (~ X) = [:J,I:] by FUNCT_4:46; hence for b1 being [:J,I:] -defined Function st b1 = ~ X holds b1 is total by PARTFUN1:def_2; ::_thesis: verum end; end; registration let X be set ; let Y be non empty set ; let f be ManySortedSet of [:X,Y:]; cluster curry f -> X -defined ; coherence curry f is X -defined proof set a = curry f; ( dom f = [:X,Y:] & dom (curry f) = proj1 (dom f) ) by FUNCT_5:def_1, PARTFUN1:def_2; then dom (curry f) = X by FUNCT_5:9; hence curry f is X -defined by RELAT_1:def_18; ::_thesis: verum end; end; registration let X be set ; let Y be non empty set ; let f be ManySortedSet of [:X,Y:]; cluster curry f -> X -defined total for X -defined Function; coherence for b1 being X -defined Function st b1 = curry f holds b1 is total proof set a = curry f; ( dom f = [:X,Y:] & dom (curry f) = proj1 (dom f) ) by FUNCT_5:def_1, PARTFUN1:def_2; then dom (curry f) = X by FUNCT_5:9; hence for b1 being X -defined Function st b1 = curry f holds b1 is total by PARTFUN1:def_2; ::_thesis: verum end; end; definition let J be non empty set ; let B be V2() ManySortedSet of J; let O be equal-arity ManySortedOperation of B; func ComAr O -> Nat means :Def19: :: PRALG_1:def 19 for j being Element of J holds it = arity (O . j); existence ex b1 being Nat st for j being Element of J holds b1 = arity (O . j) proof set i = the Element of J; take arity (O . the Element of J) ; ::_thesis: for j being Element of J holds arity (O . the Element of J) = arity (O . j) let j be Element of J; ::_thesis: arity (O . the Element of J) = arity (O . j) thus arity (O . the Element of J) = arity (O . j) by Th11; ::_thesis: verum end; uniqueness for b1, b2 being Nat st ( for j being Element of J holds b1 = arity (O . j) ) & ( for j being Element of J holds b2 = arity (O . j) ) holds b1 = b2 proof set j = the Element of J; let n, m be Nat; ::_thesis: ( ( for j being Element of J holds n = arity (O . j) ) & ( for j being Element of J holds m = arity (O . j) ) implies n = m ) assume that A1: for j being Element of J holds n = arity (O . j) and A2: for j being Element of J holds m = arity (O . j) ; ::_thesis: n = m n = arity (O . the Element of J) by A1; hence n = m by A2; ::_thesis: verum end; end; :: deftheorem Def19 defines ComAr PRALG_1:def_19_:_ for J being non empty set for B being V2() ManySortedSet of J for O being equal-arity ManySortedOperation of B for b4 being Nat holds ( b4 = ComAr O iff for j being Element of J holds b4 = arity (O . j) ); definition let I be set ; let A be ManySortedSet of I; func EmptySeq A -> ManySortedSet of I means :Def20: :: PRALG_1:def 20 for i being set st i in I holds it . i = {} (A . i); existence ex b1 being ManySortedSet of I st for i being set st i in I holds b1 . i = {} (A . i) proof deffunc H1( set ) -> Element of bool (A . $1) = {} (A . $1); consider f being Function such that A1: ( dom f = I & ( for x being set st x in I holds f . x = H1(x) ) ) from FUNCT_1:sch_3(); reconsider f = f as ManySortedSet of I by A1, PARTFUN1:def_2, RELAT_1:def_18; take f ; ::_thesis: for i being set st i in I holds f . i = {} (A . i) thus for i being set st i in I holds f . i = {} (A . i) by A1; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds b1 . i = {} (A . i) ) & ( for i being set st i in I holds b2 . i = {} (A . i) ) holds b1 = b2 proof let X, Y be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds X . i = {} (A . i) ) & ( for i being set st i in I holds Y . i = {} (A . i) ) implies X = Y ) assume that A2: for i being set st i in I holds X . i = {} (A . i) and A3: for i being set st i in I holds Y . i = {} (A . i) ; ::_thesis: X = Y for i being set st i in I holds X . i = Y . i proof let i be set ; ::_thesis: ( i in I implies X . i = Y . i ) assume A4: i in I ; ::_thesis: X . i = Y . i then X . i = {} (A . i) by A2; hence X . i = Y . i by A3, A4; ::_thesis: verum end; hence X = Y by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def20 defines EmptySeq PRALG_1:def_20_:_ for I being set for A, b3 being ManySortedSet of I holds ( b3 = EmptySeq A iff for i being set st i in I holds b3 . i = {} (A . i) ); definition let J be non empty set ; let B be V2() ManySortedSet of J; let O be equal-arity ManySortedOperation of B; func[[:O:]] -> non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) means :: PRALG_1:def 21 ( dom it = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom it holds ( ( dom p = {} implies it . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds it . p = O .. (curry w) ) ) ) ); existence ex b1 being non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) st ( dom b1 = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom b1 holds ( ( dom p = {} implies b1 . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds b1 . p = O .. (curry w) ) ) ) ) proof set pr = product B; set ca = ComAr O; set ct = (ComAr O) -tuples_on (product B); defpred S1[ set , set ] means for p being Element of (product B) * st p = $1 holds ( ( dom p = {} implies $2 = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds $2 = O .. (curry w) ) ); set aa = { q where q is Element of (product B) * : len q = ComAr O } ; A1: for x being set st x in (ComAr O) -tuples_on (product B) holds ex y being set st ( y in product B & S1[x,y] ) proof let x be set ; ::_thesis: ( x in (ComAr O) -tuples_on (product B) implies ex y being set st ( y in product B & S1[x,y] ) ) assume x in (ComAr O) -tuples_on (product B) ; ::_thesis: ex y being set st ( y in product B & S1[x,y] ) then consider w being Element of (product B) * such that A2: x = w and A3: len w = ComAr O ; now__::_thesis:_(_(_dom_w_=_{}_&_ex_y_being_Function_st_ (_y_in_product_B_&_(_for_p_being_Element_of_(product_B)_*_st_p_=_x_holds_ (_(_dom_p_=_{}_implies_y_=_O_.._(EmptySeq_B)_)_&_(_dom_p_<>_{}_implies_for_Z_being_non_empty_set_ for_w_being_ManySortedSet_of_[:J,Z:]_st_Z_=_dom_p_&_w_=_~_(uncurry_p)_holds_ y_=_O_.._(curry_w)_)_)_)_)_)_or_(_dom_w_<>_{}_&_ex_y_being_Function_st_ (_y_in_product_B_&_(_for_l_being_Element_of_(product_B)_*_st_l_=_x_holds_ (_(_dom_l_=_{}_implies_y_=_O_.._(EmptySeq_B)_)_&_(_dom_l_<>_{}_implies_for_Z_being_non_empty_set_ for_w_being_ManySortedSet_of_[:J,Z:]_st_Z_=_dom_l_&_w_=_~_(uncurry_l)_holds_ y_=_O_.._(curry_w)_)_)_)_)_)_) percases ( dom w = {} or dom w <> {} ) ; caseA4: dom w = {} ; ::_thesis: ex y being Function st ( y in product B & ( for p being Element of (product B) * st p = x holds ( ( dom p = {} implies y = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds y = O .. (curry w) ) ) ) ) A5: for z being set st z in dom B holds (O .. (EmptySeq B)) . z in B . z proof let z be set ; ::_thesis: ( z in dom B implies (O .. (EmptySeq B)) . z in B . z ) assume z in dom B ; ::_thesis: (O .. (EmptySeq B)) . z in B . z then reconsider j = z as Element of J by PARTFUN1:def_2; A6: rng (O . j) c= B . j by RELAT_1:def_19; w = {} by A4; then arity (O . j) = 0 by A3, Def19; then dom (O . j) = 0 -tuples_on (B . j) by MARGREL1:22 .= {(<*> (B . j))} by FINSEQ_2:94 ; then {} (B . j) in dom (O . j) by TARSKI:def_1; then A7: (O . j) . ({} (B . j)) in rng (O . j) by FUNCT_1:def_3; (O .. (EmptySeq B)) . z = (O . j) . ((EmptySeq B) . j) by Def18 .= (O . j) . ({} (B . j)) by Def20 ; hence (O .. (EmptySeq B)) . z in B . z by A7, A6; ::_thesis: verum end; take y = O .. (EmptySeq B); ::_thesis: ( y in product B & ( for p being Element of (product B) * st p = x holds ( ( dom p = {} implies y = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds y = O .. (curry w) ) ) ) ) dom (O .. (EmptySeq B)) = J by PARTFUN1:def_2 .= dom B by PARTFUN1:def_2 ; hence y in product B by A5, CARD_3:def_5; ::_thesis: for p being Element of (product B) * st p = x holds ( ( dom p = {} implies y = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds y = O .. (curry w) ) ) let p be Element of (product B) * ; ::_thesis: ( p = x implies ( ( dom p = {} implies y = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds y = O .. (curry w) ) ) ) assume p = x ; ::_thesis: ( ( dom p = {} implies y = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds y = O .. (curry w) ) ) hence ( ( dom p = {} implies y = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds y = O .. (curry w) ) ) by A2, A4; ::_thesis: verum end; case dom w <> {} ; ::_thesis: ex y being Function st ( y in product B & ( for l being Element of (product B) * st l = x holds ( ( dom l = {} implies y = O .. (EmptySeq B) ) & ( dom l <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom l & w = ~ (uncurry l) holds y = O .. (curry w) ) ) ) ) then reconsider Z = dom w as non empty set ; reconsider p = ~ (uncurry w) as ManySortedSet of [:J,Z:] ; take y = O .. (curry p); ::_thesis: ( y in product B & ( for l being Element of (product B) * st l = x holds ( ( dom l = {} implies y = O .. (EmptySeq B) ) & ( dom l <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom l & w = ~ (uncurry l) holds y = O .. (curry w) ) ) ) ) A8: for z being set st z in dom B holds (O .. (curry p)) . z in B . z proof let z be set ; ::_thesis: ( z in dom B implies (O .. (curry p)) . z in B . z ) assume z in dom B ; ::_thesis: (O .. (curry p)) . z in B . z then reconsider j = z as Element of J by PARTFUN1:def_2; A9: dom p = [:J,Z:] by PARTFUN1:def_2; then proj1 (dom p) = J by FUNCT_5:9; then consider g being Function such that A10: (curry p) . j = g and A11: dom g = proj2 ((dom p) /\ [:{j},(proj2 (dom p)):]) and A12: for y being set st y in dom g holds g . y = p . (j,y) by FUNCT_5:def_1; proj2 (dom p) = Z by A9, FUNCT_5:9; then A13: dom g = proj2 [:(J /\ {j}),(Z /\ Z):] by A9, A11, ZFMISC_1:100 .= proj2 [:{j},Z:] by ZFMISC_1:46 .= dom w by FUNCT_5:9 .= Seg (len w) by FINSEQ_1:def_3 ; then reconsider g = g as FinSequence by FINSEQ_1:def_2; rng g c= B . j proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in B . j ) assume y in rng g ; ::_thesis: y in B . j then consider x being set such that A14: x in dom g and A15: g . x = y by FUNCT_1:def_3; ( dom (uncurry w) = [:(dom w),J:] & dom g = dom w ) by A13, FINSEQ_1:def_3, PARTFUN1:def_2; then A16: [x,j] in dom (uncurry w) by A14, ZFMISC_1:87; then consider a being set , f being Function, b being set such that A17: [x,j] = [a,b] and A18: a in dom w and A19: f = w . a and A20: b in dom f by FUNCT_5:def_2; y = (~ (uncurry w)) . (j,x) by A12, A14, A15; then A21: y = (uncurry w) . (x,j) by A16, FUNCT_4:def_2; ( [a,b] `1 = a & [a,b] `2 = j ) by A17, MCART_1:7; then A22: y = f . j by A16, A21, A17, A19, FUNCT_5:def_2; A23: j = b by A17, XTUPLE_0:1; A24: ( rng w c= product B & w . a in rng w ) by A18, FINSEQ_1:def_4, FUNCT_1:def_3; then dom f = dom B by A19, CARD_3:9; hence y in B . j by A19, A20, A23, A24, A22, CARD_3:9; ::_thesis: verum end; then reconsider g = g as FinSequence of B . j by FINSEQ_1:def_4; reconsider g = g as Element of (B . j) * by FINSEQ_1:def_11; arity (O . j) = ComAr O by Def19; then A25: dom (O . j) = (ComAr O) -tuples_on (B . j) by MARGREL1:22 .= { s where s is Element of (B . j) * : len s = ComAr O } ; len g = len w by A13, FINSEQ_1:def_3; then g in dom (O . j) by A3, A25; then A26: (O . j) . g in rng (O . j) by FUNCT_1:def_3; ( (O .. (curry p)) . z = (O . j) . ((curry p) . j) & rng (O . j) c= B . j ) by Def18, RELAT_1:def_19; hence (O .. (curry p)) . z in B . z by A10, A26; ::_thesis: verum end; dom (O .. (curry p)) = J by PARTFUN1:def_2 .= dom B by PARTFUN1:def_2 ; hence y in product B by A8, CARD_3:def_5; ::_thesis: for l being Element of (product B) * st l = x holds ( ( dom l = {} implies y = O .. (EmptySeq B) ) & ( dom l <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom l & w = ~ (uncurry l) holds y = O .. (curry w) ) ) let l be Element of (product B) * ; ::_thesis: ( l = x implies ( ( dom l = {} implies y = O .. (EmptySeq B) ) & ( dom l <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom l & w = ~ (uncurry l) holds y = O .. (curry w) ) ) ) assume l = x ; ::_thesis: ( ( dom l = {} implies y = O .. (EmptySeq B) ) & ( dom l <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom l & w = ~ (uncurry l) holds y = O .. (curry w) ) ) hence ( ( dom l = {} implies y = O .. (EmptySeq B) ) & ( dom l <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom l & w = ~ (uncurry l) holds y = O .. (curry w) ) ) by A2; ::_thesis: verum end; end; end; hence ex y being set st ( y in product B & S1[x,y] ) ; ::_thesis: verum end; consider f being Function such that A27: ( dom f = (ComAr O) -tuples_on (product B) & rng f c= product B & ( for x being set st x in (ComAr O) -tuples_on (product B) holds S1[x,f . x] ) ) from FUNCT_1:sch_5(A1); ComAr O in NAT by ORDINAL1:def_12; then (ComAr O) -tuples_on (product B) in { (n -tuples_on (product B)) where n is Element of NAT : verum } ; then A28: (ComAr O) -tuples_on (product B) c= union { (m -tuples_on (product B)) where m is Element of NAT : verum } by ZFMISC_1:74; then dom f c= (product B) * by A27, FINSEQ_2:108; then reconsider f = f as PartFunc of ((product B) *),(product B) by A27, RELSET_1:4; A29: f is homogeneous proof let x, y be FinSequence; :: according to MARGREL1:def_1,MARGREL1:def_21 ::_thesis: ( not x in proj1 f or not y in proj1 f or len x = len y ) assume A30: ( x in dom f & y in dom f ) ; ::_thesis: len x = len y then reconsider x1 = x, y1 = y as Element of (product B) * by A27, A28, FINSEQ_2:108; ( ex w being Element of (product B) * st ( x1 = w & len w = ComAr O ) & ex w being Element of (product B) * st ( y1 = w & len w = ComAr O ) ) by A27, A30; hence len x = len y ; ::_thesis: verum end; f is quasi_total proof let x, y be FinSequence of product B; :: according to MARGREL1:def_22 ::_thesis: ( not len x = len y or not x in proj1 f or y in proj1 f ) assume that A31: len x = len y and A32: x in dom f ; ::_thesis: y in proj1 f reconsider x1 = x, y1 = y as Element of (product B) * by FINSEQ_1:def_11; ex w being Element of (product B) * st ( x1 = w & len w = ComAr O ) by A27, A32; then y1 in { q where q is Element of (product B) * : len q = ComAr O } by A31; hence y in proj1 f by A27; ::_thesis: verum end; then reconsider f = f as non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) by A27, A29; take f ; ::_thesis: ( dom f = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom f holds ( ( dom p = {} implies f . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds f . p = O .. (curry w) ) ) ) ) thus dom f = (ComAr O) -tuples_on (product B) by A27; ::_thesis: for p being Element of (product B) * st p in dom f holds ( ( dom p = {} implies f . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds f . p = O .. (curry w) ) ) let p be Element of (product B) * ; ::_thesis: ( p in dom f implies ( ( dom p = {} implies f . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds f . p = O .. (curry w) ) ) ) assume p in dom f ; ::_thesis: ( ( dom p = {} implies f . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds f . p = O .. (curry w) ) ) hence ( ( dom p = {} implies f . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds f . p = O .. (curry w) ) ) by A27; ::_thesis: verum end; uniqueness for b1, b2 being non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) st dom b1 = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom b1 holds ( ( dom p = {} implies b1 . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds b1 . p = O .. (curry w) ) ) ) & dom b2 = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom b2 holds ( ( dom p = {} implies b2 . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds b2 . p = O .. (curry w) ) ) ) holds b1 = b2 proof set pr = product B; set ca = ComAr O; let f, g be non empty homogeneous quasi_total PartFunc of ((product B) *),(product B); ::_thesis: ( dom f = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom f holds ( ( dom p = {} implies f . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds f . p = O .. (curry w) ) ) ) & dom g = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom g holds ( ( dom p = {} implies g . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds g . p = O .. (curry w) ) ) ) implies f = g ) assume that A33: dom f = (ComAr O) -tuples_on (product B) and A34: for p being Element of (product B) * st p in dom f holds ( ( dom p = {} implies f . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds f . p = O .. (curry w) ) ) and A35: dom g = (ComAr O) -tuples_on (product B) and A36: for p being Element of (product B) * st p in dom g holds ( ( dom p = {} implies g . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds g . p = O .. (curry w) ) ) ; ::_thesis: f = g for x being set st x in (ComAr O) -tuples_on (product B) holds f . x = g . x proof let x be set ; ::_thesis: ( x in (ComAr O) -tuples_on (product B) implies f . x = g . x ) assume A37: x in (ComAr O) -tuples_on (product B) ; ::_thesis: f . x = g . x then consider s being Element of (product B) * such that A38: x = s and len s = ComAr O ; now__::_thesis:_(_(_dom_s_=_{}_&_f_._x_=_g_._x_)_or_(_dom_s_<>_{}_&_f_._x_=_g_._x_)_) percases ( dom s = {} or dom s <> {} ) ; caseA39: dom s = {} ; ::_thesis: f . x = g . x then f . s = O .. (EmptySeq B) by A33, A34, A37, A38; hence f . x = g . x by A35, A36, A37, A38, A39; ::_thesis: verum end; case dom s <> {} ; ::_thesis: f . x = g . x then reconsider Z = dom s as non empty set ; reconsider w = ~ (uncurry s) as ManySortedSet of [:J,Z:] ; f . s = O .. (curry w) by A33, A34, A37, A38; hence f . x = g . x by A35, A36, A37, A38; ::_thesis: verum end; end; end; hence f . x = g . x ; ::_thesis: verum end; hence f = g by A33, A35, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem defines [[: PRALG_1:def_21_:_ for J being non empty set for B being V2() ManySortedSet of J for O being equal-arity ManySortedOperation of B for b4 being non empty homogeneous quasi_total PartFunc of ((product B) *),(product B) holds ( b4 = [[:O:]] iff ( dom b4 = (ComAr O) -tuples_on (product B) & ( for p being Element of (product B) * st p in dom b4 holds ( ( dom p = {} implies b4 . p = O .. (EmptySeq B) ) & ( dom p <> {} implies for Z being non empty set for w being ManySortedSet of [:J,Z:] st Z = dom p & w = ~ (uncurry p) holds b4 . p = O .. (curry w) ) ) ) ) ); definition let J be non empty set ; let A be Univ_Alg-yielding equal-signature ManySortedSet of J; let n be Nat; assume A1: n in dom (ComSign A) ; func ProdOp (A,n) -> equal-arity ManySortedOperation of Carrier A means :: PRALG_1:def 22 for j being Element of J for o being operation of (A . j) st the charact of (A . j) . n = o holds it . j = o; existence ex b1 being equal-arity ManySortedOperation of Carrier A st for j being Element of J for o being operation of (A . j) st the charact of (A . j) . n = o holds b1 . j = o proof defpred S1[ set , set ] means for j being Element of J st $1 = j holds for o being operation of (A . j) st the charact of (A . j) . n = o holds $2 = o; A2: for x being set st x in J holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in J implies ex y being set st S1[x,y] ) assume x in J ; ::_thesis: ex y being set st S1[x,y] then reconsider x1 = x as Element of J ; n in dom (signature (A . x1)) by A1, Def14; then n in Seg (len (signature (A . x1))) by FINSEQ_1:def_3; then n in Seg (len the charact of (A . x1)) by UNIALG_1:def_4; then n in dom the charact of (A . x1) by FINSEQ_1:def_3; then reconsider o = the charact of (A . x1) . n as operation of (A . x1) by FUNCT_1:def_3; take o ; ::_thesis: S1[x,o] let j be Element of J; ::_thesis: ( x = j implies for o being operation of (A . j) st the charact of (A . j) . n = o holds o = o ) assume A3: x = j ; ::_thesis: for o being operation of (A . j) st the charact of (A . j) . n = o holds o = o let o1 be operation of (A . j); ::_thesis: ( the charact of (A . j) . n = o1 implies o = o1 ) assume the charact of (A . j) . n = o1 ; ::_thesis: o = o1 hence o = o1 by A3; ::_thesis: verum end; consider f being Function such that A4: ( dom f = J & ( for x being set st x in J holds S1[x,f . x] ) ) from CLASSES1:sch_1(A2); reconsider f = f as ManySortedSet of J by A4, 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 x1 = x as Element of J by A4; n in dom (signature (A . x1)) by A1, Def14; then n in Seg (len (signature (A . x1))) by FINSEQ_1:def_3; then n in Seg (len the charact of (A . x1)) by UNIALG_1:def_4; then n in dom the charact of (A . x1) by FINSEQ_1:def_3; then reconsider o = the charact of (A . x1) . n as operation of (A . x1) by FUNCT_1:def_3; f . x = o by A4; hence f . x is Function ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of J by FUNCOP_1:def_6; for j being Element of J holds f . j is non empty homogeneous quasi_total PartFunc of (((Carrier A) . j) *),((Carrier A) . j) proof let j be Element of J; ::_thesis: f . j is non empty homogeneous quasi_total PartFunc of (((Carrier A) . j) *),((Carrier A) . j) n in dom (signature (A . j)) by A1, Def14; then n in Seg (len (signature (A . j))) by FINSEQ_1:def_3; then n in Seg (len the charact of (A . j)) by UNIALG_1:def_4; then n in dom the charact of (A . j) by FINSEQ_1:def_3; then reconsider o = the charact of (A . j) . n as operation of (A . j) by FUNCT_1:def_3; ( ex R being 1-sorted st ( R = A . j & (Carrier A) . j = the carrier of R ) & f . j = o ) by A4, Def13; hence f . j is non empty homogeneous quasi_total PartFunc of (((Carrier A) . j) *),((Carrier A) . j) ; ::_thesis: verum end; then reconsider f = f as ManySortedOperation of Carrier A by Def15; for i, j being Element of J holds arity (f . i) = arity (f . j) proof let i, j be Element of J; ::_thesis: arity (f . i) = arity (f . j) A5: n in dom (signature (A . j)) by A1, Def14; then A6: n in Seg (len (signature (A . j))) by FINSEQ_1:def_3; then n in Seg (len the charact of (A . j)) by UNIALG_1:def_4; then n in dom the charact of (A . j) by FINSEQ_1:def_3; then reconsider o = the charact of (A . j) . n as operation of (A . j) by FUNCT_1:def_3; A7: (signature (A . j)) . n = arity o by A5, UNIALG_1:def_4; dom A = J by PARTFUN1:def_2; then A8: signature (A . i) = signature (A . j) by Def12; then n in Seg (len the charact of (A . i)) by A6, UNIALG_1:def_4; then n in dom the charact of (A . i) by FINSEQ_1:def_3; then reconsider o1 = the charact of (A . i) . n as operation of (A . i) by FUNCT_1:def_3; ( arity (f . j) = arity o & f . i = o1 ) by A4; hence arity (f . i) = arity (f . j) by A8, A5, A7, UNIALG_1:def_4; ::_thesis: verum end; then reconsider f = f as equal-arity ManySortedOperation of Carrier A by Th11; take f ; ::_thesis: for j being Element of J for o being operation of (A . j) st the charact of (A . j) . n = o holds f . j = o let j be Element of J; ::_thesis: for o being operation of (A . j) st the charact of (A . j) . n = o holds f . j = o let o be operation of (A . j); ::_thesis: ( the charact of (A . j) . n = o implies f . j = o ) assume the charact of (A . j) . n = o ; ::_thesis: f . j = o hence f . j = o by A4; ::_thesis: verum end; uniqueness for b1, b2 being equal-arity ManySortedOperation of Carrier A st ( for j being Element of J for o being operation of (A . j) st the charact of (A . j) . n = o holds b1 . j = o ) & ( for j being Element of J for o being operation of (A . j) st the charact of (A . j) . n = o holds b2 . j = o ) holds b1 = b2 proof let O1, O2 be equal-arity ManySortedOperation of Carrier A; ::_thesis: ( ( for j being Element of J for o being operation of (A . j) st the charact of (A . j) . n = o holds O1 . j = o ) & ( for j being Element of J for o being operation of (A . j) st the charact of (A . j) . n = o holds O2 . j = o ) implies O1 = O2 ) assume that A9: for j being Element of J for o being operation of (A . j) st the charact of (A . j) . n = o holds O1 . j = o and A10: for j being Element of J for o being operation of (A . j) st the charact of (A . j) . n = o holds O2 . j = o ; ::_thesis: O1 = O2 for x being set st x in J holds O1 . x = O2 . x proof let x be set ; ::_thesis: ( x in J implies O1 . x = O2 . x ) assume x in J ; ::_thesis: O1 . x = O2 . x then reconsider x1 = x as Element of J ; n in dom (signature (A . x1)) by A1, Def14; then n in Seg (len (signature (A . x1))) by FINSEQ_1:def_3; then n in Seg (len the charact of (A . x1)) by UNIALG_1:def_4; then n in dom the charact of (A . x1) by FINSEQ_1:def_3; then reconsider o = the charact of (A . x1) . n as operation of (A . x1) by FUNCT_1:def_3; O1 . x1 = o by A9; hence O1 . x = O2 . x by A10; ::_thesis: verum end; hence O1 = O2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem defines ProdOp PRALG_1:def_22_:_ for J being non empty set for A being Univ_Alg-yielding equal-signature ManySortedSet of J for n being Nat st n in dom (ComSign A) holds for b4 being equal-arity ManySortedOperation of Carrier A holds ( b4 = ProdOp (A,n) iff for j being Element of J for o being operation of (A . j) st the charact of (A . j) . n = o holds b4 . j = o ); definition let J be non empty set ; let A be Univ_Alg-yielding equal-signature ManySortedSet of J; func ProdOpSeq A -> PFuncFinSequence of (product (Carrier A)) means :Def23: :: PRALG_1:def 23 ( len it = len (ComSign A) & ( for n being Nat st n in dom it holds it . n = [[:(ProdOp (A,n)):]] ) ); existence ex b1 being PFuncFinSequence of (product (Carrier A)) st ( len b1 = len (ComSign A) & ( for n being Nat st n in dom b1 holds b1 . n = [[:(ProdOp (A,n)):]] ) ) proof set f = ComSign A; defpred S1[ Nat, set ] means $2 = [[:(ProdOp (A,$1)):]]; A1: for k being Nat st k in Seg (len (ComSign A)) holds ex x being Element of PFuncs (((product (Carrier A)) *),(product (Carrier A))) st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len (ComSign A)) implies ex x being Element of PFuncs (((product (Carrier A)) *),(product (Carrier A))) st S1[k,x] ) assume k in Seg (len (ComSign A)) ; ::_thesis: ex x being Element of PFuncs (((product (Carrier A)) *),(product (Carrier A))) st S1[k,x] reconsider a = [[:(ProdOp (A,k)):]] as Element of PFuncs (((product (Carrier A)) *),(product (Carrier A))) by PARTFUN1:45; take a ; ::_thesis: S1[k,a] thus S1[k,a] ; ::_thesis: verum end; consider p being FinSequence of PFuncs (((product (Carrier A)) *),(product (Carrier A))) such that A2: ( dom p = Seg (len (ComSign A)) & ( for k being Nat st k in Seg (len (ComSign A)) holds S1[k,p . k] ) ) from FINSEQ_1:sch_5(A1); reconsider p = p as PFuncFinSequence of (product (Carrier A)) ; take p ; ::_thesis: ( len p = len (ComSign A) & ( for n being Nat st n in dom p holds p . n = [[:(ProdOp (A,n)):]] ) ) thus len p = len (ComSign A) by A2, FINSEQ_1:def_3; ::_thesis: for n being Nat st n in dom p holds p . n = [[:(ProdOp (A,n)):]] let n be Nat; ::_thesis: ( n in dom p implies p . n = [[:(ProdOp (A,n)):]] ) assume n in dom p ; ::_thesis: p . n = [[:(ProdOp (A,n)):]] hence p . n = [[:(ProdOp (A,n)):]] by A2; ::_thesis: verum end; uniqueness for b1, b2 being PFuncFinSequence of (product (Carrier A)) st len b1 = len (ComSign A) & ( for n being Nat st n in dom b1 holds b1 . n = [[:(ProdOp (A,n)):]] ) & len b2 = len (ComSign A) & ( for n being Nat st n in dom b2 holds b2 . n = [[:(ProdOp (A,n)):]] ) holds b1 = b2 proof let x, y be PFuncFinSequence of (product (Carrier A)); ::_thesis: ( len x = len (ComSign A) & ( for n being Nat st n in dom x holds x . n = [[:(ProdOp (A,n)):]] ) & len y = len (ComSign A) & ( for n being Nat st n in dom y holds y . n = [[:(ProdOp (A,n)):]] ) implies x = y ) assume that A3: len x = len (ComSign A) and A4: for n being Nat st n in dom x holds x . n = [[:(ProdOp (A,n)):]] and A5: len y = len (ComSign A) and A6: for n being Nat st n in dom y holds y . n = [[:(ProdOp (A,n)):]] ; ::_thesis: x = y A7: dom x = Seg (len (ComSign A)) by A3, FINSEQ_1:def_3; now__::_thesis:_for_n_being_Nat_st_n_in_dom_x_holds_ x_._n_=_y_._n let n be Nat; ::_thesis: ( n in dom x implies x . n = y . n ) assume n in dom x ; ::_thesis: x . n = y . n then ( n in dom y & x . n = [[:(ProdOp (A,n)):]] ) by A4, A5, A7, FINSEQ_1:def_3; hence x . n = y . n by A6; ::_thesis: verum end; hence x = y by A3, A5, FINSEQ_2:9; ::_thesis: verum end; end; :: deftheorem Def23 defines ProdOpSeq PRALG_1:def_23_:_ for J being non empty set for A being Univ_Alg-yielding equal-signature ManySortedSet of J for b3 being PFuncFinSequence of (product (Carrier A)) holds ( b3 = ProdOpSeq A iff ( len b3 = len (ComSign A) & ( for n being Nat st n in dom b3 holds b3 . n = [[:(ProdOp (A,n)):]] ) ) ); definition let J be non empty set ; let A be Univ_Alg-yielding equal-signature ManySortedSet of J; func ProdUnivAlg A -> strict Universal_Algebra equals :: PRALG_1:def 24 UAStr(# (product (Carrier A)),(ProdOpSeq A) #); coherence UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is strict Universal_Algebra proof set j = the Element of J; set ua = UAStr(# (product (Carrier A)),(ProdOpSeq A) #); set pr = product (Carrier A); for n being Nat for h being PartFunc of ((product (Carrier A)) *),(product (Carrier A)) st n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & h = the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n holds h is quasi_total proof let n be Nat; ::_thesis: for h being PartFunc of ((product (Carrier A)) *),(product (Carrier A)) st n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & h = the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n holds h is quasi_total let h be PartFunc of ((product (Carrier A)) *),(product (Carrier A)); ::_thesis: ( n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & h = the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n implies h is quasi_total ) assume that A1: n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) and A2: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = h ; ::_thesis: h is quasi_total the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = [[:(ProdOp (A,n)):]] by A1, Def23; hence h is quasi_total by A2; ::_thesis: verum end; then A3: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is quasi_total by MARGREL1:def_24; for n being Nat for h being PartFunc of ((product (Carrier A)) *),(product (Carrier A)) st n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & h = the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n holds h is homogeneous proof let n be Nat; ::_thesis: for h being PartFunc of ((product (Carrier A)) *),(product (Carrier A)) st n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & h = the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n holds h is homogeneous let h be PartFunc of ((product (Carrier A)) *),(product (Carrier A)); ::_thesis: ( n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & h = the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n implies h is homogeneous ) assume that A4: n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) and A5: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = h ; ::_thesis: h is homogeneous the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = [[:(ProdOp (A,n)):]] by A4, Def23; hence h is homogeneous by A5; ::_thesis: verum end; then A6: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is homogeneous by MARGREL1:def_23; for n being set st n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) holds not the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n is empty proof let n be set ; ::_thesis: ( n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) implies not the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n is empty ) assume A7: n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) ; ::_thesis: not the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n is empty then reconsider n9 = n as Element of NAT ; the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = [[:(ProdOp (A,n9)):]] by A7, Def23; hence not the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n is empty ; ::_thesis: verum end; then A8: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is non-empty by FUNCT_1:def_9; len the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) = len (ComSign A) by Def23 .= len (signature (A . the Element of J)) by Def14 .= len the charact of (A . the Element of J) by UNIALG_1:def_4 ; then the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) <> {} ; hence UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is strict Universal_Algebra by A3, A6, A8, UNIALG_1:def_1, UNIALG_1:def_2, UNIALG_1:def_3; ::_thesis: verum end; end; :: deftheorem defines ProdUnivAlg PRALG_1:def_24_:_ for J being non empty set for A being Univ_Alg-yielding equal-signature ManySortedSet of J holds ProdUnivAlg A = UAStr(# (product (Carrier A)),(ProdOpSeq A) #);