:: FOMODEL0 semantic presentation begin definition let X be set ; let f be Function; attrf is X -one-to-one means :DefInj1: :: FOMODEL0:def 1 f | X is one-to-one ; end; :: deftheorem DefInj1 defines -one-to-one FOMODEL0:def_1_:_ for X being set for f being Function holds ( f is X -one-to-one iff f | X is one-to-one ); definition let D be non empty set ; let f be BinOp of D; let X be set ; attrX is f -unambiguous means :DefUnambiguous1: :: FOMODEL0:def 2 f is [:X,D:] -one-to-one ; end; :: deftheorem DefUnambiguous1 defines -unambiguous FOMODEL0:def_2_:_ for D being non empty set for f being BinOp of D for X being set holds ( X is f -unambiguous iff f is [:X,D:] -one-to-one ); definition let D be non empty set ; let X be set ; attrX is D -prefix means :DefPrefix: :: FOMODEL0:def 3 X is D -concatenation -unambiguous ; end; :: deftheorem DefPrefix defines -prefix FOMODEL0:def_3_:_ for D being non empty set for X being set holds ( X is D -prefix iff X is D -concatenation -unambiguous ); definition let D be set ; funcD -pr1 -> BinOp of D equals :: FOMODEL0:def 4 pr1 (D,D); coherence pr1 (D,D) is BinOp of D ; end; :: deftheorem defines -pr1 FOMODEL0:def_4_:_ for D being set holds D -pr1 = pr1 (D,D); Lm45: for Y being set for g being Function st g is Y -valued & g is FinSequence-like holds g is FinSequence of Y proof let Y be set ; ::_thesis: for g being Function st g is Y -valued & g is FinSequence-like holds g is FinSequence of Y let g be Function; ::_thesis: ( g is Y -valued & g is FinSequence-like implies g is FinSequence of Y ) set f = g; set X = Y; assume B0: ( g is Y -valued & g is FinSequence-like ) ; ::_thesis: g is FinSequence of Y then reconsider p = g as FinSequence ; rng p c= Y by B0, RELAT_1:def_19; hence g is FinSequence of Y by FINSEQ_1:def_4; ::_thesis: verum end; Lm28: for Y, A, B being set st Y c= Funcs (A,B) holds union Y c= [:A,B:] proof let Y, A, B be set ; ::_thesis: ( Y c= Funcs (A,B) implies union Y c= [:A,B:] ) set AB = [:A,B:]; set F = Funcs (A,B); set X = Y; assume Y c= Funcs (A,B) ; ::_thesis: union Y c= [:A,B:] then ( Y c= Funcs (A,B) & Funcs (A,B) c= bool [:A,B:] ) by FRAENKEL:2; then reconsider XX = Y as Subset of (bool [:A,B:]) by XBOOLE_1:1; union XX is Subset of [:A,B:] ; hence union Y c= [:A,B:] ; ::_thesis: verum end; LmOneOne: for X being set for f being Function holds ( f is X -one-to-one iff for x, y being set st x in (dom f) /\ X & y in (dom f) /\ X & f . x = f . y holds x = y ) proof let X be set ; ::_thesis: for f being Function holds ( f is X -one-to-one iff for x, y being set st x in (dom f) /\ X & y in (dom f) /\ X & f . x = f . y holds x = y ) let f be Function; ::_thesis: ( f is X -one-to-one iff for x, y being set st x in (dom f) /\ X & y in (dom f) /\ X & f . x = f . y holds x = y ) set g = f | X; thus ( f is X -one-to-one implies for x, y being set st x in (dom f) /\ X & y in (dom f) /\ X & f . x = f . y holds x = y ) ::_thesis: ( ( for x, y being set st x in (dom f) /\ X & y in (dom f) /\ X & f . x = f . y holds x = y ) implies f is X -one-to-one ) proof assume f is X -one-to-one ; ::_thesis: for x, y being set st x in (dom f) /\ X & y in (dom f) /\ X & f . x = f . y holds x = y then B1: f | X is one-to-one by DefInj1; let x, y be set ; ::_thesis: ( x in (dom f) /\ X & y in (dom f) /\ X & f . x = f . y implies x = y ) assume x in (dom f) /\ X ; ::_thesis: ( not y in (dom f) /\ X or not f . x = f . y or x = y ) then C3: x in dom (f | X) by RELAT_1:61; assume y in (dom f) /\ X ; ::_thesis: ( not f . x = f . y or x = y ) then C4: y in dom (f | X) by RELAT_1:61; assume f . x = f . y ; ::_thesis: x = y then ( (f | X) . x = f . x & (f | X) . y = f . y & f . x = f . y ) by C3, C4, FUNCT_1:47; hence x = y by B1, C3, C4, FUNCT_1:def_4; ::_thesis: verum end; assume A1: for x, y being set st x in (dom f) /\ X & y in (dom f) /\ X & f . x = f . y holds x = y ; ::_thesis: f is X -one-to-one now__::_thesis:_for_x,_y_being_set_st_x_in_dom_(f_|_X)_&_y_in_dom_(f_|_X)_&_(f_|_X)_._x_=_(f_|_X)_._y_holds_ x_=_y let x, y be set ; ::_thesis: ( x in dom (f | X) & y in dom (f | X) & (f | X) . x = (f | X) . y implies x = y ) assume B1: ( x in dom (f | X) & y in dom (f | X) & (f | X) . x = (f | X) . y ) ; ::_thesis: x = y then ( (f | X) . x = f . x & (f | X) . y = f . y & (f | X) . x = (f | X) . y ) by FUNCT_1:47; then ( x in (dom f) /\ X & y in (dom f) /\ X & f . x = f . y ) by B1, RELAT_1:61; hence x = y by A1; ::_thesis: verum end; then f | X is one-to-one by FUNCT_1:def_4; hence f is X -one-to-one by DefInj1; ::_thesis: verum end; Lm12: for D being non empty set for A, B being set for f being BinOp of D st A c= B & f is B -one-to-one holds f is A -one-to-one proof let D be non empty set ; ::_thesis: for A, B being set for f being BinOp of D st A c= B & f is B -one-to-one holds f is A -one-to-one let A, B be set ; ::_thesis: for f being BinOp of D st A c= B & f is B -one-to-one holds f is A -one-to-one let f be BinOp of D; ::_thesis: ( A c= B & f is B -one-to-one implies f is A -one-to-one ) assume ( A c= B & f is B -one-to-one ) ; ::_thesis: f is A -one-to-one then ( f | B is one-to-one & f | A = (f | B) | A ) by DefInj1, FUNCT_1:51; then ( (f | B) | A is one-to-one & f | A = (f | B) | A ) by FUNCT_1:52; hence f is A -one-to-one by DefInj1; ::_thesis: verum end; Lm18: for A, B being set for m, n being Nat st m -tuples_on A meets n -tuples_on B holds m = n proof let A, B be set ; ::_thesis: for m, n being Nat st m -tuples_on A meets n -tuples_on B holds m = n let m, n be Nat; ::_thesis: ( m -tuples_on A meets n -tuples_on B implies m = n ) assume m -tuples_on A meets n -tuples_on B ; ::_thesis: m = n then not (m -tuples_on A) /\ (n -tuples_on B) is empty by XBOOLE_0:def_7; then consider p being set such that B1: p in (m -tuples_on A) /\ (n -tuples_on B) by XBOOLE_0:def_1; B2: ( p in m -tuples_on A & p in n -tuples_on B ) by B1, XBOOLE_0:def_4; reconsider pA = p as m -element FinSequence by B2, FINSEQ_2:141; reconsider pB = p as n -element FinSequence by B2, FINSEQ_2:141; m = len pA by CARD_1:def_7 .= len pB .= n by CARD_1:def_7 ; hence m = n ; ::_thesis: verum end; Lm21: for i being Nat for Y being set holds i -tuples_on Y = Funcs ((Seg i),Y) proof let i be Nat; ::_thesis: for Y being set holds i -tuples_on Y = Funcs ((Seg i),Y) let Y be set ; ::_thesis: i -tuples_on Y = Funcs ((Seg i),Y) percases ( Y is empty or not Y is empty ) ; supposeB1: Y is empty ; ::_thesis: i -tuples_on Y = Funcs ((Seg i),Y) percases ( i is zero or not i is zero ) ; suppose i is zero ; ::_thesis: i -tuples_on Y = Funcs ((Seg i),Y) then ( i is zero & Seg i = {} ) ; then ( Funcs ((Seg i),Y) = {{}} & i -tuples_on Y = {{}} ) by COMPUT_1:5, FUNCT_5:57; hence i -tuples_on Y = Funcs ((Seg i),Y) ; ::_thesis: verum end; suppose not i is zero ; ::_thesis: i -tuples_on Y = Funcs ((Seg i),Y) then ( Funcs ((Seg i),Y) = {} & i -tuples_on Y = {} ) by B1, FINSEQ_3:119; hence i -tuples_on Y = Funcs ((Seg i),Y) ; ::_thesis: verum end; end; end; suppose not Y is empty ; ::_thesis: i -tuples_on Y = Funcs ((Seg i),Y) then reconsider YY = Y as non empty set ; i -tuples_on YY = Funcs ((Seg i),YY) by FINSEQ_2:93; hence i -tuples_on Y = Funcs ((Seg i),Y) ; ::_thesis: verum end; end; end; Lm11: for A, B being set for m being Nat holds (m -tuples_on A) /\ (B *) c= m -tuples_on B proof let A, B be set ; ::_thesis: for m being Nat holds (m -tuples_on A) /\ (B *) c= m -tuples_on B let m be Nat; ::_thesis: (m -tuples_on A) /\ (B *) c= m -tuples_on B reconsider mm = m as Element of NAT by ORDINAL1:def_12; set L = (m -tuples_on A) /\ (B *); set R = m -tuples_on B; now__::_thesis:_for_x_being_set_st_x_in_(m_-tuples_on_A)_/\_(B_*)_holds_ x_in_m_-tuples_on_B let x be set ; ::_thesis: ( x in (m -tuples_on A) /\ (B *) implies x in m -tuples_on B ) assume x in (m -tuples_on A) /\ (B *) ; ::_thesis: x in m -tuples_on B then Z1: ( x in m -tuples_on A & x in B * ) by XBOOLE_0:def_4; then B1: ( x is m -element FinSequence & x is FinSequence of B ) by FINSEQ_1:def_11, FINSEQ_2:141; reconsider xx = x as FinSequence of B by Z1, FINSEQ_1:def_11; len xx = m by B1, CARD_1:def_7; then ( xx = xx & dom xx = Seg m & rng xx c= B ) by FINSEQ_1:def_3; then xx in Funcs ((Seg m),B) by FUNCT_2:def_2; hence x in m -tuples_on B by Lm21; ::_thesis: verum end; hence (m -tuples_on A) /\ (B *) c= m -tuples_on B by TARSKI:def_3; ::_thesis: verum end; theorem Lm22: :: FOMODEL0:1 for A, B being set for m being Nat holds (m -tuples_on A) /\ (B *) = (m -tuples_on A) /\ (m -tuples_on B) proof let A, B be set ; ::_thesis: for m being Nat holds (m -tuples_on A) /\ (B *) = (m -tuples_on A) /\ (m -tuples_on B) let m be Nat; ::_thesis: (m -tuples_on A) /\ (B *) = (m -tuples_on A) /\ (m -tuples_on B) reconsider mm = m as Element of NAT by ORDINAL1:def_12; set L = (m -tuples_on A) /\ (B *); set R = (m -tuples_on A) /\ (m -tuples_on B); (m -tuples_on A) /\ ((m -tuples_on A) /\ (B *)) c= (m -tuples_on A) /\ (m -tuples_on B) by Lm11, XBOOLE_1:26; then A2: ((m -tuples_on A) /\ (m -tuples_on A)) /\ (B *) c= (m -tuples_on A) /\ (m -tuples_on B) by XBOOLE_1:16; now__::_thesis:_for_x_being_set_st_x_in_m_-tuples_on_B_holds_ x_in_B_* let x be set ; ::_thesis: ( x in m -tuples_on B implies x in B * ) assume C1: x in m -tuples_on B ; ::_thesis: x in B * then reconsider xx = x as m -element FinSequence by FINSEQ_2:141; xx in mm -tuples_on B by C1; then ( len xx = mm & rng xx c= B ) by FINSEQ_2:132; then x is FinSequence of B by FINSEQ_1:def_4; hence x in B * by FINSEQ_1:def_11; ::_thesis: verum end; then m -tuples_on B c= B * by TARSKI:def_3; then (m -tuples_on A) /\ (m -tuples_on B) c= (m -tuples_on A) /\ (B *) by XBOOLE_1:26; hence (m -tuples_on A) /\ (B *) = (m -tuples_on A) /\ (m -tuples_on B) by A2, XBOOLE_0:def_10; ::_thesis: verum end; Lm20: for A, B, C being set holds (Funcs (A,B)) /\ (Funcs (A,C)) = Funcs (A,(B /\ C)) proof let A, B, C be set ; ::_thesis: (Funcs (A,B)) /\ (Funcs (A,C)) = Funcs (A,(B /\ C)) set L = (Funcs (A,B)) /\ (Funcs (A,C)); set R = Funcs (A,(B /\ C)); now__::_thesis:_for_f_being_set_st_f_in_(Funcs_(A,B))_/\_(Funcs_(A,C))_holds_ f_in_Funcs_(A,(B_/\_C)) let f be set ; ::_thesis: ( f in (Funcs (A,B)) /\ (Funcs (A,C)) implies f in Funcs (A,(B /\ C)) ) assume f in (Funcs (A,B)) /\ (Funcs (A,C)) ; ::_thesis: f in Funcs (A,(B /\ C)) then C0: ( f in Funcs (A,B) & f in Funcs (A,C) ) by XBOOLE_0:def_4; consider f1 being Function such that C1: ( f1 = f & dom f1 = A & rng f1 c= B ) by C0, FUNCT_2:def_2; consider f2 being Function such that C2: ( f2 = f & dom f2 = A & rng f2 c= C ) by C0, FUNCT_2:def_2; ( f1 = f & dom f1 = A & rng f1 c= B /\ C ) by C1, C2, XBOOLE_1:19; hence f in Funcs (A,(B /\ C)) by FUNCT_2:def_2; ::_thesis: verum end; then A1: (Funcs (A,B)) /\ (Funcs (A,C)) c= Funcs (A,(B /\ C)) by TARSKI:def_3; ( Funcs (A,(B /\ C)) c= Funcs (A,B) & Funcs (A,(B /\ C)) c= Funcs (A,C) ) by FUNCT_5:56, XBOOLE_1:17; then Funcs (A,(B /\ C)) c= (Funcs (A,B)) /\ (Funcs (A,C)) by XBOOLE_1:19; hence (Funcs (A,B)) /\ (Funcs (A,C)) = Funcs (A,(B /\ C)) by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Lm23: :: FOMODEL0:2 for A, B being set for m being Nat holds (m -tuples_on A) /\ (B *) = m -tuples_on (A /\ B) proof let A, B be set ; ::_thesis: for m being Nat holds (m -tuples_on A) /\ (B *) = m -tuples_on (A /\ B) let m be Nat; ::_thesis: (m -tuples_on A) /\ (B *) = m -tuples_on (A /\ B) m -tuples_on (A /\ B) = Funcs ((Seg m),(A /\ B)) by Lm21 .= (Funcs ((Seg m),A)) /\ (Funcs ((Seg m),B)) by Lm20 .= (m -tuples_on A) /\ (Funcs ((Seg m),B)) by Lm21 .= (m -tuples_on A) /\ (m -tuples_on B) by Lm21 .= (m -tuples_on A) /\ (B *) by Lm22 ; hence (m -tuples_on A) /\ (B *) = m -tuples_on (A /\ B) ; ::_thesis: verum end; theorem Lm24: :: FOMODEL0:3 for A, B being set for m being Nat holds m -tuples_on (A /\ B) = (m -tuples_on A) /\ (m -tuples_on B) proof let A, B be set ; ::_thesis: for m being Nat holds m -tuples_on (A /\ B) = (m -tuples_on A) /\ (m -tuples_on B) let m be Nat; ::_thesis: m -tuples_on (A /\ B) = (m -tuples_on A) /\ (m -tuples_on B) m -tuples_on (A /\ B) = (m -tuples_on A) /\ (B *) by Lm23 .= (m -tuples_on A) /\ (m -tuples_on B) by Lm22 ; hence m -tuples_on (A /\ B) = (m -tuples_on A) /\ (m -tuples_on B) ; ::_thesis: verum end; ThConcatenation: for D being non empty set for x, y being FinSequence of D holds (D -concatenation) . (x,y) = x ^ y proof let D be non empty set ; ::_thesis: for x, y being FinSequence of D holds (D -concatenation) . (x,y) = x ^ y let x, y be FinSequence of D; ::_thesis: (D -concatenation) . (x,y) = x ^ y reconsider x2 = x, y2 = y as Element of D * by FINSEQ_1:def_11; reconsider x1 = x2, y1 = y2 as Element of (D *+^) by MONOID_0:def_34; B1: D -concatenation = the multF of (D *+^) by MONOID_0:def_36; x1 ^ y1 = x1 * y1 by MONOID_0:def_34 .= (D -concatenation) . (x1,y1) by B1, ALGSTR_0:def_18 ; hence (D -concatenation) . (x,y) = x ^ y ; ::_thesis: verum end; theorem Th4: :: FOMODEL0:4 for U being non empty set for x, y being FinSequence st x is U -valued & y is U -valued holds (U -concatenation) . (x,y) = x ^ y proof let U be non empty set ; ::_thesis: for x, y being FinSequence st x is U -valued & y is U -valued holds (U -concatenation) . (x,y) = x ^ y let x, y be FinSequence; ::_thesis: ( x is U -valued & y is U -valued implies (U -concatenation) . (x,y) = x ^ y ) set f = U -concatenation ; assume ( x is U -valued & y is U -valued ) ; ::_thesis: (U -concatenation) . (x,y) = x ^ y then reconsider xx = x, yy = y as FinSequence of U by Lm45; (U -concatenation) . (xx,yy) = xx ^ yy by ThConcatenation; hence (U -concatenation) . (x,y) = x ^ y ; ::_thesis: verum end; theorem Lm2: :: FOMODEL0:5 for D being non empty set for x being set holds ( x is non empty FinSequence of D iff x in (D *) \ {{}} ) proof let D be non empty set ; ::_thesis: for x being set holds ( x is non empty FinSequence of D iff x in (D *) \ {{}} ) let x be set ; ::_thesis: ( x is non empty FinSequence of D iff x in (D *) \ {{}} ) thus ( x is non empty FinSequence of D implies x in (D *) \ {{}} ) ::_thesis: ( x in (D *) \ {{}} implies x is non empty FinSequence of D ) proof assume x is non empty FinSequence of D ; ::_thesis: x in (D *) \ {{}} then ( not x in {{}} & x in D * ) by FINSEQ_1:def_11, TARSKI:def_1; hence x in (D *) \ {{}} by XBOOLE_0:def_5; ::_thesis: verum end; assume x in (D *) \ {{}} ; ::_thesis: x is non empty FinSequence of D then ( x in D * & not x in {{}} ) by XBOOLE_0:def_5; hence x is non empty FinSequence of D by FINSEQ_1:def_11, TARSKI:def_1; ::_thesis: verum end; Lm13: for D being non empty set for B, A being set for f being BinOp of D st B is f -unambiguous & A c= B holds A is f -unambiguous proof let D be non empty set ; ::_thesis: for B, A being set for f being BinOp of D st B is f -unambiguous & A c= B holds A is f -unambiguous let B, A be set ; ::_thesis: for f being BinOp of D st B is f -unambiguous & A c= B holds A is f -unambiguous let f be BinOp of D; ::_thesis: ( B is f -unambiguous & A c= B implies A is f -unambiguous ) assume ( B is f -unambiguous & A c= B ) ; ::_thesis: A is f -unambiguous then C1: ( f is [:B,D:] -one-to-one & A c= B ) by DefUnambiguous1; f is [:A,D:] -one-to-one by C1, Lm12, ZFMISC_1:96; hence A is f -unambiguous by DefUnambiguous1; ::_thesis: verum end; Lm14: for D being non empty set for f being BinOp of D holds {} is f -unambiguous proof let D be non empty set ; ::_thesis: for f being BinOp of D holds {} is f -unambiguous let f be BinOp of D; ::_thesis: {} is f -unambiguous reconsider A = [:{},D:] as empty set ; f | A is one-to-one ; then f is A -one-to-one by DefInj1; hence {} is f -unambiguous by DefUnambiguous1; ::_thesis: verum end; Lm27: for f, g being FinSequence holds dom <:f,g:> = Seg (min ((len f),(len g))) proof let f, g be FinSequence; ::_thesis: dom <:f,g:> = Seg (min ((len f),(len g))) set m = len f; set n = len g; set l = min ((len f),(len g)); thus dom <:f,g:> = (dom f) /\ (dom g) by FUNCT_3:def_7 .= (Seg (len f)) /\ (dom g) by FINSEQ_1:def_3 .= (Seg (len f)) /\ (Seg (len g)) by FINSEQ_1:def_3 .= Seg (min ((len f),(len g))) by FINSEQ_2:2 ; ::_thesis: verum end; registration let D be non empty set ; clusterD -pr1 -> associative for BinOp of D; coherence for b1 being BinOp of D st b1 = D -pr1 holds b1 is associative proof now__::_thesis:_for_a,_b,_c_being_Element_of_D_holds_(D_-pr1)_._(a,((D_-pr1)_._(b,c)))_=_(D_-pr1)_._(((D_-pr1)_._(a,b)),c) let a, b, c be Element of D; ::_thesis: (D -pr1) . (a,((D -pr1) . (b,c))) = (D -pr1) . (((D -pr1) . (a,b)),c) ( (D -pr1) . (a,((D -pr1) . (b,c))) = a & (D -pr1) . (((D -pr1) . (a,b)),c) = (D -pr1) . (a,c) ) by FUNCT_3:def_4; hence (D -pr1) . (a,((D -pr1) . (b,c))) = (D -pr1) . (((D -pr1) . (a,b)),c) by FUNCT_3:def_4; ::_thesis: verum end; hence for b1 being BinOp of D st b1 = D -pr1 holds b1 is associative by BINOP_1:def_3; ::_thesis: verum end; end; registration let D be set ; cluster Relation-like [:D,D:] -defined D -valued Function-like quasi_total associative for Element of bool [:[:D,D:],D:]; existence ex b1 being BinOp of D st b1 is associative proof percases ( not D is empty or D is empty ) ; suppose not D is empty ; ::_thesis: ex b1 being BinOp of D st b1 is associative then reconsider DD = D as non empty set ; reconsider ff = DD -pr1 as BinOp of D ; take ff ; ::_thesis: ff is associative thus ff is associative ; ::_thesis: verum end; suppose D is empty ; ::_thesis: ex b1 being BinOp of D st b1 is associative then reconsider DD = D as empty set ; set f = the BinOp of {}; ( the BinOp of {} is associative & the BinOp of {} is BinOp of DD ) ; hence ex b1 being BinOp of D st b1 is associative ; ::_thesis: verum end; end; end; end; definition let X be set ; let Y be Subset of X; :: original: * redefine funcY * -> non empty Subset of (X *); coherence Y * is non empty Subset of (X *) by FINSEQ_1:62; end; registration let D be non empty set ; clusterD -concatenation -> associative for BinOp of (D *); coherence for b1 being BinOp of (D *) st b1 = D -concatenation holds b1 is associative by MONOID_0:67; end; registration let D be non empty set ; cluster(D *) \ {{}} -> non empty ; coherence not (D *) \ {{}} is empty proof set x = the Element of D; ( <* the Element of D*> in D * & not <* the Element of D*> in {{}} ) by FINSEQ_1:def_11, TARSKI:def_1; hence not (D *) \ {{}} is empty by XBOOLE_0:def_5; ::_thesis: verum end; end; registration let D be non empty set ; let m be Nat; cluster Relation-like NAT -defined D -valued Function-like finite m -element FinSequence-like FinSubsequence-like countable finite-support for Element of D * ; existence ex b1 being Element of D * st b1 is m -element proof set p = the m -element FinSequence of D; reconsider pp = the m -element FinSequence of D as Element of D * by FINSEQ_1:def_11; take pp ; ::_thesis: pp is m -element thus pp is m -element ; ::_thesis: verum end; end; definition let X be set ; let f be Function; redefine attr f is X -one-to-one means :DefInj2: :: FOMODEL0:def 5 for x, y being set st x in X /\ (dom f) & y in X /\ (dom f) & f . x = f . y holds x = y; compatibility ( f is X -one-to-one iff for x, y being set st x in X /\ (dom f) & y in X /\ (dom f) & f . x = f . y holds x = y ) by LmOneOne; end; :: deftheorem DefInj2 defines -one-to-one FOMODEL0:def_5_:_ for X being set for f being Function holds ( f is X -one-to-one iff for x, y being set st x in X /\ (dom f) & y in X /\ (dom f) & f . x = f . y holds x = y ); registration let D be non empty set ; let f be BinOp of D; clusterf -unambiguous for set ; existence ex b1 being set st b1 is f -unambiguous proof take {} ; ::_thesis: {} is f -unambiguous thus {} is f -unambiguous by Lm14; ::_thesis: verum end; end; registration let f be Function; let x be set ; clusterf | {x} -> one-to-one ; coherence f | {x} is one-to-one proof set g = f | {x}; percases ( x in dom f or not x in dom f ) ; suppose x in dom f ; ::_thesis: f | {x} is one-to-one then f | {x} = x .--> (f . x) by FUNCT_7:6; hence f | {x} is one-to-one ; ::_thesis: verum end; suppose not x in dom f ; ::_thesis: f | {x} is one-to-one then reconsider gg = f | {x} as empty Function by RELAT_1:152, ZFMISC_1:50; gg is one-to-one ; hence f | {x} is one-to-one ; ::_thesis: verum end; end; end; end; registration let e be empty set ; identifye * with {e}; compatibility e * = {e} by FUNCT_7:17; identify{e} with e * ; compatibility {e} = e * ; end; registration cluster empty -> empty-membered for set ; coherence for b1 being set st b1 is empty holds b1 is empty-membered ; let e be empty set ; cluster{e} -> empty-membered ; coherence {e} is empty-membered proof for x being non empty set holds not x in {e} by TARSKI:def_1; hence {e} is empty-membered by SETFAM_1:def_10; ::_thesis: verum end; end; registration let U be non empty set ; let m1 be non zero Nat; clusterm1 -tuples_on U -> with_non-empty_elements ; coherence m1 -tuples_on U is with_non-empty_elements proof not len {} = m1 ; then {} is not Element of m1 -tuples_on U by CARD_1:def_7; hence m1 -tuples_on U is with_non-empty_elements by SETFAM_1:def_8; ::_thesis: verum end; end; registration let X be empty-membered set ; cluster -> empty-membered for Element of bool X; coherence for b1 being Subset of X holds b1 is empty-membered proof let Y be Subset of X; ::_thesis: Y is empty-membered for x being non empty set holds not x in Y by SETFAM_1:def_10; hence Y is empty-membered by SETFAM_1:def_10; ::_thesis: verum end; end; registration let A be set ; let m0 be zero number ; clusterm0 -tuples_on A -> empty-membered for set ; coherence for b1 being set st b1 = m0 -tuples_on A holds b1 is empty-membered by COMPUT_1:5; end; registration let e be empty set ; let m1 be non zero Nat; clusterm1 -tuples_on e -> empty ; coherence m1 -tuples_on e is empty by FINSEQ_3:119; end; registration let D be non empty set ; let f be BinOp of D; let e be empty set ; clustere /\ f -> f -unambiguous ; coherence e /\ f is f -unambiguous by Lm14; end; registration let U be non empty set ; let e be empty set ; clustere /\ U -> U -prefix ; coherence e /\ U is U -prefix proof set f = U -concatenation ; e /\ (U -concatenation) is U -concatenation -unambiguous ; hence e /\ U is U -prefix by DefPrefix; ::_thesis: verum end; end; registration let U be non empty set ; clusterU -prefix for set ; existence ex b1 being set st b1 is U -prefix proof take {} /\ U ; ::_thesis: {} /\ U is U -prefix thus {} /\ U is U -prefix ; ::_thesis: verum end; end; definition let D be non empty set ; let f be BinOp of D; let x be FinSequence of D; func MultPlace (f,x) -> Function means :DefMultPlace: :: FOMODEL0:def 6 ( dom it = NAT & it . 0 = x . 1 & ( for n being Nat holds it . (n + 1) = f . ((it . n),(x . (n + 2))) ) ); existence ex b1 being Function st ( dom b1 = NAT & b1 . 0 = x . 1 & ( for n being Nat holds b1 . (n + 1) = f . ((b1 . n),(x . (n + 2))) ) ) proof deffunc H1( Nat, set ) -> set = f . (\$2,(x . (\$1 + 2))); consider f1 being Function such that B1: ( dom f1 = NAT & f1 . 0 = x . 1 & ( for n being Nat holds f1 . (n + 1) = H1(n,f1 . n) ) ) from NAT_1:sch_11(); take f1 ; ::_thesis: ( dom f1 = NAT & f1 . 0 = x . 1 & ( for n being Nat holds f1 . (n + 1) = f . ((f1 . n),(x . (n + 2))) ) ) thus ( dom f1 = NAT & f1 . 0 = x . 1 & ( for n being Nat holds f1 . (n + 1) = f . ((f1 . n),(x . (n + 2))) ) ) by B1; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = NAT & b1 . 0 = x . 1 & ( for n being Nat holds b1 . (n + 1) = f . ((b1 . n),(x . (n + 2))) ) & dom b2 = NAT & b2 . 0 = x . 1 & ( for n being Nat holds b2 . (n + 1) = f . ((b2 . n),(x . (n + 2))) ) holds b1 = b2 proof let IT1, IT2 be Function; ::_thesis: ( dom IT1 = NAT & IT1 . 0 = x . 1 & ( for n being Nat holds IT1 . (n + 1) = f . ((IT1 . n),(x . (n + 2))) ) & dom IT2 = NAT & IT2 . 0 = x . 1 & ( for n being Nat holds IT2 . (n + 1) = f . ((IT2 . n),(x . (n + 2))) ) implies IT1 = IT2 ) assume C1: ( dom IT1 = NAT & IT1 . 0 = x . 1 & ( for n being Nat holds IT1 . (n + 1) = f . ((IT1 . n),(x . (n + 2))) ) ) ; ::_thesis: ( not dom IT2 = NAT or not IT2 . 0 = x . 1 or ex n being Nat st not IT2 . (n + 1) = f . ((IT2 . n),(x . (n + 2))) or IT1 = IT2 ) assume C2: ( dom IT2 = NAT & IT2 . 0 = x . 1 & ( for n being Nat holds IT2 . (n + 1) = f . ((IT2 . n),(x . (n + 2))) ) ) ; ::_thesis: IT1 = IT2 deffunc H1( Nat, set ) -> set = f . (\$2,(x . (\$1 + 2))); B1: dom IT1 = NAT by C1; B2: IT1 . 0 = x . 1 by C1; B3: for n being Nat holds IT1 . (n + 1) = H1(n,IT1 . n) by C1; B4: dom IT2 = NAT by C2; B5: IT2 . 0 = x . 1 by C2; B6: for n being Nat holds IT2 . (n + 1) = H1(n,IT2 . n) by C2; thus IT1 = IT2 from NAT_1:sch_15(B1, B2, B3, B4, B5, B6); ::_thesis: verum end; end; :: deftheorem DefMultPlace defines MultPlace FOMODEL0:def_6_:_ for D being non empty set for f being BinOp of D for x being FinSequence of D for b4 being Function holds ( b4 = MultPlace (f,x) iff ( dom b4 = NAT & b4 . 0 = x . 1 & ( for n being Nat holds b4 . (n + 1) = f . ((b4 . n),(x . (n + 2))) ) ) ); Lm1: for D being non empty set for f being BinOp of D for x being FinSequence of D for m being Nat holds ( ( m + 1 <= len x implies (MultPlace (f,x)) . m in D ) & ( for n being Nat st n >= m + 1 holds (MultPlace (f,(x | n))) . m = (MultPlace (f,x)) . m ) ) proof let D be non empty set ; ::_thesis: for f being BinOp of D for x being FinSequence of D for m being Nat holds ( ( m + 1 <= len x implies (MultPlace (f,x)) . m in D ) & ( for n being Nat st n >= m + 1 holds (MultPlace (f,(x | n))) . m = (MultPlace (f,x)) . m ) ) let f be BinOp of D; ::_thesis: for x being FinSequence of D for m being Nat holds ( ( m + 1 <= len x implies (MultPlace (f,x)) . m in D ) & ( for n being Nat st n >= m + 1 holds (MultPlace (f,(x | n))) . m = (MultPlace (f,x)) . m ) ) let x be FinSequence of D; ::_thesis: for m being Nat holds ( ( m + 1 <= len x implies (MultPlace (f,x)) . m in D ) & ( for n being Nat st n >= m + 1 holds (MultPlace (f,(x | n))) . m = (MultPlace (f,x)) . m ) ) defpred S1[ Nat] means ( \$1 + 1 <= len x implies (MultPlace (f,x)) . \$1 in D ); C0: S1[ 0 ] proof assume 0 + 1 <= len x ; ::_thesis: (MultPlace (f,x)) . 0 in D then 1 in Seg (len x) ; then 1 in dom x by FINSEQ_1:def_3; then ( x . 1 in rng x & rng x c= D ) by FUNCT_1:def_3; then ( x . 1 in D & (MultPlace (f,x)) . 0 = x . 1 ) by DefMultPlace; hence (MultPlace (f,x)) . 0 in D ; ::_thesis: verum end; C1: for m being Nat st S1[m] holds S1[m + 1] proof let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] ) assume E0: S1[m] ; ::_thesis: S1[m + 1] assume E1: (m + 1) + 1 <= len x ; ::_thesis: (MultPlace (f,x)) . (m + 1) in D then ( m + 2 <= len x & 1 <= m + 2 ) by NAT_1:12; then m + 2 in Seg (len x) by FINSEQ_1:1; then m + 2 in dom x by FINSEQ_1:def_3; then Z1: ( x . (m + 2) in rng x & rng x c= D ) by FUNCT_1:def_3; Z3: ( m + 1 <= m + 2 implies m + 1 <= len x ) by E1, XXREAL_0:2; [((MultPlace (f,x)) . m),(x . (m + 2))] in [:D,D:] by Z3, E0, Z1, XREAL_1:6, ZFMISC_1:def_2; then f . (((MultPlace (f,x)) . m),(x . (m + 2))) in D by FUNCT_2:5; hence (MultPlace (f,x)) . (m + 1) in D by DefMultPlace; ::_thesis: verum end; defpred S2[ Nat] means for n being Nat st n >= \$1 + 1 holds (MultPlace (f,(x | n))) . \$1 = (MultPlace (f,x)) . \$1; B0: S2[ 0 ] proof let n be Nat; ::_thesis: ( n >= 0 + 1 implies (MultPlace (f,(x | n))) . 0 = (MultPlace (f,x)) . 0 ) assume Z1: n >= 0 + 1 ; ::_thesis: (MultPlace (f,(x | n))) . 0 = (MultPlace (f,x)) . 0 (MultPlace (f,(x | n))) . 0 = (x | n) . 1 by DefMultPlace .= x . 1 by Z1, FINSEQ_3:112 .= (MultPlace (f,x)) . 0 by DefMultPlace ; hence (MultPlace (f,(x | n))) . 0 = (MultPlace (f,x)) . 0 ; ::_thesis: verum end; B1: for m being Nat st S2[m] holds S2[m + 1] proof let m be Nat; ::_thesis: ( S2[m] implies S2[m + 1] ) assume C1: S2[m] ; ::_thesis: S2[m + 1] let n be Nat; ::_thesis: ( n >= (m + 1) + 1 implies (MultPlace (f,(x | n))) . (m + 1) = (MultPlace (f,x)) . (m + 1) ) assume C2: n >= (m + 1) + 1 ; ::_thesis: (MultPlace (f,(x | n))) . (m + 1) = (MultPlace (f,x)) . (m + 1) then Z2: ( m + 2 >= m + 1 & n >= m + 2 ) by XREAL_1:6; (MultPlace (f,(x | n))) . (m + 1) = f . (((MultPlace (f,(x | n))) . m),((x | n) . (m + 2))) by DefMultPlace .= f . (((MultPlace (f,x)) . m),((x | n) . (m + 2))) by C1, Z2, XXREAL_0:2 .= f . (((MultPlace (f,x)) . m),(x . (m + 2))) by C2, FINSEQ_3:112 .= (MultPlace (f,x)) . (m + 1) by DefMultPlace ; hence (MultPlace (f,(x | n))) . (m + 1) = (MultPlace (f,x)) . (m + 1) ; ::_thesis: verum end; defpred S3[ Nat] means ( S2[\$1] & S1[\$1] ); D0: S3[ 0 ] by B0, C0; D1: for m being Nat st S3[m] holds S3[m + 1] by B1, C1; for m being Nat holds S3[m] from NAT_1:sch_2(D0, D1); hence for m being Nat holds ( ( m + 1 <= len x implies (MultPlace (f,x)) . m in D ) & ( for n being Nat st n >= m + 1 holds (MultPlace (f,(x | n))) . m = (MultPlace (f,x)) . m ) ) ; ::_thesis: verum end; definition let D be non empty set ; let f be BinOp of D; let x be Element of (D *) \ {{}}; func MultPlace (f,x) -> Function equals :: FOMODEL0:def 7 MultPlace (f,x); coherence MultPlace (f,x) is Function ; end; :: deftheorem defines MultPlace FOMODEL0:def_7_:_ for D being non empty set for f being BinOp of D for x being Element of (D *) \ {{}} holds MultPlace (f,x) = MultPlace (f,x); definition let D be non empty set ; let f be BinOp of D; func MultPlace f -> Function of ((D *) \ {{}}),D means :DefMultPlace2: :: FOMODEL0:def 8 for x being Element of (D *) \ {{}} holds it . x = (MultPlace (f,x)) . ((len x) - 1); existence ex b1 being Function of ((D *) \ {{}}),D st for x being Element of (D *) \ {{}} holds b1 . x = (MultPlace (f,x)) . ((len x) - 1) proof defpred S1[ Element of (D *) \ {{}}, Element of D] means \$2 = (MultPlace (f,\$1)) . ((len \$1) - 1); B1: for x being Element of (D *) \ {{}} ex y being Element of D st S1[x,y] proof let x be Element of (D *) \ {{}}; ::_thesis: ex y being Element of D st S1[x,y] reconsider x1 = x as Element of D * ; not x1 in {{}} by XBOOLE_0:def_5; then x1 <> {} by TARSKI:def_1; then len x1 >= 1 by FINSEQ_1:20; then (len x1) - 1 in NAT by INT_1:3, XREAL_1:48; then reconsider m = (len x1) - 1 as Nat ; C1: m + 1 <= len x1 ; reconsider y = (MultPlace (f,x1)) . m as Element of D by Lm1, C1; take y ; ::_thesis: S1[x,y] thus S1[x,y] ; ::_thesis: verum end; consider g being Function of ((D *) \ {{}}),D such that B2: for x being Element of (D *) \ {{}} holds S1[x,g . x] from FUNCT_2:sch_3(B1); take g ; ::_thesis: for x being Element of (D *) \ {{}} holds g . x = (MultPlace (f,x)) . ((len x) - 1) thus for x being Element of (D *) \ {{}} holds g . x = (MultPlace (f,x)) . ((len x) - 1) by B2; ::_thesis: verum end; uniqueness for b1, b2 being Function of ((D *) \ {{}}),D st ( for x being Element of (D *) \ {{}} holds b1 . x = (MultPlace (f,x)) . ((len x) - 1) ) & ( for x being Element of (D *) \ {{}} holds b2 . x = (MultPlace (f,x)) . ((len x) - 1) ) holds b1 = b2 proof let IT1, IT2 be Function of ((D *) \ {{}}),D; ::_thesis: ( ( for x being Element of (D *) \ {{}} holds IT1 . x = (MultPlace (f,x)) . ((len x) - 1) ) & ( for x being Element of (D *) \ {{}} holds IT2 . x = (MultPlace (f,x)) . ((len x) - 1) ) implies IT1 = IT2 ) Z1: ( dom IT1 = (D *) \ {{}} & dom IT2 = (D *) \ {{}} ) by FUNCT_2:def_1; assume A1: for x being Element of (D *) \ {{}} holds IT1 . x = (MultPlace (f,x)) . ((len x) - 1) ; ::_thesis: ( ex x being Element of (D *) \ {{}} st not IT2 . x = (MultPlace (f,x)) . ((len x) - 1) or IT1 = IT2 ) assume A2: for x being Element of (D *) \ {{}} holds IT2 . x = (MultPlace (f,x)) . ((len x) - 1) ; ::_thesis: IT1 = IT2 now__::_thesis:_for_x_being_set_st_x_in_dom_IT1_holds_ IT1_._x_=_IT2_._x let x be set ; ::_thesis: ( x in dom IT1 implies IT1 . x = IT2 . x ) assume x in dom IT1 ; ::_thesis: IT1 . x = IT2 . x then reconsider xx = x as Element of (D *) \ {{}} ; IT1 . x = (MultPlace (f,xx)) . ((len xx) - 1) by A1 .= IT2 . x by A2 ; hence IT1 . x = IT2 . x ; ::_thesis: verum end; hence IT1 = IT2 by Z1, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem DefMultPlace2 defines MultPlace FOMODEL0:def_8_:_ for D being non empty set for f being BinOp of D for b3 being Function of ((D *) \ {{}}),D holds ( b3 = MultPlace f iff for x being Element of (D *) \ {{}} holds b3 . x = (MultPlace (f,x)) . ((len x) - 1) ); LmMultPlace: for D being non empty set for f being BinOp of D for x being non empty FinSequence of D for y being Element of D holds ( (MultPlace f) . <*y*> = y & (MultPlace f) . (x ^ <*y*>) = f . (((MultPlace f) . x),y) ) proof let D be non empty set ; ::_thesis: for f being BinOp of D for x being non empty FinSequence of D for y being Element of D holds ( (MultPlace f) . <*y*> = y & (MultPlace f) . (x ^ <*y*>) = f . (((MultPlace f) . x),y) ) let f be BinOp of D; ::_thesis: for x being non empty FinSequence of D for y being Element of D holds ( (MultPlace f) . <*y*> = y & (MultPlace f) . (x ^ <*y*>) = f . (((MultPlace f) . x),y) ) set F = MultPlace f; let x be non empty FinSequence of D; ::_thesis: for y being Element of D holds ( (MultPlace f) . <*y*> = y & (MultPlace f) . (x ^ <*y*>) = f . (((MultPlace f) . x),y) ) let y be Element of D; ::_thesis: ( (MultPlace f) . <*y*> = y & (MultPlace f) . (x ^ <*y*>) = f . (((MultPlace f) . x),y) ) consider k being Nat such that B2: k + 1 = len x by NAT_1:6; reconsider x0 = x as Element of (D *) \ {{}} by Lm2; reconsider x1 = x ^ <*y*> as non empty FinSequence of D ; 1 in Seg 1 ; then 1 in dom <*y*> by FINSEQ_1:def_8; then Z2: x1 . ((len x) + 1) = <*y*> . 1 by FINSEQ_1:def_7 .= y by FINSEQ_1:40 ; Z1: x1 | (len x) = x | (len x) by FINSEQ_5:22 .= x by FINSEQ_3:49 ; B7: len <*y*> = 1 by FINSEQ_1:40; then B3: len x1 = (len x) + 1 by FINSEQ_1:22; reconsider y1 = <*y*> as non empty FinSequence of D ; reconsider y2 = y1 as Element of (D *) \ {{}} by Lm2; (len y2) - 1 = 0 by B7; then (MultPlace f) . y2 = (MultPlace (f,y2)) . 0 by DefMultPlace2 .= y2 . 1 by DefMultPlace .= y by FINSEQ_1:def_8 ; hence (MultPlace f) . <*y*> = y ; ::_thesis: (MultPlace f) . (x ^ <*y*>) = f . (((MultPlace f) . x),y) reconsider x2 = x1 as Element of (D *) \ {{}} by Lm2; (MultPlace f) . x2 = (MultPlace (f,x2)) . ((len x2) - 1) by DefMultPlace2 .= f . (((MultPlace (f,x2)) . k),(x2 . (k + 2))) by DefMultPlace, B2, B3 .= f . (((MultPlace (f,x0)) . ((len x) - 1)),(x2 . ((len x) + 1))) by Z1, B2, Lm1 .= f . (((MultPlace f) . x0),y) by Z2, DefMultPlace2 ; hence (MultPlace f) . (x ^ <*y*>) = f . (((MultPlace f) . x),y) ; ::_thesis: verum end; Lm3: for D being non empty set for f being BinOp of D for X being set holds ( f is [:X,D:] -one-to-one iff for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds ( x = y & d1 = d2 ) ) proof let D be non empty set ; ::_thesis: for f being BinOp of D for X being set holds ( f is [:X,D:] -one-to-one iff for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds ( x = y & d1 = d2 ) ) let f be BinOp of D; ::_thesis: for X being set holds ( f is [:X,D:] -one-to-one iff for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds ( x = y & d1 = d2 ) ) A1: dom f = [:D,D:] by FUNCT_2:def_1; let X be set ; ::_thesis: ( f is [:X,D:] -one-to-one iff for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds ( x = y & d1 = d2 ) ) thus ( f is [:X,D:] -one-to-one implies for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds ( x = y & d1 = d2 ) ) ::_thesis: ( ( for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds ( x = y & d1 = d2 ) ) implies f is [:X,D:] -one-to-one ) proof assume Z1: f is [:X,D:] -one-to-one ; ::_thesis: for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds ( x = y & d1 = d2 ) let x, y, d1, d2 be set ; ::_thesis: ( x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) implies ( x = y & d1 = d2 ) ) assume C1: ( x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) ) ; ::_thesis: ( x = y & d1 = d2 ) then ( [x,d1] in [:(X /\ D),(D /\ D):] & [y,d2] in [:(X /\ D),(D /\ D):] ) by ZFMISC_1:def_2; then C2: ( [x,d1] in [:X,D:] /\ [:D,D:] & [y,d2] in [:X,D:] /\ [:D,D:] ) by ZFMISC_1:100; [x,d1] = [y,d2] by DefInj2, A1, Z1, C2, C1; hence ( x = y & d1 = d2 ) by XTUPLE_0:1; ::_thesis: verum end; assume B2: for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds ( x = y & d1 = d2 ) ; ::_thesis: f is [:X,D:] -one-to-one now__::_thesis:_for_x,_y_being_set_st_x_in_[:X,D:]_/\_(dom_f)_&_y_in_[:X,D:]_/\_(dom_f)_&_f_._x_=_f_._y_holds_ x_=_y let x, y be set ; ::_thesis: ( x in [:X,D:] /\ (dom f) & y in [:X,D:] /\ (dom f) & f . x = f . y implies x = y ) assume Z1: ( x in [:X,D:] /\ (dom f) & y in [:X,D:] /\ (dom f) & f . x = f . y ) ; ::_thesis: x = y then C1: ( x in [:(X /\ D),(D /\ D):] & y in [:(X /\ D),(D /\ D):] & f . x = f . y ) by A1, ZFMISC_1:100; then consider x1, d1 being set such that C2: ( x1 in X /\ D & d1 in D & x = [x1,d1] ) by ZFMISC_1:def_2; consider x2, d2 being set such that C3: ( x2 in X /\ D & d2 in D & y = [x2,d2] ) by C1, ZFMISC_1:def_2; ( x1 in X /\ D & x2 in X /\ D & d1 in D & d2 in D & f . (x1,d1) = f . (x2,d2) ) by C2, C3, Z1; then ( x1 = x2 & d1 = d2 ) by B2; hence x = y by C2, C3; ::_thesis: verum end; hence f is [:X,D:] -one-to-one by DefInj2; ::_thesis: verum end; definition let D be non empty set ; let f be BinOp of D; let X be set ; redefine attr X is f -unambiguous means :DefUnambiguous2: :: FOMODEL0:def 9 for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds ( x = y & d1 = d2 ); compatibility ( X is f -unambiguous iff for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds ( x = y & d1 = d2 ) ) proof thus ( X is f -unambiguous implies for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds ( x = y & d1 = d2 ) ) ::_thesis: ( ( for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds ( x = y & d1 = d2 ) ) implies X is f -unambiguous ) proof assume X is f -unambiguous ; ::_thesis: for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds ( x = y & d1 = d2 ) then f is [:X,D:] -one-to-one by DefUnambiguous1; hence for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds ( x = y & d1 = d2 ) by Lm3; ::_thesis: verum end; assume for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds ( x = y & d1 = d2 ) ; ::_thesis: X is f -unambiguous then f is [:X,D:] -one-to-one by Lm3; hence X is f -unambiguous by DefUnambiguous1; ::_thesis: verum end; end; :: deftheorem DefUnambiguous2 defines -unambiguous FOMODEL0:def_9_:_ for D being non empty set for f being BinOp of D for X being set holds ( X is f -unambiguous iff for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds ( x = y & d1 = d2 ) ); Lm19: for D being non empty set for f being BinOp of D st f is associative holds for d being Element of D for m being Nat for x being Element of (m + 1) -tuples_on D holds (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x)) proof let D be non empty set ; ::_thesis: for f being BinOp of D st f is associative holds for d being Element of D for m being Nat for x being Element of (m + 1) -tuples_on D holds (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x)) let f be BinOp of D; ::_thesis: ( f is associative implies for d being Element of D for m being Nat for x being Element of (m + 1) -tuples_on D holds (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x)) ) set F = MultPlace f; assume A10: f is associative ; ::_thesis: for d being Element of D for m being Nat for x being Element of (m + 1) -tuples_on D holds (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x)) let d be Element of D; ::_thesis: for m being Nat for x being Element of (m + 1) -tuples_on D holds (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x)) defpred S1[ Nat] means for x being Element of (\$1 + 1) -tuples_on D holds (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x)); A0: S1[ 0 ] proof let x be Element of (0 + 1) -tuples_on D; ::_thesis: (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x)) consider xx being Element of D such that C1: x = <*xx*> by FINSEQ_2:97; (MultPlace f) . (<*d*> ^ x) = f . (((MultPlace f) . <*d*>),xx) by LmMultPlace, C1 .= f . (d,xx) by LmMultPlace .= f . (d,((MultPlace f) . x)) by LmMultPlace, C1 ; hence (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x)) ; ::_thesis: verum end; A1: for m being Nat st S1[m] holds S1[m + 1] proof let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] ) assume B0: S1[m] ; ::_thesis: S1[m + 1] let x be Element of ((m + 1) + 1) -tuples_on D; ::_thesis: (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x)) ( (m + 1) + 0 <= (m + 1) + 1 & len x = (m + 1) + 1 ) by CARD_1:def_7, XREAL_1:6; then len (x | (m + 1)) = m + 1 by FINSEQ_1:59; then reconsider xx = x | (m + 1) as Element of (m + 1) -tuples_on D by FINSEQ_2:92; reconsider xxx = xx as non empty FinSequence of D ; reconsider y = x /. (len x) as Element of D ; xxx in (D *) \ {{}} by Lm2; then reconsider XX = (MultPlace f) . xxx as Element of D by FUNCT_2:5; B2: (m + 1) + 1 = len x by CARD_1:def_7; then (MultPlace f) . (<*d*> ^ x) = (MultPlace f) . (<*d*> ^ ((x | (m + 1)) ^ <*y*>)) by FINSEQ_5:21 .= (MultPlace f) . ((<*d*> ^ xx) ^ <*y*>) by FINSEQ_1:32 .= f . (((MultPlace f) . (<*d*> ^ xx)),y) by LmMultPlace .= f . ((f . (d,((MultPlace f) . xx))),y) by B0 .= f . (d,(f . (XX,y))) by A10, BINOP_1:def_3 .= f . (d,((MultPlace f) . (xxx ^ <*y*>))) by LmMultPlace .= f . (d,((MultPlace f) . x)) by B2, FINSEQ_5:21 ; hence (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x)) ; ::_thesis: verum end; thus for m being Nat holds S1[m] from NAT_1:sch_2(A0, A1); ::_thesis: verum end; Lm5: for D being non empty set for X being non empty Subset of D for f being BinOp of D for m being Nat st f is associative & X is f -unambiguous holds (MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous proof let D be non empty set ; ::_thesis: for X being non empty Subset of D for f being BinOp of D for m being Nat st f is associative & X is f -unambiguous holds (MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous let X be non empty Subset of D; ::_thesis: for f being BinOp of D for m being Nat st f is associative & X is f -unambiguous holds (MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous let f be BinOp of D; ::_thesis: for m being Nat st f is associative & X is f -unambiguous holds (MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous let m be Nat; ::_thesis: ( f is associative & X is f -unambiguous implies (MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous ) set F = MultPlace f; assume A10: f is associative ; ::_thesis: ( not X is f -unambiguous or (MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous ) assume A11: X is f -unambiguous ; ::_thesis: (MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous defpred S1[ Nat] means (MultPlace f) .: ((\$1 + 1) -tuples_on X) is f -unambiguous ; A0: S1[ 0 ] proof set Z = (0 + 1) -tuples_on X; set Y = (MultPlace f) .: ((0 + 1) -tuples_on X); for x, y, d1, d2 being set st x in ((MultPlace f) .: ((0 + 1) -tuples_on X)) /\ D & y in ((MultPlace f) .: ((0 + 1) -tuples_on X)) /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds ( x = y & d1 = d2 ) proof let x, y, d1, d2 be set ; ::_thesis: ( x in ((MultPlace f) .: ((0 + 1) -tuples_on X)) /\ D & y in ((MultPlace f) .: ((0 + 1) -tuples_on X)) /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) implies ( x = y & d1 = d2 ) ) assume x in ((MultPlace f) .: ((0 + 1) -tuples_on X)) /\ D ; ::_thesis: ( not y in ((MultPlace f) .: ((0 + 1) -tuples_on X)) /\ D or not d1 in D or not d2 in D or not f . (x,d1) = f . (y,d2) or ( x = y & d1 = d2 ) ) then x in (MultPlace f) .: ((0 + 1) -tuples_on X) by XBOOLE_0:def_4; then consider uu being set such that C1: ( uu in dom (MultPlace f) & [uu,x] in MultPlace f & uu in (0 + 1) -tuples_on X ) by RELAT_1:110; assume y in ((MultPlace f) .: ((0 + 1) -tuples_on X)) /\ D ; ::_thesis: ( not d1 in D or not d2 in D or not f . (x,d1) = f . (y,d2) or ( x = y & d1 = d2 ) ) then y in (MultPlace f) .: ((0 + 1) -tuples_on X) by XBOOLE_0:def_4; then consider vv being set such that C2: ( vv in dom (MultPlace f) & [vv,y] in MultPlace f & vv in (0 + 1) -tuples_on X ) by RELAT_1:110; assume d1 in D ; ::_thesis: ( not d2 in D or not f . (x,d1) = f . (y,d2) or ( x = y & d1 = d2 ) ) then reconsider d11 = d1 as Element of D ; assume d2 in D ; ::_thesis: ( not f . (x,d1) = f . (y,d2) or ( x = y & d1 = d2 ) ) then reconsider d22 = d2 as Element of D ; reconsider u = uu as Element of 1 -tuples_on X by C1; reconsider v = vv as Element of 1 -tuples_on X by C2; assume f . (x,d1) = f . (y,d2) ; ::_thesis: ( x = y & d1 = d2 ) then C7: ( f . (x,d1) = f . (y,d2) & (MultPlace f) . u = x & (MultPlace f) . v = y ) by C1, C2, FUNCT_1:def_2; consider ee being Element of X such that C5: u = <*ee*> by FINSEQ_2:97; consider ff being Element of X such that C6: v = <*ff*> by FINSEQ_2:97; reconsider eee = ee, fff = ff as Element of D ; ( f . (((MultPlace f) . <*eee*>),d1) = f . (((MultPlace f) . <*fff*>),d2) & (MultPlace f) . <*eee*> = eee & (MultPlace f) . <*fff*> = fff ) by C7, C5, C6, LmMultPlace; then ( ee in X /\ D & ff in X /\ D & d11 in D & d22 in D & f . (ee,d11) = f . (ff,d22) ) by XBOOLE_0:def_4; hence ( x = y & d1 = d2 ) by C7, C5, C6, A11, DefUnambiguous2; ::_thesis: verum end; hence S1[ 0 ] by DefUnambiguous2; ::_thesis: verum end; A1: for m being Nat st S1[m] holds S1[m + 1] proof let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] ) assume B1: S1[m] ; ::_thesis: S1[m + 1] set Z = ((m + 1) + 1) -tuples_on X; set Y = (MultPlace f) .: (((m + 1) + 1) -tuples_on X); for x, y, d1, d2 being set st x in ((MultPlace f) .: (((m + 1) + 1) -tuples_on X)) /\ D & y in ((MultPlace f) .: (((m + 1) + 1) -tuples_on X)) /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds ( x = y & d1 = d2 ) proof let x, y, d1, d2 be set ; ::_thesis: ( x in ((MultPlace f) .: (((m + 1) + 1) -tuples_on X)) /\ D & y in ((MultPlace f) .: (((m + 1) + 1) -tuples_on X)) /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) implies ( x = y & d1 = d2 ) ) assume x in ((MultPlace f) .: (((m + 1) + 1) -tuples_on X)) /\ D ; ::_thesis: ( not y in ((MultPlace f) .: (((m + 1) + 1) -tuples_on X)) /\ D or not d1 in D or not d2 in D or not f . (x,d1) = f . (y,d2) or ( x = y & d1 = d2 ) ) then x in (MultPlace f) .: (((m + 1) + 1) -tuples_on X) by XBOOLE_0:def_4; then consider uu being set such that C1: ( uu in dom (MultPlace f) & [uu,x] in MultPlace f & uu in ((m + 1) + 1) -tuples_on X ) by RELAT_1:110; assume y in ((MultPlace f) .: (((m + 1) + 1) -tuples_on X)) /\ D ; ::_thesis: ( not d1 in D or not d2 in D or not f . (x,d1) = f . (y,d2) or ( x = y & d1 = d2 ) ) then y in (MultPlace f) .: (((m + 1) + 1) -tuples_on X) by XBOOLE_0:def_4; then consider vv being set such that C2: ( vv in dom (MultPlace f) & [vv,y] in MultPlace f & vv in ((m + 1) + 1) -tuples_on X ) by RELAT_1:110; assume d1 in D ; ::_thesis: ( not d2 in D or not f . (x,d1) = f . (y,d2) or ( x = y & d1 = d2 ) ) then reconsider d11 = d1 as Element of D ; assume d2 in D ; ::_thesis: ( not f . (x,d1) = f . (y,d2) or ( x = y & d1 = d2 ) ) then reconsider d22 = d2 as Element of D ; reconsider u = uu as Element of ((m + 1) + 1) -tuples_on X by C1; reconsider v = vv as Element of ((m + 1) + 1) -tuples_on X by C2; ( len u = (m + 1) + 1 & len v = (m + 1) + 1 & m + 1 <= (m + 1) + 1 ) by CARD_1:def_7, NAT_1:11; then C3: ( u = (u | (m + 1)) ^ <*(u /. (len u))*> & v = (v | (m + 1)) ^ <*(v /. (len v))*> & len (u | (m + 1)) = m + 1 & len (v | (m + 1)) = m + 1 ) by FINSEQ_1:59, FINSEQ_5:21; then reconsider u1 = u | (m + 1), v1 = v | (m + 1) as Tuple of m + 1,X by CARD_1:def_7; ( rng u1 c= D & rng v1 c= D ) by XBOOLE_1:1; then reconsider u2 = u1, v2 = v1 as non empty FinSequence of D by C3, FINSEQ_1:def_4; reconsider u3 = u2, v3 = v2 as Element of (D *) \ {{}} by Lm2; reconsider u4 = u2, v4 = v3 as Element of (m + 1) -tuples_on X by FINSEQ_2:131; reconsider ul = u /. (len u), vl = v /. (len v) as Element of D by TARSKI:def_3; C15: ( ul in X /\ D & vl in X /\ D ) by XBOOLE_0:def_4; C5: ( (MultPlace f) . (u2 ^ <*ul*>) = f . (((MultPlace f) . u2),ul) & (MultPlace f) . (v2 ^ <*vl*>) = f . (((MultPlace f) . v2),vl) ) by LmMultPlace; C6: ( f . ((f . (((MultPlace f) . u3),ul)),d11) = f . (((MultPlace f) . u3),(f . (ul,d11))) & f . ((f . (((MultPlace f) . v3),vl)),d22) = f . (((MultPlace f) . v3),(f . (vl,d22))) ) by A10, BINOP_1:def_3; assume f . (x,d1) = f . (y,d2) ; ::_thesis: ( x = y & d1 = d2 ) then Z2: ( f . (x,d1) = f . (y,d2) & (MultPlace f) . u = x & (MultPlace f) . v = y ) by C1, C2, FUNCT_1:def_2; dom (MultPlace f) = (D *) \ {{}} by FUNCT_2:def_1; then ( u3 in dom (MultPlace f) & v3 in dom (MultPlace f) & u4 in (m + 1) -tuples_on X & v4 in (m + 1) -tuples_on X ) ; then ( (MultPlace f) . u4 in (MultPlace f) .: ((m + 1) -tuples_on X) & (MultPlace f) . v4 in (MultPlace f) .: ((m + 1) -tuples_on X) & f . (ul,d11) in D & f . (vl,d22) in D ) by FUNCT_1:def_6; then ( (MultPlace f) . u4 in ((MultPlace f) .: ((m + 1) -tuples_on X)) /\ D & (MultPlace f) . v4 in ((MultPlace f) .: ((m + 1) -tuples_on X)) /\ D & f . (ul,d11) in D & f . (vl,d22) in D ) by XBOOLE_0:def_4; then C8: ( (MultPlace f) . u3 = (MultPlace f) . v3 & f . (ul,d11) = f . (vl,d22) ) by Z2, C3, C5, C6, B1, DefUnambiguous2; thus ( x = y & d1 = d2 ) by C8, A11, DefUnambiguous2, C15, Z2, C3, C5; ::_thesis: verum end; hence S1[m + 1] by DefUnambiguous2; ::_thesis: verum end; for m being Nat holds S1[m] from NAT_1:sch_2(A0, A1); hence (MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous ; ::_thesis: verum end; Lm15: for D being non empty set for Y being set for f being BinOp of D for m being Nat st f is associative & Y is f -unambiguous holds (MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous proof let D be non empty set ; ::_thesis: for Y being set for f being BinOp of D for m being Nat st f is associative & Y is f -unambiguous holds (MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous let Y be set ; ::_thesis: for f being BinOp of D for m being Nat st f is associative & Y is f -unambiguous holds (MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous let f be BinOp of D; ::_thesis: for m being Nat st f is associative & Y is f -unambiguous holds (MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous let m be Nat; ::_thesis: ( f is associative & Y is f -unambiguous implies (MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous ) set F = MultPlace f; B1: dom (MultPlace f) = (D *) \ {{}} by FUNCT_2:def_1; assume ( f is associative & Y is f -unambiguous ) ; ::_thesis: (MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous then B0: ( f is associative & Y /\ D is f -unambiguous ) by Lm13, XBOOLE_1:17; B2: (m + 1) -tuples_on (Y /\ D) misses 0 -tuples_on Y by Lm18; Z1: (MultPlace f) .: ((m + 1) -tuples_on Y) = (MultPlace f) .: (((D *) \ {{}}) /\ ((m + 1) -tuples_on Y)) by B1, RELAT_1:112 .= (MultPlace f) .: (((D *) /\ ((m + 1) -tuples_on Y)) \ {{}}) by XBOOLE_1:49 .= (MultPlace f) .: (((m + 1) -tuples_on (Y /\ D)) \ {{}}) by Lm23 .= (MultPlace f) .: (((m + 1) -tuples_on (Y /\ D)) \ (0 -tuples_on Y)) by COMPUT_1:5 .= (MultPlace f) .: ((m + 1) -tuples_on (Y /\ D)) by B2, XBOOLE_1:83 ; percases ( Y /\ D <> {} or Y /\ D = {} ) ; suppose Y /\ D <> {} ; ::_thesis: (MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous then reconsider YY = Y /\ D as non empty Subset of D by XBOOLE_1:17; (MultPlace f) .: ((m + 1) -tuples_on Y) = (MultPlace f) .: ((m + 1) -tuples_on YY) by Z1; hence (MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous by Lm5, B0; ::_thesis: verum end; suppose Y /\ D = {} ; ::_thesis: (MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous then (MultPlace f) .: ((m + 1) -tuples_on Y) = (MultPlace f) .: {} by Z1 .= {} ; hence (MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous by Lm14; ::_thesis: verum end; end; end; Lm17: for D being non empty set for X being non empty Subset of D for f being BinOp of D for m being Nat st f is associative & X is f -unambiguous holds MultPlace f is (m + 1) -tuples_on X -one-to-one proof let D be non empty set ; ::_thesis: for X being non empty Subset of D for f being BinOp of D for m being Nat st f is associative & X is f -unambiguous holds MultPlace f is (m + 1) -tuples_on X -one-to-one let X be non empty Subset of D; ::_thesis: for f being BinOp of D for m being Nat st f is associative & X is f -unambiguous holds MultPlace f is (m + 1) -tuples_on X -one-to-one let f be BinOp of D; ::_thesis: for m being Nat st f is associative & X is f -unambiguous holds MultPlace f is (m + 1) -tuples_on X -one-to-one let m be Nat; ::_thesis: ( f is associative & X is f -unambiguous implies MultPlace f is (m + 1) -tuples_on X -one-to-one ) set F = MultPlace f; A0: dom (MultPlace f) = (D *) \ {{}} by FUNCT_2:def_1; defpred S1[ Nat] means MultPlace f is (\$1 + 1) -tuples_on X -one-to-one ; assume Z2: ( f is associative & X is f -unambiguous ) ; ::_thesis: MultPlace f is (m + 1) -tuples_on X -one-to-one A10: S1[ 0 ] proof now__::_thesis:_for_x,_y_being_set_st_x_in_((0_+_1)_-tuples_on_X)_/\_(dom_(MultPlace_f))_&_y_in_((0_+_1)_-tuples_on_X)_/\_(dom_(MultPlace_f))_&_(MultPlace_f)_._x_=_(MultPlace_f)_._y_holds_ x_=_y let x, y be set ; ::_thesis: ( x in ((0 + 1) -tuples_on X) /\ (dom (MultPlace f)) & y in ((0 + 1) -tuples_on X) /\ (dom (MultPlace f)) & (MultPlace f) . x = (MultPlace f) . y implies x = y ) assume Z3: ( x in ((0 + 1) -tuples_on X) /\ (dom (MultPlace f)) & y in ((0 + 1) -tuples_on X) /\ (dom (MultPlace f)) & (MultPlace f) . x = (MultPlace f) . y ) ; ::_thesis: x = y then Z1: ( x is Element of 1 -tuples_on X & y is Element of 1 -tuples_on X & (MultPlace f) . x = (MultPlace f) . y ) by XBOOLE_0:def_4; consider u being Element of X such that C3: x = <*u*> by Z1, FINSEQ_2:97; consider v being Element of X such that C4: y = <*v*> by Z1, FINSEQ_2:97; reconsider uu = u, vv = v as Element of D ; uu = (MultPlace f) . y by Z3, C3, LmMultPlace .= vv by C4, LmMultPlace ; hence x = y by C3, C4; ::_thesis: verum end; hence MultPlace f is (0 + 1) -tuples_on X -one-to-one by DefInj2; ::_thesis: verum end; A11: for m being Nat st S1[m] holds S1[m + 1] proof let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] ) assume B1: S1[m] ; ::_thesis: S1[m + 1] set goal = ((m + 1) + 1) -tuples_on X; now__::_thesis:_for_x,_y_being_set_st_x_in_(((m_+_1)_+_1)_-tuples_on_X)_/\_(dom_(MultPlace_f))_&_y_in_(((m_+_1)_+_1)_-tuples_on_X)_/\_(dom_(MultPlace_f))_&_(MultPlace_f)_._x_=_(MultPlace_f)_._y_holds_ x_=_y let x, y be set ; ::_thesis: ( x in (((m + 1) + 1) -tuples_on X) /\ (dom (MultPlace f)) & y in (((m + 1) + 1) -tuples_on X) /\ (dom (MultPlace f)) & (MultPlace f) . x = (MultPlace f) . y implies x = y ) assume Z1: ( x in (((m + 1) + 1) -tuples_on X) /\ (dom (MultPlace f)) & y in (((m + 1) + 1) -tuples_on X) /\ (dom (MultPlace f)) & (MultPlace f) . x = (MultPlace f) . y ) ; ::_thesis: x = y reconsider xx = x, yy = y as Element of ((m + 1) + 1) -tuples_on X by Z1, XBOOLE_0:def_4; ( len xx = (m + 1) + 1 & len yy = (m + 1) + 1 & (m + 1) + 0 <= (m + 1) + 1 ) by CARD_1:def_7, NAT_1:11; then ( len (xx | (m + 1)) = m + 1 & len (yy | (m + 1)) = m + 1 ) by FINSEQ_1:59; then reconsider x1 = xx | (m + 1), y1 = yy | (m + 1) as Element of (m + 1) -tuples_on X by FINSEQ_2:92; reconsider x11 = x1, y11 = y1 as non empty FinSequence of X ; ( rng x11 c= D & rng y11 c= D ) by XBOOLE_1:1; then reconsider x111 = x11, y111 = y11 as non empty FinSequence of D by FINSEQ_1:def_4; reconsider xl = xx /. (len xx), yl = yy /. (len yy) as Element of D by TARSKI:def_3; C2: ( (MultPlace f) . (x111 ^ <*xl*>) = f . (((MultPlace f) . x111),xl) & (MultPlace f) . (y111 ^ <*yl*>) = f . (((MultPlace f) . y111),yl) ) by LmMultPlace; ( len xx = (m + 1) + 1 & len yy = (m + 1) + 1 ) by CARD_1:def_7; then C10: ( xx = x1 ^ <*xl*> & yy = y1 ^ <*yl*> ) by FINSEQ_5:21; C7: ( x111 in dom (MultPlace f) & x1 in (m + 1) -tuples_on X & y111 in dom (MultPlace f) & y1 in (m + 1) -tuples_on X ) by Lm2, A0; then ( (MultPlace f) . x1 in (MultPlace f) .: ((m + 1) -tuples_on X) & (MultPlace f) . x111 in D & (MultPlace f) . y1 in (MultPlace f) .: ((m + 1) -tuples_on X) & (MultPlace f) . y111 in D ) by FUNCT_1:def_6, PARTFUN1:4; then C4: ( (MultPlace f) . x1 in ((MultPlace f) .: ((m + 1) -tuples_on X)) /\ D & (MultPlace f) . y1 in ((MultPlace f) .: ((m + 1) -tuples_on X)) /\ D & xl in D & yl in D & f . (((MultPlace f) . x1),xl) = f . (((MultPlace f) . y1),yl) ) by C10, C2, Z1, XBOOLE_0:def_4; (MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous by Z2, Lm5; then C8: ( (MultPlace f) . x1 = (MultPlace f) . y1 & xl = yl ) by C4, DefUnambiguous2; ( x1 in ((m + 1) -tuples_on X) /\ (dom (MultPlace f)) & y1 in ((m + 1) -tuples_on X) /\ (dom (MultPlace f)) ) by C7, XBOOLE_0:def_4; hence x = y by C8, B1, DefInj2, C10; ::_thesis: verum end; hence MultPlace f is ((m + 1) + 1) -tuples_on X -one-to-one by DefInj2; ::_thesis: verum end; for m being Nat holds S1[m] from NAT_1:sch_2(A10, A11); hence MultPlace f is (m + 1) -tuples_on X -one-to-one ; ::_thesis: verum end; Lm26: for D being non empty set for Y being set for f being BinOp of D for m being Nat st f is associative & Y is f -unambiguous holds MultPlace f is (m + 1) -tuples_on Y -one-to-one proof let D be non empty set ; ::_thesis: for Y being set for f being BinOp of D for m being Nat st f is associative & Y is f -unambiguous holds MultPlace f is (m + 1) -tuples_on Y -one-to-one let Y be set ; ::_thesis: for f being BinOp of D for m being Nat st f is associative & Y is f -unambiguous holds MultPlace f is (m + 1) -tuples_on Y -one-to-one let f be BinOp of D; ::_thesis: for m being Nat st f is associative & Y is f -unambiguous holds MultPlace f is (m + 1) -tuples_on Y -one-to-one let m be Nat; ::_thesis: ( f is associative & Y is f -unambiguous implies MultPlace f is (m + 1) -tuples_on Y -one-to-one ) A0: (m + 1) -tuples_on Y misses 0 -tuples_on Y by Lm18; assume B0: ( f is associative & Y is f -unambiguous ) ; ::_thesis: MultPlace f is (m + 1) -tuples_on Y -one-to-one set F = MultPlace f; dom (MultPlace f) = (D *) \ {{}} by FUNCT_2:def_1; Z1: (MultPlace f) | ((m + 1) -tuples_on Y) = ((MultPlace f) | ((D *) \ {{}})) | ((m + 1) -tuples_on Y) .= (MultPlace f) | (((D *) \ {{}}) /\ ((m + 1) -tuples_on Y)) by RELAT_1:71 .= (MultPlace f) | (((D *) /\ ((m + 1) -tuples_on Y)) \ {{}}) by XBOOLE_1:49 .= (MultPlace f) | ((D *) /\ (((m + 1) -tuples_on Y) \ {{}})) by XBOOLE_1:49 .= (MultPlace f) | ((D *) /\ (((m + 1) -tuples_on Y) \ (0 -tuples_on Y))) by COMPUT_1:5 .= (MultPlace f) | ((D *) /\ ((m + 1) -tuples_on Y)) by A0, XBOOLE_1:83 .= (MultPlace f) | ((m + 1) -tuples_on (Y /\ D)) by Lm23 ; B2: Y /\ D is f -unambiguous by Lm13, B0, XBOOLE_1:17; percases ( D /\ Y <> {} or D /\ Y = {} ) ; suppose D /\ Y <> {} ; ::_thesis: MultPlace f is (m + 1) -tuples_on Y -one-to-one then reconsider X = D /\ Y as non empty Subset of D by XBOOLE_1:17; MultPlace f is (m + 1) -tuples_on X -one-to-one by Lm17, B2, B0; then (MultPlace f) | ((m + 1) -tuples_on Y) is one-to-one by DefInj1, Z1; hence MultPlace f is (m + 1) -tuples_on Y -one-to-one by DefInj1; ::_thesis: verum end; suppose D /\ Y = {} ; ::_thesis: MultPlace f is (m + 1) -tuples_on Y -one-to-one hence MultPlace f is (m + 1) -tuples_on Y -one-to-one by Z1, DefInj1; ::_thesis: verum end; end; end; definition let D be non empty set ; funcD -firstChar -> Function of ((D *) \ {{}}),D equals :: FOMODEL0:def 10 MultPlace (D -pr1); coherence MultPlace (D -pr1) is Function of ((D *) \ {{}}),D ; end; :: deftheorem defines -firstChar FOMODEL0:def_10_:_ for D being non empty set holds D -firstChar = MultPlace (D -pr1); Th2: for D being non empty set for w being non empty FinSequence of D holds (D -firstChar) . w = w . 1 proof let D be non empty set ; ::_thesis: for w being non empty FinSequence of D holds (D -firstChar) . w = w . 1 let w be non empty FinSequence of D; ::_thesis: (D -firstChar) . w = w . 1 consider d being Element of D, df1 being FinSequence of D such that B1: ( d = w . 1 & w = <*d*> ^ df1 ) by FINSEQ_3:102; set f = D -pr1 ; set F = MultPlace (D -pr1); percases ( len w <= 1 or len w > 1 ) ; suppose len w <= 1 ; ::_thesis: (D -firstChar) . w = w . 1 then ( len w <= 0 or len w = 0 + 1 ) by NAT_1:8; then w = <*d*> by B1, FINSEQ_1:40; hence (D -firstChar) . w = w . 1 by LmMultPlace, B1; ::_thesis: verum end; supposeC1: len w > 1 ; ::_thesis: (D -firstChar) . w = w . 1 len w = (len <*d*>) + (len df1) by B1, FINSEQ_1:22 .= 1 + (len df1) by FINSEQ_1:40 ; then len df1 <> 0 by C1; then consider k being Nat such that C2: len df1 = k + 1 by NAT_1:6; reconsider df11 = df1 as Element of (k + 1) -tuples_on D by C2, FINSEQ_2:133; reconsider df111 = df11 as Element of (D *) \ {{}} by Lm2; (MultPlace (D -pr1)) . w = (pr1 (D,D)) . (d,((MultPlace (D -pr1)) . df111)) by B1, Lm19 .= w . 1 by B1, FUNCT_3:def_4 ; hence (D -firstChar) . w = w . 1 ; ::_thesis: verum end; end; end; theorem :: FOMODEL0:6 for U being non empty set for p being FinSequence st p is U -valued & not p is empty holds (U -firstChar) . p = p . 1 proof let U be non empty set ; ::_thesis: for p being FinSequence st p is U -valued & not p is empty holds (U -firstChar) . p = p . 1 let p be FinSequence; ::_thesis: ( p is U -valued & not p is empty implies (U -firstChar) . p = p . 1 ) assume ( p is U -valued & not p is empty ) ; ::_thesis: (U -firstChar) . p = p . 1 then reconsider pp = p as non empty FinSequence of U by Lm45; (U -firstChar) . pp = pp . 1 by Th2; hence (U -firstChar) . p = p . 1 ; ::_thesis: verum end; definition let D be non empty set ; funcD -multiCat -> Function equals :: FOMODEL0:def 11 ({} .--> {}) +* (MultPlace (D -concatenation)); coherence ({} .--> {}) +* (MultPlace (D -concatenation)) is Function ; end; :: deftheorem defines -multiCat FOMODEL0:def_11_:_ for D being non empty set holds D -multiCat = ({} .--> {}) +* (MultPlace (D -concatenation)); definition let D be non empty set ; :: original: -multiCat redefine funcD -multiCat -> Function of ((D *) *),(D *); coherence D -multiCat is Function of ((D *) *),(D *) proof ( {} in (D *) * & {} in D * ) by FINSEQ_1:49; then Z1: ( {{}} c= (D *) * & {{}} c= D * ) by ZFMISC_1:31; then A0: ( {{}} \/ ((D *) *) = (D *) * & {{}} \/ (D *) = D * ) by XBOOLE_1:12; set f = {} .--> {}; set g = MultPlace (D -concatenation); A1: ( dom ({} .--> {}) = {{}} & rng ({} .--> {}) c= {{}} ) by FUNCOP_1:13; A2: ( dom (MultPlace (D -concatenation)) = ((D *) *) \ {{}} & rng (MultPlace (D -concatenation)) c= D * ) by FUNCT_2:def_1; (dom ({} .--> {})) \/ (dom (MultPlace (D -concatenation))) = {{}} \/ ((D *) *) by A1, A2, XBOOLE_1:39; then A4: (dom ({} .--> {})) \/ (dom (MultPlace (D -concatenation))) = (D *) * by Z1, XBOOLE_1:12; ( (rng ({} .--> {})) \/ (rng (MultPlace (D -concatenation))) c= D * & rng (({} .--> {}) +* (MultPlace (D -concatenation))) c= (rng ({} .--> {})) \/ (rng (MultPlace (D -concatenation))) ) by A0, A1, FUNCT_4:17, XBOOLE_1:13; then ( dom (D -multiCat) = (D *) * & rng (D -multiCat) c= D * ) by A4, FUNCT_4:def_1, XBOOLE_1:1; hence D -multiCat is Function of ((D *) *),(D *) by FUNCT_2:67, RELSET_1:4; ::_thesis: verum end; end; Lm6: for D being non empty set holds (D -multiCat) | (((D *) *) \ {{}}) = MultPlace (D -concatenation) proof let D be non empty set ; ::_thesis: (D -multiCat) | (((D *) *) \ {{}}) = MultPlace (D -concatenation) set f = D -concatenation ; set F = MultPlace (D -concatenation); dom (MultPlace (D -concatenation)) = ((D *) *) \ {{}} by FUNCT_2:def_1; hence (D -multiCat) | (((D *) *) \ {{}}) = MultPlace (D -concatenation) by FUNCT_4:23; ::_thesis: verum end; Lm16: for D being non empty set for Y being set holds (D -multiCat) | (Y \ {{}}) = (MultPlace (D -concatenation)) | Y proof let D be non empty set ; ::_thesis: for Y being set holds (D -multiCat) | (Y \ {{}}) = (MultPlace (D -concatenation)) | Y let Y be set ; ::_thesis: (D -multiCat) | (Y \ {{}}) = (MultPlace (D -concatenation)) | Y set F = D -multiCat ; B1: dom (D -multiCat) = (D *) * by FUNCT_2:def_1; (D -multiCat) | (Y \ {{}}) = ((D -multiCat) | ((D *) *)) | (Y \ {{}}) .= (D -multiCat) | (((D *) *) /\ (Y \ {{}})) by RELAT_1:71 .= (D -multiCat) | ((((D *) *) /\ Y) \ {{}}) by XBOOLE_1:49 .= (D -multiCat) | (Y /\ (((D *) *) \ {{}})) by XBOOLE_1:49 .= ((D -multiCat) | (((D *) *) \ {{}})) | Y by RELAT_1:71 .= (MultPlace (D -concatenation)) | Y by Lm6 ; hence (D -multiCat) | (Y \ {{}}) = (MultPlace (D -concatenation)) | Y ; ::_thesis: verum end; Lm9: for D being non empty set holds {} .--> {} tolerates MultPlace (D -concatenation) proof let D be non empty set ; ::_thesis: {} .--> {} tolerates MultPlace (D -concatenation) set f = {} .--> {}; set g = MultPlace (D -concatenation); ( dom ({} .--> {}) = {{}} & dom (MultPlace (D -concatenation)) = ((D *) *) \ {{}} ) by FUNCT_2:def_1; then dom (MultPlace (D -concatenation)) misses dom ({} .--> {}) by XBOOLE_1:79; then for x being set st x in (dom (MultPlace (D -concatenation))) /\ (dom ({} .--> {})) holds ({} .--> {}) . x = (MultPlace (D -concatenation)) . x by XBOOLE_0:def_7; hence {} .--> {} tolerates MultPlace (D -concatenation) by PARTFUN1:def_4; ::_thesis: verum end; registration let D be non empty set ; let e be empty set ; cluster(D -multiCat) . e -> empty for set ; coherence for b1 being set st b1 = (D -multiCat) . e holds b1 is empty proof set g = MultPlace (D -concatenation); set f = {} .--> {}; ( dom ({} .--> {}) = {{}} & dom (MultPlace (D -concatenation)) = ((D *) *) \ {{}} ) by FUNCT_2:def_1; then {} in dom ({} .--> {}) by TARSKI:def_1; then A1: ( {} in dom ({} .--> {}) & {} in (dom (MultPlace (D -concatenation))) \/ (dom ({} .--> {})) ) by XBOOLE_0:def_3; {} .--> {} tolerates MultPlace (D -concatenation) by Lm9; then D -multiCat = (MultPlace (D -concatenation)) +* ({} .--> {}) by FUNCT_4:34; then ( e = {} & (D -multiCat) . {} = ({} .--> {}) . {} ) by A1, FUNCT_4:def_1; hence for b1 being set st b1 = (D -multiCat) . e holds b1 is empty by FUNCOP_1:72; ::_thesis: verum end; end; Lm59: for D being non empty set for B, A being set st B is D -prefix & A c= B holds A is D -prefix proof let D be non empty set ; ::_thesis: for B, A being set st B is D -prefix & A c= B holds A is D -prefix let B, A be set ; ::_thesis: ( B is D -prefix & A c= B implies A is D -prefix ) set f = D -concatenation ; assume ( B is D -prefix & A c= B ) ; ::_thesis: A is D -prefix then ( B is D -concatenation -unambiguous & A c= B ) by DefPrefix; then A is D -concatenation -unambiguous by Lm13; hence A is D -prefix by DefPrefix; ::_thesis: verum end; registration let D be non empty set ; cluster -> D -prefix for Element of bool (1 -tuples_on D); coherence for b1 being Subset of (1 -tuples_on D) holds b1 is D -prefix proof set f = D -concatenation ; set D1 = 1 -tuples_on D; let X be Subset of (1 -tuples_on D); ::_thesis: X is D -prefix B1: 1 -tuples_on D c= D * by FINSEQ_2:134; now__::_thesis:_for_x1,_x2,_d1,_d2_being_set_st_x1_in_X_/\_(D_*)_&_x2_in_X_/\_(D_*)_&_d1_in_D_*_&_d2_in_D_*_&_(D_-concatenation)_._(x1,d1)_=_(D_-concatenation)_._(x2,d2)_holds_ (_x1_=_x2_&_d1_=_d2_) let x1, x2, d1, d2 be set ; ::_thesis: ( x1 in X /\ (D *) & x2 in X /\ (D *) & d1 in D * & d2 in D * & (D -concatenation) . (x1,d1) = (D -concatenation) . (x2,d2) implies ( x1 = x2 & d1 = d2 ) ) assume C1: ( x1 in X /\ (D *) & x2 in X /\ (D *) & d1 in D * & d2 in D * ) ; ::_thesis: ( (D -concatenation) . (x1,d1) = (D -concatenation) . (x2,d2) implies ( x1 = x2 & d1 = d2 ) ) then reconsider x11 = x1, x22 = x2 as Element of 1 -tuples_on D ; reconsider x111 = x11, x222 = x22 as 1 -element FinSequence ; reconsider x1111 = x11, x2222 = x22 as Element of D * by B1, TARSKI:def_3; reconsider xx1 = x1111, xx2 = x2222, dd1 = d1, dd2 = d2 as FinSequence of D by C1, FINSEQ_1:def_11; ( len xx1 = 1 & len xx2 = 1 ) by CARD_1:def_7; then C3: ( xx1 = <*(xx1 . 1)*> & xx2 = <*(xx2 . 1)*> ) by FINSEQ_1:40; C2: ( (D -concatenation) . (x1,d1) = xx1 ^ dd1 & (D -concatenation) . (x2,d2) = xx2 ^ dd2 ) by ThConcatenation; assume Z1: (D -concatenation) . (x1,d1) = (D -concatenation) . (x2,d2) ; ::_thesis: ( x1 = x2 & d1 = d2 ) Z2: xx1 . 1 = (xx1 ^ dd1) . 1 by C3, FINSEQ_1:41 .= xx2 . 1 by C3, Z1, C2, FINSEQ_1:41 ; thus ( x1 = x2 & d1 = d2 ) by Z2, C3, Z1, C2, FINSEQ_1:33; ::_thesis: verum end; then X is D -concatenation -unambiguous by DefUnambiguous2; hence X is D -prefix by DefPrefix; ::_thesis: verum end; end; theorem Lm25: :: FOMODEL0:7 for D being non empty set for A being set for m being Nat st A is D -prefix holds (D -multiCat) .: (m -tuples_on A) is D -prefix proof let D be non empty set ; ::_thesis: for A being set for m being Nat st A is D -prefix holds (D -multiCat) .: (m -tuples_on A) is D -prefix let A be set ; ::_thesis: for m being Nat st A is D -prefix holds (D -multiCat) .: (m -tuples_on A) is D -prefix let m be Nat; ::_thesis: ( A is D -prefix implies (D -multiCat) .: (m -tuples_on A) is D -prefix ) reconsider f = D -concatenation as BinOp of (D *) ; set F = D -multiCat ; set Y = (D -multiCat) .: (m -tuples_on A); {} in (D *) * by FINSEQ_1:49; then A1: {} in dom (D -multiCat) by FUNCT_2:def_1; percases ( m = 0 or m <> 0 ) ; suppose m = 0 ; ::_thesis: ( A is D -prefix implies (D -multiCat) .: (m -tuples_on A) is D -prefix ) then Z1: (D -multiCat) .: (m -tuples_on A) = (D -multiCat) .: {(<*> A)} by FINSEQ_2:94 .= Im ((D -multiCat),{}) .= {((D -multiCat) . {})} by A1, FUNCT_1:59 .= {{}} ; for x, y, d1, d2 being set st x in ((D -multiCat) .: (m -tuples_on A)) /\ (D *) & y in ((D -multiCat) .: (m -tuples_on A)) /\ (D *) & d1 in D * & d2 in D * & f . (x,d1) = f . (y,d2) holds ( x = y & d1 = d2 ) proof let x, y, d1, d2 be set ; ::_thesis: ( x in ((D -multiCat) .: (m -tuples_on A)) /\ (D *) & y in ((D -multiCat) .: (m -tuples_on A)) /\ (D *) & d1 in D * & d2 in D * & f . (x,d1) = f . (y,d2) implies ( x = y & d1 = d2 ) ) assume C1: ( x in ((D -multiCat) .: (m -tuples_on A)) /\ (D *) & y in ((D -multiCat) .: (m -tuples_on A)) /\ (D *) & d1 in D * & d2 in D * & f . (x,d1) = f . (y,d2) ) ; ::_thesis: ( x = y & d1 = d2 ) then ( x in (D -multiCat) .: (m -tuples_on A) & x in D * & y in (D -multiCat) .: (m -tuples_on A) & y in D * ) by XBOOLE_0:def_4; then C3: ( x = {} & y = {} ) by Z1, TARSKI:def_1; reconsider xx = x as Element of D * by C1; reconsider yy = y as Element of D * by C1; reconsider d11 = d1 as Element of D * by C1; reconsider d22 = d2 as Element of D * by C1; d11 = xx ^ d11 by C3, FINSEQ_1:34 .= f . (yy,d22) by ThConcatenation, C1 .= {} ^ d22 by C3, ThConcatenation .= d22 by FINSEQ_1:34 ; hence ( x = y & d1 = d2 ) by C3; ::_thesis: verum end; then (D -multiCat) .: (m -tuples_on A) is f -unambiguous by DefUnambiguous2; hence ( A is D -prefix implies (D -multiCat) .: (m -tuples_on A) is D -prefix ) by DefPrefix; ::_thesis: verum end; suppose m <> 0 ; ::_thesis: ( A is D -prefix implies (D -multiCat) .: (m -tuples_on A) is D -prefix ) then consider k being Nat such that C0: m = k + 1 by NAT_1:6; set B = (k + 1) -tuples_on A; (k + 1) -tuples_on A misses 0 -tuples_on A by Lm18; then (k + 1) -tuples_on A misses {{}} by COMPUT_1:5; then C1: ((k + 1) -tuples_on A) \ {{}} = (k + 1) -tuples_on A by XBOOLE_1:83; assume A is D -prefix ; ::_thesis: (D -multiCat) .: (m -tuples_on A) is D -prefix then A is f -unambiguous by DefPrefix; then C2: (MultPlace f) .: ((k + 1) -tuples_on A) is f -unambiguous by Lm15; (D -multiCat) .: ((k + 1) -tuples_on A) = ((D -multiCat) | (((k + 1) -tuples_on A) \ {{}})) .: (((k + 1) -tuples_on A) \ {{}}) by C1, RELAT_1:129 .= ((MultPlace f) | ((k + 1) -tuples_on A)) .: ((k + 1) -tuples_on A) by C1, Lm16 .= (MultPlace f) .: ((k + 1) -tuples_on A) by RELAT_1:129 ; hence (D -multiCat) .: (m -tuples_on A) is D -prefix by C0, C2, DefPrefix; ::_thesis: verum end; end; end; theorem :: FOMODEL0:8 for D being non empty set for A being set for m being Nat st A is D -prefix holds D -multiCat is m -tuples_on A -one-to-one proof let D be non empty set ; ::_thesis: for A being set for m being Nat st A is D -prefix holds D -multiCat is m -tuples_on A -one-to-one let A be set ; ::_thesis: for m being Nat st A is D -prefix holds D -multiCat is m -tuples_on A -one-to-one let m be Nat; ::_thesis: ( A is D -prefix implies D -multiCat is m -tuples_on A -one-to-one ) set f = D -concatenation ; set F = D -multiCat ; set Z = m -tuples_on A; assume A is D -prefix ; ::_thesis: D -multiCat is m -tuples_on A -one-to-one then B1: ( D -concatenation is associative & A is D -concatenation -unambiguous ) by DefPrefix; percases ( m = 0 or m <> 0 ) ; suppose m = 0 ; ::_thesis: D -multiCat is m -tuples_on A -one-to-one then m -tuples_on A = Funcs ((Seg 0),A) by Lm21 .= {{}} by FUNCT_5:57 ; then (D -multiCat) | (m -tuples_on A) is one-to-one ; hence D -multiCat is m -tuples_on A -one-to-one by DefInj1; ::_thesis: verum end; suppose m <> 0 ; ::_thesis: D -multiCat is m -tuples_on A -one-to-one then consider k being Nat such that C1: m = k + 1 by NAT_1:6; reconsider kk = k + 1 as Element of NAT by ORDINAL1:def_12; set ZZ = kk -tuples_on A; MultPlace (D -concatenation) is kk -tuples_on A -one-to-one by B1, Lm26; then C2: (MultPlace (D -concatenation)) | (kk -tuples_on A) is one-to-one by DefInj1; len {} = 0 ; then not {} in kk -tuples_on A by FINSEQ_2:132; then {{}} misses kk -tuples_on A by ZFMISC_1:50; then (kk -tuples_on A) \ {{}} = kk -tuples_on A by XBOOLE_1:83; then (D -multiCat) | (m -tuples_on A) is one-to-one by Lm16, C2, C1; hence D -multiCat is m -tuples_on A -one-to-one by DefInj1; ::_thesis: verum end; end; end; theorem :: FOMODEL0:9 for Y being set for m being Nat holds (m + 1) -tuples_on Y c= (Y *) \ {{}} proof let Y be set ; ::_thesis: for m being Nat holds (m + 1) -tuples_on Y c= (Y *) \ {{}} let m be Nat; ::_thesis: (m + 1) -tuples_on Y c= (Y *) \ {{}} reconsider k = m, K = m + 1 as Element of NAT by ORDINAL1:def_12; A1: 0 -tuples_on Y misses K -tuples_on Y by Lm18; K -tuples_on Y c= (Y *) \ (0 -tuples_on Y) by A1, FINSEQ_2:134, XBOOLE_1:86; hence (m + 1) -tuples_on Y c= (Y *) \ {{}} by COMPUT_1:5; ::_thesis: verum end; theorem :: FOMODEL0:10 for Y being set for m being Nat st m is zero holds m -tuples_on Y = {{}} by COMPUT_1:5; theorem :: FOMODEL0:11 for Y being set for i being Nat holds i -tuples_on Y = Funcs ((Seg i),Y) by Lm21; theorem :: FOMODEL0:12 for x, A being set for m being Nat st x in m -tuples_on A holds x is FinSequence of A proof let x, A be set ; ::_thesis: for m being Nat st x in m -tuples_on A holds x is FinSequence of A let m be Nat; ::_thesis: ( x in m -tuples_on A implies x is FinSequence of A ) assume B1: x in m -tuples_on A ; ::_thesis: x is FinSequence of A then reconsider p = x as m -element FinSequence by FINSEQ_2:141; p in Funcs ((Seg m),A) by B1, Lm21; then consider f being Function such that B2: ( p = f & dom f = Seg m & rng f c= A ) by FUNCT_2:def_2; thus x is FinSequence of A by B2, FINSEQ_1:def_4; ::_thesis: verum end; definition let A, X be set ; :: original: chi redefine func chi (A,X) -> Function of X,BOOLEAN; coherence chi (A,X) is Function of X,BOOLEAN proof ( chi (A,X) is Function of X,{{},1} & {{},1} = BOOLEAN ) ; hence chi (A,X) is Function of X,BOOLEAN ; ::_thesis: verum end; end; theorem :: FOMODEL0:13 for D being non empty set for d being Element of D for f being BinOp of D holds ( (MultPlace f) . <*d*> = d & ( for x being non empty FinSequence of D holds (MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d) ) ) by LmMultPlace; theorem Th14: :: FOMODEL0:14 for D being non empty set for d being non empty Element of (D *) * holds (D -multiCat) . d = (MultPlace (D -concatenation)) . d proof let D be non empty set ; ::_thesis: for d being non empty Element of (D *) * holds (D -multiCat) . d = (MultPlace (D -concatenation)) . d let d be non empty Element of (D *) * ; ::_thesis: (D -multiCat) . d = (MultPlace (D -concatenation)) . d set f = D -concatenation ; set F = D -multiCat ; not d in {{}} by TARSKI:def_1; then d in ((D *) *) \ {{}} by XBOOLE_0:def_5; hence (D -multiCat) . d = ((D -multiCat) | (((D *) *) \ {{}})) . d by FUNCT_1:49 .= (MultPlace (D -concatenation)) . d by Lm6 ; ::_thesis: verum end; theorem :: FOMODEL0:15 for D being non empty set for d1, d2 being Element of D * holds (D -multiCat) . <*d1,d2*> = d1 ^ d2 proof let D be non empty set ; ::_thesis: for d1, d2 being Element of D * holds (D -multiCat) . <*d1,d2*> = d1 ^ d2 let d1, d2 be Element of D * ; ::_thesis: (D -multiCat) . <*d1,d2*> = d1 ^ d2 set F = D -multiCat ; set f = D -concatenation ; set d = <*d1,d2*>; reconsider dd = <*d1*> ^ <*d2*> as non empty Element of (D *) * ; B0: (D -multiCat) . dd = (MultPlace (D -concatenation)) . dd by Th14; thus (D -multiCat) . <*d1,d2*> = (D -concatenation) . (((MultPlace (D -concatenation)) . <*d1*>),d2) by LmMultPlace, B0 .= (D -concatenation) . (d1,d2) by LmMultPlace .= d1 ^ d2 by ThConcatenation ; ::_thesis: verum end; registration let f, g be FinSequence; cluster<:f,g:> -> FinSequence-like ; coherence <:f,g:> is FinSequence-like proof set m = len f; set n = len g; set l = min ((len f),(len g)); dom <:f,g:> = Seg (min ((len f),(len g))) by Lm27; hence <:f,g:> is FinSequence-like by FINSEQ_1:def_2; ::_thesis: verum end; end; registration let m be Nat; let f, g be m -element FinSequence; cluster<:f,g:> -> m -element ; coherence <:f,g:> is m -element proof set l = min ((len f),(len g)); Z1: ( len f = m & len g = m ) by CARD_1:def_7; reconsider h = <:f,g:> as FinSequence ; reconsider ll = min ((len f),(len g)) as Element of NAT by ORDINAL1:def_12; dom h = Seg ll by Lm27; then len h = ll by FINSEQ_1:def_3; hence <:f,g:> is m -element by Z1, CARD_1:def_7; ::_thesis: verum end; end; registration let X, Y be set ; let f be X -defined Function; let g be Y -defined Function; cluster<:f,g:> -> X /\ Y -defined for Function; coherence for b1 being Function st b1 = <:f,g:> holds b1 is X /\ Y -defined proof reconsider F = dom f as Subset of X ; reconsider G = dom g as Subset of Y ; set h = <:f,g:>; Z2: dom <:f,g:> = G /\ F by FUNCT_3:def_7; (dom <:f,g:>) /\ (dom <:f,g:>) c= X /\ Y by Z2, XBOOLE_1:27; hence for b1 being Function st b1 = <:f,g:> holds b1 is X /\ Y -defined by RELAT_1:def_18; ::_thesis: verum end; end; registration let X be set ; let f, g be X -defined Function; cluster<:f,g:> -> X -defined for Function; coherence for b1 being Function st b1 = <:f,g:> holds b1 is X -defined ; end; registration let X, Y be set ; let f be X -defined total Function; let g be Y -defined total Function; cluster<:f,g:> -> X /\ Y -defined total for X /\ Y -defined Function; coherence for b1 being X /\ Y -defined Function st b1 = <:f,g:> holds b1 is total proof reconsider h = <:f,g:> as X /\ Y -defined Function ; ( dom f = X & dom g = Y ) by PARTFUN1:def_2; then dom h = X /\ Y by FUNCT_3:def_7; hence for b1 being X /\ Y -defined Function st b1 = <:f,g:> holds b1 is total by PARTFUN1:def_2; ::_thesis: verum end; end; registration let X be set ; let f, g be X -defined total Function; cluster<:f,g:> -> X -defined total for X -defined Function; coherence for b1 being X -defined Function st b1 = <:f,g:> holds b1 is total ; end; registration let X, Y be set ; let f be X -valued Function; let g be Y -valued Function; cluster<:f,g:> -> [:X,Y:] -valued for Function; coherence for b1 being Function st b1 = <:f,g:> holds b1 is [:X,Y:] -valued proof set h = <:f,g:>; rng <:f,g:> c= [:(rng f),(rng g):] by FUNCT_3:51; then rng <:f,g:> c= [:X,Y:] by XBOOLE_1:1; hence for b1 being Function st b1 = <:f,g:> holds b1 is [:X,Y:] -valued by RELAT_1:def_19; ::_thesis: verum end; end; registration let D be non empty set ; cluster Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support for set ; existence ex b1 being FinSequence st b1 is D -valued proof take the FinSequence of D ; ::_thesis: the FinSequence of D is D -valued thus the FinSequence of D is D -valued ; ::_thesis: verum end; end; registration let D be non empty set ; let m be Nat; cluster Relation-like NAT -defined D -valued Function-like finite m -element FinSequence-like FinSubsequence-like countable finite-support for set ; existence ex b1 being D -valued FinSequence st b1 is m -element proof take the m -element FinSequence of D ; ::_thesis: the m -element FinSequence of D is m -element thus the m -element FinSequence of D is m -element ; ::_thesis: verum end; end; registration let X, Y be non empty set ; let f be Function of X,Y; let p be X -valued FinSequence; clusterp * f -> FinSequence-like ; coherence f * p is FinSequence-like proof rng p c= X ; then reconsider pp = p as FinSequence of X by FINSEQ_1:def_4; f * pp is FinSequence of Y ; hence f * p is FinSequence-like ; ::_thesis: verum end; end; registration let X, Y be non empty set ; let m be Nat; let f be Function of X,Y; let p be X -valued m -element FinSequence; clusterp * f -> m -element ; coherence f * p is m -element proof reconsider mm = m as Element of NAT by ORDINAL1:def_12; ( rng p c= X & dom f = X ) by FUNCT_2:def_1; then dom (f * p) = dom p by RELAT_1:27 .= Seg (len p) by FINSEQ_1:def_3 .= Seg mm by CARD_1:def_7 ; then len (f * p) = mm by FINSEQ_1:def_3; hence f * p is m -element by CARD_1:def_7; ::_thesis: verum end; end; definition let D be non empty set ; let f be BinOp of D; let p, q be Element of D * ; funcf AppliedPairwiseTo (p,q) -> FinSequence of D equals :: FOMODEL0:def 12 f * <:p,q:>; coherence f * <:p,q:> is FinSequence of D proof rng (f * <:p,q:>) c= D ; hence f * <:p,q:> is FinSequence of D by FINSEQ_1:def_4; ::_thesis: verum end; end; :: deftheorem defines AppliedPairwiseTo FOMODEL0:def_12_:_ for D being non empty set for f being BinOp of D for p, q being Element of D * holds f AppliedPairwiseTo (p,q) = f * <:p,q:>; registration let D be non empty set ; let f be BinOp of D; let m be Nat; let p, q be m -element Element of D * ; clusterf AppliedPairwiseTo (p,q) -> m -element ; coherence f AppliedPairwiseTo (p,q) is m -element ; end; notation let D be non empty set ; let f be BinOp of D; let p, q be Element of D * ; synonym f _\ (p,q) for f AppliedPairwiseTo (p,q); end; definition redefine func INT equals :: FOMODEL0:def 13 NAT \/ ([:{0},NAT:] \ {[0,0]}); compatibility for b1 being set holds ( b1 = INT iff b1 = NAT \/ ([:{0},NAT:] \ {[0,0]}) ) proof B1: not [0,0] in NAT by ARYTM_3:32; INT = (NAT \ {[0,0]}) \/ ([:{0},NAT:] \ {[0,0]}) by NUMBERS:def_4, XBOOLE_1:42 .= NAT \/ ([:{0},NAT:] \ {[0,0]}) by B1, ZFMISC_1:57 ; hence for b1 being set holds ( b1 = INT iff b1 = NAT \/ ([:{0},NAT:] \ {[0,0]}) ) ; ::_thesis: verum end; end; :: deftheorem defines INT FOMODEL0:def_13_:_ INT = NAT \/ ([:{0},NAT:] \ {[0,0]}); theorem Th16: :: FOMODEL0:16 for Y being set for m being Nat for p being FinSequence st p is Y -valued & p is m -element holds p in m -tuples_on Y proof let Y be set ; ::_thesis: for m being Nat for p being FinSequence st p is Y -valued & p is m -element holds p in m -tuples_on Y let m be Nat; ::_thesis: for p being FinSequence st p is Y -valued & p is m -element holds p in m -tuples_on Y reconsider mm = m as Element of NAT by ORDINAL1:def_12; let p be FinSequence; ::_thesis: ( p is Y -valued & p is m -element implies p in m -tuples_on Y ) assume ( p is Y -valued & p is m -element ) ; ::_thesis: p in m -tuples_on Y then ( rng p c= Y & len p = mm ) by CARD_1:def_7, RELAT_1:def_19; hence p in m -tuples_on Y by FINSEQ_2:132; ::_thesis: verum end; definition let A, B be set ; funcA typed/\ B -> Subset of A equals :: FOMODEL0:def 14 A /\ B; coherence A /\ B is Subset of A by XBOOLE_1:17; funcA /\typed B -> Subset of B equals :: FOMODEL0:def 15 A /\ B; coherence A /\ B is Subset of B by XBOOLE_1:17; end; :: deftheorem defines typed/\ FOMODEL0:def_14_:_ for A, B being set holds A typed/\ B = A /\ B; :: deftheorem defines /\typed FOMODEL0:def_15_:_ for A, B being set holds A /\typed B = A /\ B; registration let A, B be set ; identifyA /\ B with A typed/\ B; compatibility A /\ B = A typed/\ B ; identifyA typed/\ B with A /\ B; compatibility A typed/\ B = A /\ B ; identifyA /\ B with A /\typed B; compatibility A /\ B = A /\typed B ; identifyA /\typed B with A /\ B; compatibility A /\typed B = A /\ B ; end; definition let B, A be set ; funcA null B -> set equals :: FOMODEL0:def 16 A; coherence A is set ; end; :: deftheorem defines null FOMODEL0:def_16_:_ for B, A being set holds A null B = A; registration let A be set ; let B be Subset of A; identifyA /\ B with B null A; compatibility A /\ B = B null A by XBOOLE_1:28; identifyB null A with A /\ B; compatibility B null A = A /\ B ; end; registration let A, B, C be set ; cluster(B \ A) /\ (A /\ C) -> empty for set ; coherence for b1 being set st b1 = (B \ A) /\ (A /\ C) holds b1 is empty proof set X = B \ A; set Y = A /\ C; ( B \ A misses A & A /\ C c= A ) by XBOOLE_1:79; then B \ A misses A /\ C by XBOOLE_1:63; hence for b1 being set st b1 = (B \ A) /\ (A /\ C) holds b1 is empty by XBOOLE_0:def_7; ::_thesis: verum end; end; definition let A, B be set ; funcA typed\ B -> Subset of A equals :: FOMODEL0:def 17 A \ B; coherence A \ B is Subset of A ; end; :: deftheorem defines typed\ FOMODEL0:def_17_:_ for A, B being set holds A typed\ B = A \ B; registration let A, B be set ; identifyA \ B with A typed\ B; compatibility A \ B = A typed\ B ; identifyA typed\ B with A \ B; compatibility A typed\ B = A \ B ; end; definition let A, B be set ; funcA \typed/ B -> Subset of (A \/ B) equals :: FOMODEL0:def 18 A; coherence A is Subset of (A \/ B) by XBOOLE_1:7; end; :: deftheorem defines \typed/ FOMODEL0:def_18_:_ for A, B being set holds A \typed/ B = A; registration let A, B be set ; identifyA \typed/ B with A null B; compatibility A \typed/ B = A null B ; identifyA null B with A \typed/ B; compatibility A null B = A \typed/ B ; end; registration let A be set ; let B be Subset of A; identifyA \/ B with A null B; compatibility A \/ B = A null B by XBOOLE_1:12; identifyA null B with A \/ B; compatibility A null B = A \/ B ; end; Lm43: for m being Nat for g, f being Function st f c= g holds iter (f,m) c= iter (g,m) proof let m be Nat; ::_thesis: for g, f being Function st f c= g holds iter (f,m) c= iter (g,m) let g, f be Function; ::_thesis: ( f c= g implies iter (f,m) c= iter (g,m) ) assume B2: f c= g ; ::_thesis: iter (f,m) c= iter (g,m) defpred S1[ Nat] means iter (f,\$1) c= iter (g,\$1); B0: S1[ 0 ] proof C0: ( iter (f,0) = id (field f) & iter (g,0) = id (field g) ) by FUNCT_7:68; ( dom f c= dom g & rng f c= rng g ) by B2, RELAT_1:11; then (dom f) \/ (rng f) c= (dom g) \/ (rng g) by XBOOLE_1:13; hence S1[ 0 ] by C0, FUNCT_4:3; ::_thesis: verum end; B1: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] then f * (iter (f,n)) c= g * (iter (g,n)) by B2, RELAT_1:31; then iter (f,(n + 1)) c= g * (iter (g,n)) by FUNCT_7:71; hence S1[n + 1] by FUNCT_7:71; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(B0, B1); hence iter (f,m) c= iter (g,m) ; ::_thesis: verum end; Lm31: for R being Relation holds R [*] is_transitive_in field R proof let R be Relation; ::_thesis: R [*] is_transitive_in field R set X = field R; set S = R [*] ; now__::_thesis:_for_x,_y,_z_being_set_st_x_in_field_R_&_y_in_field_R_&_z_in_field_R_&_[x,y]_in_R_[*]_&_[y,z]_in_R_[*]_holds_ [x,z]_in_R_[*] let x, y, z be set ; ::_thesis: ( x in field R & y in field R & z in field R & [x,y] in R [*] & [y,z] in R [*] implies [x,z] in R [*] ) assume C7: ( x in field R & y in field R & z in field R ) ; ::_thesis: ( [x,y] in R [*] & [y,z] in R [*] implies [x,z] in R [*] ) assume C0: ( [x,y] in R [*] & [y,z] in R [*] ) ; ::_thesis: [x,z] in R [*] consider p1 being FinSequence such that C1: ( len p1 >= 1 & p1 . 1 = x & p1 . (len p1) = y & ( for i being Nat st i >= 1 & i < len p1 holds [(p1 . i),(p1 . (i + 1))] in R ) ) by C0, FINSEQ_1:def_16; consider m being Nat such that C5: len p1 = m + 1 by C1, NAT_1:6; consider p2 being FinSequence such that C2: ( len p2 >= 1 & p2 . 1 = y & p2 . (len p2) = z & ( for i being Nat st i >= 1 & i < len p2 holds [(p2 . i),(p2 . (i + 1))] in R ) ) by C0, FINSEQ_1:def_16; C6: 1 in dom p2 by C2, FINSEQ_3:25; reconsider l1 = len p1, l2 = len p2 as non zero Nat by C1, C2; reconsider p11 = p1 | (Seg m) as FinSequence ; set p = p11 ^ p2; Z1: m + 0 < m + 1 by XREAL_1:8; C21: len p11 = m by Z1, C5, FINSEQ_1:17; Z11: m + l2 >= 0 + 1 by C2, XREAL_1:7; C3: for n being Nat st n >= 1 & n <= len p2 holds (p11 ^ p2) . (m + n) = p2 . n proof let n be Nat; ::_thesis: ( n >= 1 & n <= len p2 implies (p11 ^ p2) . (m + n) = p2 . n ) reconsider nn = n as Element of NAT by ORDINAL1:def_12; D0: nn = n ; assume ( n >= 1 & n <= len p2 ) ; ::_thesis: (p11 ^ p2) . (m + n) = p2 . n then n in Seg (len p2) by D0; then n in dom p2 by FINSEQ_1:def_3; hence (p11 ^ p2) . (m + n) = p2 . n by C21, FINSEQ_1:def_7; ::_thesis: verum end; C11: (p11 ^ p2) . 1 = x proof percases ( m = 0 or m <> 0 ) ; supposeD0: m = 0 ; ::_thesis: (p11 ^ p2) . 1 = x thus (p11 ^ p2) . 1 = x by D0, C5, C1, C3, C2; ::_thesis: verum end; suppose m <> 0 ; ::_thesis: (p11 ^ p2) . 1 = x then 0 + 1 <= m by INT_1:7; then 1 in Seg m ; then E0: 1 in dom p11 by Z1, C5, FINSEQ_1:17; hence (p11 ^ p2) . 1 = p11 . 1 by FINSEQ_1:def_7 .= x by C1, E0, FUNCT_1:47 ; ::_thesis: verum end; end; end; l2 in Seg l2 by C2; then l2 in dom p2 by FINSEQ_1:def_3; then Z13: (p11 ^ p2) . ((len p11) + (len p2)) = z by C2, FINSEQ_1:def_7; C13: for i being Nat st i >= 1 & i < len (p11 ^ p2) holds [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R proof let i be Nat; ::_thesis: ( i >= 1 & i < len (p11 ^ p2) implies [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R ) assume Z9: ( i >= 1 & i < len (p11 ^ p2) ) ; ::_thesis: [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R then D1: ( i + 1 >= 1 & i >= 1 & i < len (p11 ^ p2) ) by NAT_1:11; percases ( i < m or i = m or i > m ) by XXREAL_0:1; suppose i < m ; ::_thesis: [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R then E1: ( i < l1 & i < m & i + 1 <= m ) by Z1, C5, INT_1:7, XXREAL_0:2; then ( i in Seg m & i + 1 in Seg m ) by D1, FINSEQ_1:1; then E0: ( i in dom p11 & i + 1 in dom p11 ) by Z1, C5, FINSEQ_1:17; then ( (p11 ^ p2) . i = p11 . i & (p11 ^ p2) . (i + 1) = p11 . (i + 1) ) by FINSEQ_1:def_7; then ( (p11 ^ p2) . i = p1 . i & (p11 ^ p2) . (i + 1) = p1 . (i + 1) ) by E0, FUNCT_1:47; hence [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R by C1, Z9, E1; ::_thesis: verum end; supposeE0: i = m ; ::_thesis: [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R E10: m in dom p11 by E0, Z9, C21, FINSEQ_3:25; then E1: (p11 ^ p2) . m = p11 . m by FINSEQ_1:def_7 .= p1 . m by E10, FUNCT_1:47 ; E2: (p11 ^ p2) . (m + 1) = p1 . (m + 1) by C1, C6, C5, C21, C2, FINSEQ_1:def_7; thus [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R by E0, E1, E2, C1, Z9, Z1, C5; ::_thesis: verum end; supposeE4: i > m ; ::_thesis: [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R then consider j being Nat such that E3: i = m + j by NAT_1:10; j <> 0 by E4, E3; then Z12: j >= 0 + 1 by INT_1:7; then E7: ( j >= 1 & j + 1 >= 1 + 0 ) by XREAL_1:7; m + j < m + l2 by E3, Z9, C21, FINSEQ_1:22; then E5: j < l2 by XREAL_1:7; then E6: ( j <= l2 & j + 1 <= l2 ) by INT_1:7; ( j in Seg l2 & j + 1 in Seg l2 ) by E6, E7, FINSEQ_1:1; then E0: ( j in dom p2 & j + 1 in dom p2 ) by FINSEQ_1:def_3; E1: (p11 ^ p2) . i = p2 . j by E0, E3, C21, FINSEQ_1:def_7; E2: (p11 ^ p2) . (i + 1) = (p11 ^ p2) . ((len p11) + (j + 1)) by E3, C21 .= p2 . (j + 1) by E0, FINSEQ_1:def_7 ; thus [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R by E1, E2, C2, E5, Z12; ::_thesis: verum end; end; end; ( x in field R & z in field R & len (p11 ^ p2) >= 1 & (p11 ^ p2) . 1 = x & (p11 ^ p2) . (len (p11 ^ p2)) = z & ( for i being Nat st i >= 1 & i < len (p11 ^ p2) holds [((p11 ^ p2) . i),((p11 ^ p2) . (i + 1))] in R ) ) by C7, Z11, C21, C11, Z13, C13, FINSEQ_1:22; hence [x,z] in R [*] by FINSEQ_1:def_16; ::_thesis: verum end; hence R [*] is_transitive_in field R by RELAT_2:def_8; ::_thesis: verum end; Lm32: for R being Relation holds field (R [*]) c= field R proof let R be Relation; ::_thesis: field (R [*]) c= field R set RR = R [*] ; set LH = field (R [*]); set RH = field R; now__::_thesis:_for_x_being_set_st_x_in_field_(R_[*])_holds_ x_in_field_R let x be set ; ::_thesis: ( x in field (R [*]) implies b1 in field R ) assume Z0: x in field (R [*]) ; ::_thesis: b1 in field R percases ( x in dom (R [*]) or x in rng (R [*]) ) by Z0, XBOOLE_0:def_3; suppose x in dom (R [*]) ; ::_thesis: b1 in field R then consider y being set such that D0: [x,y] in R [*] by XTUPLE_0:def_12; thus x in field R by D0, FINSEQ_1:def_16; ::_thesis: verum end; suppose x in rng (R [*]) ; ::_thesis: b1 in field R then consider y being set such that D0: [y,x] in R [*] by XTUPLE_0:def_13; thus x in field R by D0, FINSEQ_1:def_16; ::_thesis: verum end; end; end; hence field (R [*]) c= field R by TARSKI:def_3; ::_thesis: verum end; Lm37: for R being Relation holds R [*] is_reflexive_in field R proof let R be Relation; ::_thesis: R [*] is_reflexive_in field R set RR = R [*] ; set X = field R; now__::_thesis:_for_x_being_set_st_x_in_field_R_holds_ [x,x]_in_R_[*] let x be set ; ::_thesis: ( x in field R implies [x,x] in R [*] ) reconsider p = <*x*> as 1 -element FinSequence ; ( len p = 1 & p . 1 = x ) by FINSEQ_1:40; then C0: ( len p >= 1 & p . 1 = x & p . (len p) = x & ( for i being Nat st i >= 1 & i < len p holds [(p . i),(p . (i + 1))] in R ) ) ; assume x in field R ; ::_thesis: [x,x] in R [*] hence [x,x] in R [*] by C0, FINSEQ_1:def_16; ::_thesis: verum end; hence R [*] is_reflexive_in field R by RELAT_2:def_1; ::_thesis: verum end; Lm34: for R being Relation holds field (R [*]) = field R proof let R be Relation; ::_thesis: field (R [*]) = field R set LH = field (R [*]); set RH = field R; B0: field R c= field (R [*]) by LANG1:18, RELAT_1:16; field (R [*]) c= field R by Lm32; hence field (R [*]) = field R by B0, XBOOLE_0:def_10; ::_thesis: verum end; registration let R be Relation; clusterR [*] -> transitive for Relation; coherence for b1 being Relation st b1 = R [*] holds b1 is transitive proof R [*] is_transitive_in field R by Lm31; then R [*] is_transitive_in field (R [*]) by Lm34; hence for b1 being Relation st b1 = R [*] holds b1 is transitive by RELAT_2:def_16; ::_thesis: verum end; clusterR [*] -> reflexive for Relation; coherence for b1 being Relation st b1 = R [*] holds b1 is reflexive proof R [*] is_reflexive_in field R by Lm37; then R [*] is_reflexive_in field (R [*]) by Lm34; hence for b1 being Relation st b1 = R [*] holds b1 is reflexive by RELAT_2:def_9; ::_thesis: verum end; end; Lm38: for f being Function holds iter (f,0) c= f [*] proof let f be Function; ::_thesis: iter (f,0) c= f [*] set LH = iter (f,0); set RH = f [*] ; iter (f,0) = id (field f) by FUNCT_7:68 .= id (field (f [*])) by Lm34 ; hence iter (f,0) c= f [*] by RELAT_2:1; ::_thesis: verum end; Lm39: for m being Nat for f being Function holds iter (f,(m + 1)) c= f [*] proof let m be Nat; ::_thesis: for f being Function holds iter (f,(m + 1)) c= f [*] let f be Function; ::_thesis: iter (f,(m + 1)) c= f [*] set RH = f [*] ; defpred S1[ Nat] means iter (f,(\$1 + 1)) c= f [*] ; B0: S1[ 0 ] proof C0: iter (f,1) = f by FUNCT_7:70; thus S1[ 0 ] by C0, LANG1:18; ::_thesis: verum end; B1: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] then ( iter (f,(n + 1)) c= f [*] & f c= f [*] ) by LANG1:18; then C0: (iter (f,(n + 1))) * f c= (f [*]) * (f [*]) by RELAT_1:31; (f [*]) * (f [*]) c= f [*] by RELAT_2:27; then (iter (f,(n + 1))) * f c= f [*] by C0, XBOOLE_1:1; hence S1[n + 1] by FUNCT_7:69; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(B0, B1); hence iter (f,(m + 1)) c= f [*] ; ::_thesis: verum end; Lm40: for m being Nat for f being Function holds iter (f,m) c= f [*] proof let m be Nat; ::_thesis: for f being Function holds iter (f,m) c= f [*] let f be Function; ::_thesis: iter (f,m) c= f [*] percases ( m = 0 or m <> 0 ) ; suppose m = 0 ; ::_thesis: iter (f,m) c= f [*] hence iter (f,m) c= f [*] by Lm38; ::_thesis: verum end; suppose m <> 0 ; ::_thesis: iter (f,m) c= f [*] then consider n being Nat such that C0: m = n + 1 by NAT_1:6; thus iter (f,m) c= f [*] by Lm39, C0; ::_thesis: verum end; end; end; Lm35: for x being set for m being Nat for g, f being Function st rng f c= dom f & x in dom f & g . 0 = x & ( for i being Nat st i < m holds g . (i + 1) = f . (g . i) ) holds g . m = (iter (f,m)) . x proof let x be set ; ::_thesis: for m being Nat for g, f being Function st rng f c= dom f & x in dom f & g . 0 = x & ( for i being Nat st i < m holds g . (i + 1) = f . (g . i) ) holds g . m = (iter (f,m)) . x let m be Nat; ::_thesis: for g, f being Function st rng f c= dom f & x in dom f & g . 0 = x & ( for i being Nat st i < m holds g . (i + 1) = f . (g . i) ) holds g . m = (iter (f,m)) . x let g, f be Function; ::_thesis: ( rng f c= dom f & x in dom f & g . 0 = x & ( for i being Nat st i < m holds g . (i + 1) = f . (g . i) ) implies g . m = (iter (f,m)) . x ) assume B10: ( rng f c= dom f & x in dom f ) ; ::_thesis: ( not g . 0 = x or ex i being Nat st ( i < m & not g . (i + 1) = f . (g . i) ) or g . m = (iter (f,m)) . x ) then B11: x in (dom f) \/ (rng f) by XBOOLE_0:def_3; defpred S1[ Nat] means ( g . 0 = x & ( for i being Nat st i < \$1 holds g . (i + 1) = f . (g . i) ) implies g . \$1 = (iter (f,\$1)) . x ); B0: S1[ 0 ] proof Z1: iter (f,0) = id (field f) by FUNCT_7:68; assume ( g . 0 = x & ( for i being Nat st i < 0 holds g . (i + 1) = f . (g . i) ) ) ; ::_thesis: g . 0 = (iter (f,0)) . x hence g . 0 = (iter (f,0)) . x by Z1, B11, FUNCT_1:17; ::_thesis: verum end; B1: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume C0: S1[n] ; ::_thesis: S1[n + 1] assume C1: g . 0 = x ; ::_thesis: ( ex i being Nat st ( i < n + 1 & not g . (i + 1) = f . (g . i) ) or g . (n + 1) = (iter (f,(n + 1))) . x ) assume C2: for i being Nat st i < n + 1 holds g . (i + 1) = f . (g . i) ; ::_thesis: g . (n + 1) = (iter (f,(n + 1))) . x Z3: for i being Nat st i < n holds g . (i + 1) = f . (g . i) proof let i be Nat; ::_thesis: ( i < n implies g . (i + 1) = f . (g . i) ) assume i < n ; ::_thesis: g . (i + 1) = f . (g . i) then i + 0 < n + 1 by XREAL_1:8; hence g . (i + 1) = f . (g . i) by C2; ::_thesis: verum end; C4: x in dom (iter (f,n)) by B10, FUNCT_7:74; n + 0 < n + 1 by XREAL_1:8; then g . (n + 1) = f . (g . n) by C2 .= (f * (iter (f,n))) . x by C4, Z3, C0, C1, FUNCT_1:13 .= (iter (f,(n + 1))) . x by FUNCT_7:71 ; hence g . (n + 1) = (iter (f,(n + 1))) . x ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(B0, B1); hence ( not g . 0 = x or ex i being Nat st ( i < m & not g . (i + 1) = f . (g . i) ) or g . m = (iter (f,m)) . x ) ; ::_thesis: verum end; definition func plus -> Function of COMPLEX,COMPLEX means :DefPlus: :: FOMODEL0:def 19 for z being complex number holds it . z = z + 1; existence ex b1 being Function of COMPLEX,COMPLEX st for z being complex number holds b1 . z = z + 1 proof defpred S1[ set , set ] means for z being complex number st z = \$1 holds \$2 = z + 1; B0: for x being Element of COMPLEX ex zz being Element of COMPLEX st S1[x,zz] proof let x be Element of COMPLEX ; ::_thesis: ex zz being Element of COMPLEX st S1[x,zz] reconsider z0 = x as complex number ; reconsider z1 = z0 + 1 as Element of COMPLEX by XCMPLX_0:def_2; take z1 ; ::_thesis: S1[x,z1] thus S1[x,z1] ; ::_thesis: verum end; consider f being Function of COMPLEX,COMPLEX such that B1: for x being Element of COMPLEX holds S1[x,f . x] from FUNCT_2:sch_3(B0); take f ; ::_thesis: for z being complex number holds f . z = z + 1 now__::_thesis:_for_z_being_complex_number_holds_f_._z_=_z_+_1 let z be complex number ; ::_thesis: f . z = z + 1 reconsider zz = z as Element of COMPLEX by XCMPLX_0:def_2; ( z = zz & S1[zz,f . zz] ) by B1; hence f . z = z + 1 ; ::_thesis: verum end; hence for z being complex number holds f . z = z + 1 ; ::_thesis: verum end; uniqueness for b1, b2 being Function of COMPLEX,COMPLEX st ( for z being complex number holds b1 . z = z + 1 ) & ( for z being complex number holds b2 . z = z + 1 ) holds b1 = b2 proof let IT1, IT2 be Function of COMPLEX,COMPLEX; ::_thesis: ( ( for z being complex number holds IT1 . z = z + 1 ) & ( for z being complex number holds IT2 . z = z + 1 ) implies IT1 = IT2 ) assume B1: for z being complex number holds IT1 . z = z + 1 ; ::_thesis: ( ex z being complex number st not IT2 . z = z + 1 or IT1 = IT2 ) assume B2: for z being complex number holds IT2 . z = z + 1 ; ::_thesis: IT1 = IT2 now__::_thesis:_for_zz_being_Element_of_COMPLEX_holds_IT1_._zz_=_IT2_._zz let zz be Element of COMPLEX ; ::_thesis: IT1 . zz = IT2 . zz thus IT1 . zz = zz + 1 by B1 .= IT2 . zz by B2 ; ::_thesis: verum end; hence IT1 = IT2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem DefPlus defines plus FOMODEL0:def_19_:_ for b1 being Function of COMPLEX,COMPLEX holds ( b1 = plus iff for z being complex number holds b1 . z = z + 1 ); Lm36: for x being set for m being Nat for f being Function for p being FinSequence st rng f c= dom f & x in dom f & p . 1 = x & ( for i being Nat st i >= 1 & i < m + 1 holds p . (i + 1) = f . (p . i) ) holds p . (m + 1) = (iter (f,m)) . x proof let x be set ; ::_thesis: for m being Nat for f being Function for p being FinSequence st rng f c= dom f & x in dom f & p . 1 = x & ( for i being Nat st i >= 1 & i < m + 1 holds p . (i + 1) = f . (p . i) ) holds p . (m + 1) = (iter (f,m)) . x let m be Nat; ::_thesis: for f being Function for p being FinSequence st rng f c= dom f & x in dom f & p . 1 = x & ( for i being Nat st i >= 1 & i < m + 1 holds p . (i + 1) = f . (p . i) ) holds p . (m + 1) = (iter (f,m)) . x let f be Function; ::_thesis: for p being FinSequence st rng f c= dom f & x in dom f & p . 1 = x & ( for i being Nat st i >= 1 & i < m + 1 holds p . (i + 1) = f . (p . i) ) holds p . (m + 1) = (iter (f,m)) . x let p be FinSequence; ::_thesis: ( rng f c= dom f & x in dom f & p . 1 = x & ( for i being Nat st i >= 1 & i < m + 1 holds p . (i + 1) = f . (p . i) ) implies p . (m + 1) = (iter (f,m)) . x ) B4: dom plus = COMPLEX by FUNCT_2:def_1; then reconsider Z = 0 as Element of dom plus by XCMPLX_0:def_2; reconsider g = p * plus as Function ; B2: for z being complex number holds g . z = p . (z + 1) proof let z be complex number ; ::_thesis: g . z = p . (z + 1) reconsider zz = z as Element of dom plus by B4, XCMPLX_0:def_2; thus g . z = p . (plus . zz) by FUNCT_1:13 .= p . (z + 1) by DefPlus ; ::_thesis: verum end; assume B10: ( rng f c= dom f & x in dom f ) ; ::_thesis: ( not p . 1 = x or ex i being Nat st ( i >= 1 & i < m + 1 & not p . (i + 1) = f . (p . i) ) or p . (m + 1) = (iter (f,m)) . x ) assume p . 1 = x ; ::_thesis: ( ex i being Nat st ( i >= 1 & i < m + 1 & not p . (i + 1) = f . (p . i) ) or p . (m + 1) = (iter (f,m)) . x ) then p . (0 + 1) = x ; then B0: g . 0 = x by B2; assume B3: for i being Nat st i >= 1 & i < m + 1 holds p . (i + 1) = f . (p . i) ; ::_thesis: p . (m + 1) = (iter (f,m)) . x now__::_thesis:_for_j_being_Nat_st_j_<_m_holds_ g_._(j_+_1)_=_f_._(g_._j) let j be Nat; ::_thesis: ( j < m implies g . (j + 1) = f . (g . j) ) reconsider jz = j as complex number ; assume j < m ; ::_thesis: g . (j + 1) = f . (g . j) then ( j + 1 >= 0 + 1 & j + 1 < m + 1 ) by XREAL_1:7, XREAL_1:8; then p . ((j + 1) + 1) = f . (p . (j + 1)) by B3 .= f . (g . j) by B2 ; hence g . (j + 1) = f . (g . j) by B2; ::_thesis: verum end; then g . m = (iter (f,m)) . x by Lm35, B0, B10; hence p . (m + 1) = (iter (f,m)) . x by B2; ::_thesis: verum end; Lm41: for z being set for f being Function st z in f [*] & rng f c= dom f holds ex n being Nat st z in iter (f,n) proof let z be set ; ::_thesis: for f being Function st z in f [*] & rng f c= dom f holds ex n being Nat st z in iter (f,n) let f be Function; ::_thesis: ( z in f [*] & rng f c= dom f implies ex n being Nat st z in iter (f,n) ) set LH = f [*] ; assume C19: z in f [*] ; ::_thesis: ( not rng f c= dom f or ex n being Nat st z in iter (f,n) ) then consider x, y being set such that C8: z = [x,y] by RELAT_1:def_1; consider p being FinSequence such that C0: ( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds [(p . i),(p . (i + 1))] in f ) ) by C8, C19, FINSEQ_1:def_16; assume C9: rng f c= dom f ; ::_thesis: ex n being Nat st z in iter (f,n) then Z2: ( field f = dom f & x in field f ) by C8, C19, FINSEQ_1:def_16, XBOOLE_1:12; consider m being Nat such that C1: m + 1 = len p by C0, NAT_1:6; take m ; ::_thesis: z in iter (f,m) for i being Nat st i >= 1 & i < len p holds ( p . i in dom f & p . (i + 1) = f . (p . i) ) proof let i be Nat; ::_thesis: ( i >= 1 & i < len p implies ( p . i in dom f & p . (i + 1) = f . (p . i) ) ) assume ( i >= 1 & i < len p ) ; ::_thesis: ( p . i in dom f & p . (i + 1) = f . (p . i) ) then D0: [(p . i),(p . (i + 1))] in f by C0; hence p . i in dom f by XTUPLE_0:def_12; ::_thesis: p . (i + 1) = f . (p . i) hence p . (i + 1) = f . (p . i) by D0, FUNCT_1:def_2; ::_thesis: verum end; then C2: ( m + 1 >= 1 & p . 1 = x & p . (m + 1) = y & ( for i being Nat st i >= 1 & i < m + 1 holds p . (i + 1) = f . (p . i) ) ) by C0, C1; ( x in dom (iter (f,m)) & p . (m + 1) = (iter (f,m)) . x ) by Z2, C9, C2, Lm36, FUNCT_7:74; hence z in iter (f,m) by C8, C0, C1, FUNCT_1:1; ::_thesis: verum end; Lm42: for f being Function st rng f c= dom f holds f [*] = union { (iter (f,mm)) where mm is Element of NAT : verum } proof let f be Function; ::_thesis: ( rng f c= dom f implies f [*] = union { (iter (f,mm)) where mm is Element of NAT : verum } ) set F = { (iter (f,mm)) where mm is Element of NAT : verum } ; set LH = f [*] ; set RH = union { (iter (f,mm)) where mm is Element of NAT : verum } ; now__::_thesis:_for_x_being_set_st_x_in_union__{__(iter_(f,mm))_where_mm_is_Element_of_NAT_:_verum__}__holds_ x_in_f_[*] let x be set ; ::_thesis: ( x in union { (iter (f,mm)) where mm is Element of NAT : verum } implies x in f [*] ) assume x in union { (iter (f,mm)) where mm is Element of NAT : verum } ; ::_thesis: x in f [*] then consider X being set such that C0: ( x in X & X in { (iter (f,mm)) where mm is Element of NAT : verum } ) by TARSKI:def_4; consider mm being Element of NAT such that C1: X = iter (f,mm) by C0; ( x in iter (f,mm) & iter (f,mm) c= f [*] ) by C0, C1, Lm40; hence x in f [*] ; ::_thesis: verum end; then B1: union { (iter (f,mm)) where mm is Element of NAT : verum } c= f [*] by TARSKI:def_3; assume B0: rng f c= dom f ; ::_thesis: f [*] = union { (iter (f,mm)) where mm is Element of NAT : verum } now__::_thesis:_for_x_being_set_st_x_in_f_[*]_holds_ x_in_union__{__(iter_(f,mm))_where_mm_is_Element_of_NAT_:_verum__}_ let x be set ; ::_thesis: ( x in f [*] implies x in union { (iter (f,mm)) where mm is Element of NAT : verum } ) assume x in f [*] ; ::_thesis: x in union { (iter (f,mm)) where mm is Element of NAT : verum } then consider m being Nat such that C0: x in iter (f,m) by B0, Lm41; reconsider mm = m as Element of NAT by ORDINAL1:def_12; ( x in iter (f,mm) & iter (f,mm) in { (iter (f,mm)) where mm is Element of NAT : verum } ) by C0; hence x in union { (iter (f,mm)) where mm is Element of NAT : verum } by TARSKI:def_4; ::_thesis: verum end; then B2: f [*] c= union { (iter (f,mm)) where mm is Element of NAT : verum } by TARSKI:def_3; thus f [*] = union { (iter (f,mm)) where mm is Element of NAT : verum } by B1, B2, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: FOMODEL0:17 for f being Function st rng f c= dom f holds f [*] = union { (iter (f,mm)) where mm is Element of NAT : verum } by Lm42; theorem :: FOMODEL0:18 for m being Nat for g, f being Function st f c= g holds iter (f,m) c= iter (g,m) by Lm43; registration let X be functional set ; cluster union X -> Relation-like ; coherence union X is Relation-like proof now__::_thesis:_for_x_being_set_st_x_in_union_X_holds_ ex_y,_z_being_set_st_x_=_[y,z] let x be set ; ::_thesis: ( x in union X implies ex y, z being set st x = [y,z] ) assume x in union X ; ::_thesis: ex y, z being set st x = [y,z] then consider Y being set such that C0: ( x in Y & Y in X ) by TARSKI:def_4; thus ex y, z being set st x = [y,z] by C0, RELAT_1:def_1; ::_thesis: verum end; hence union X is Relation-like by RELAT_1:def_1; ::_thesis: verum end; end; theorem :: FOMODEL0:19 for Y, A, B being set st Y c= Funcs (A,B) holds union Y c= [:A,B:] by Lm28; registration let Y be set ; clusterY \ Y -> empty for set ; coherence for b1 being set st b1 = Y \ Y holds b1 is empty by XBOOLE_1:37; end; registration let D be non empty set ; let d be Element of D; cluster{((id D) . d)} \ {d} -> empty for set ; coherence for b1 being set st b1 = {((id D) . d)} \ {d} holds b1 is empty proof (id D) . d = d by FUNCT_1:17; hence for b1 being set st b1 = {((id D) . d)} \ {d} holds b1 is empty ; ::_thesis: verum end; end; registration let p be FinSequence; let q be empty FinSequence; identifyp ^ q with p null q; compatibility p ^ q = p null q by FINSEQ_1:34; identifyp null q with p ^ q; compatibility p null q = p ^ q ; identifyq ^ p with p null q; compatibility q ^ p = p null q by FINSEQ_1:34; identifyp null q with q ^ p; compatibility p null q = q ^ p ; end; registration let Y be set ; let R be Y -defined Relation; identifyR | Y with R null Y; compatibility R | Y = R null Y proof thus R | Y = R null Y ; ::_thesis: verum end; identifyR null Y with R | Y; compatibility R null Y = R | Y ; end; theorem Th20: :: FOMODEL0:20 for f being Function holds f = { [x,(f . x)] where x is Element of dom f : x in dom f } proof let f be Function; ::_thesis: f = { [x,(f . x)] where x is Element of dom f : x in dom f } set RH = { [x,(f . x)] where x is Element of dom f : x in dom f } ; now__::_thesis:_for_z_being_set_st_z_in_f_holds_ z_in__{__[x,(f_._x)]_where_x_is_Element_of_dom_f_:_x_in_dom_f__}_ let z be set ; ::_thesis: ( z in f implies z in { [x,(f . x)] where x is Element of dom f : x in dom f } ) assume C2: z in f ; ::_thesis: z in { [x,(f . x)] where x is Element of dom f : x in dom f } then consider x, y being set such that C0: z = [x,y] by RELAT_1:def_1; reconsider xx = x as Element of dom f by C0, C2, FUNCT_1:1; ( z = [xx,(f . xx)] & xx in dom f ) by C0, C2, FUNCT_1:1; hence z in { [x,(f . x)] where x is Element of dom f : x in dom f } ; ::_thesis: verum end; then B0: f c= { [x,(f . x)] where x is Element of dom f : x in dom f } by TARSKI:def_3; now__::_thesis:_for_z_being_set_st_z_in__{__[x,(f_._x)]_where_x_is_Element_of_dom_f_:_x_in_dom_f__}__holds_ z_in_f let z be set ; ::_thesis: ( z in { [x,(f . x)] where x is Element of dom f : x in dom f } implies z in f ) assume C0: z in { [x,(f . x)] where x is Element of dom f : x in dom f } ; ::_thesis: z in f consider x being Element of dom f such that D0: ( z = [x,(f . x)] & x in dom f ) by C0; thus z in f by D0, FUNCT_1:1; ::_thesis: verum end; then { [x,(f . x)] where x is Element of dom f : x in dom f } c= f by TARSKI:def_3; hence f = { [x,(f . x)] where x is Element of dom f : x in dom f } by B0, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th21: :: FOMODEL0:21 for Y being set for R being b1 -defined total Relation holds id Y c= R * (R ~) proof let Y be set ; ::_thesis: for R being Y -defined total Relation holds id Y c= R * (R ~) set X = Y; let R be Y -defined total Relation; ::_thesis: id Y c= R * (R ~) reconsider f = id Y as Function ; B0: f = { [x,(f . x)] where x is Element of dom f : x in dom f } by Th20; now__::_thesis:_for_z_being_set_st_z_in_f_holds_ z_in_R_*_(R_~) let z be set ; ::_thesis: ( z in f implies z in R * (R ~) ) assume z in f ; ::_thesis: z in R * (R ~) then consider x being Element of dom f such that C2: ( z = [x,((id Y) . x)] & x in dom (id Y) ) by B0; C0: ( x in Y & z = [x,x] ) by C2, FUNCT_1:17; x in dom R by C0, PARTFUN1:def_2; then consider y being set such that C1: [x,y] in R by XTUPLE_0:def_12; [y,x] in R ~ by C1, RELAT_1:def_7; then [x,x] in R * (R ~) by C1, RELAT_1:def_8; hence z in R * (R ~) by C2, FUNCT_1:17; ::_thesis: verum end; hence id Y c= R * (R ~) by TARSKI:def_3; ::_thesis: verum end; theorem :: FOMODEL0:22 for D being non empty set for m, n being Nat holds (m + n) -tuples_on D = (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] proof let D be non empty set ; ::_thesis: for m, n being Nat holds (m + n) -tuples_on D = (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] let m, n be Nat; ::_thesis: (m + n) -tuples_on D = (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] reconsider m = m, n = n as Element of NAT by ORDINAL1:def_12; set U = D; set LH = (m + n) -tuples_on D; set M = m -tuples_on D; set N = n -tuples_on D; set C = D -concatenation ; set RH = (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):]; B0: (m + n) -tuples_on D = { (z ^ t) where z is Tuple of m,D, t is Tuple of n,D : verum } by FINSEQ_2:105; B1: dom (D -concatenation) = [:(D *),(D *):] by FUNCT_2:def_1; ( m -tuples_on D c= D * & n -tuples_on D c= D * ) by FINSEQ_2:134; then B2: [:(m -tuples_on D),(n -tuples_on D):] c= [:(D *),(D *):] by ZFMISC_1:96; now__::_thesis:_for_y_being_set_st_y_in_(m_+_n)_-tuples_on_D_holds_ y_in_(D_-concatenation)_.:_[:(m_-tuples_on_D),(n_-tuples_on_D):] let y be set ; ::_thesis: ( y in (m + n) -tuples_on D implies y in (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] ) assume y in (m + n) -tuples_on D ; ::_thesis: y in (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] then consider Tz being Tuple of m,D, Tt being Tuple of n,D such that C0: y = Tz ^ Tt by B0; reconsider zz = Tz as Element of m -tuples_on D by FINSEQ_2:131; reconsider tt = Tt as Element of n -tuples_on D by FINSEQ_2:131; reconsider x = [zz,tt] as Element of [:(m -tuples_on D),(n -tuples_on D):] ; reconsider xx = x as Element of dom (D -concatenation) by B1, B2, TARSKI:def_3; C1: (D -concatenation) .: {x} c= (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] by RELAT_1:123; y = (D -concatenation) . (Tz,Tt) by C0, ThConcatenation .= (D -concatenation) . x ; then y in {((D -concatenation) . xx)} by TARSKI:def_1; then y in Im ((D -concatenation),xx) by FUNCT_1:59; hence y in (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] by C1; ::_thesis: verum end; then B3: (m + n) -tuples_on D c= (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] by TARSKI:def_3; now__::_thesis:_for_y_being_set_st_y_in_(D_-concatenation)_.:_[:(m_-tuples_on_D),(n_-tuples_on_D):]_holds_ y_in_(m_+_n)_-tuples_on_D let y be set ; ::_thesis: ( y in (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] implies y in (m + n) -tuples_on D ) assume y in (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] ; ::_thesis: y in (m + n) -tuples_on D then consider x being set such that C0: ( x in dom (D -concatenation) & x in [:(m -tuples_on D),(n -tuples_on D):] & y = (D -concatenation) . x ) by FUNCT_1:def_6; consider z, t being set such that C1: ( z in m -tuples_on D & t in n -tuples_on D & x = [z,t] ) by C0, ZFMISC_1:def_2; reconsider zz = z as Element of m -tuples_on D by C1; reconsider tt = t as Element of n -tuples_on D by C1; reconsider zzz = zz, ttt = tt as FinSequence of D ; reconsider Tz = zz as Tuple of m,D ; reconsider Tt = tt as Tuple of n,D ; y = (D -concatenation) . (zzz,ttt) by C0, C1 .= Tz ^ Tt by ThConcatenation ; hence y in (m + n) -tuples_on D by B0; ::_thesis: verum end; then (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] c= (m + n) -tuples_on D by TARSKI:def_3; hence (m + n) -tuples_on D = (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] by B3, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th23: :: FOMODEL0:23 for Y being set for P, Q being Relation holds (P \/ Q) " Y = (P " Y) \/ (Q " Y) proof let Y be set ; ::_thesis: for P, Q being Relation holds (P \/ Q) " Y = (P " Y) \/ (Q " Y) let P, Q be Relation; ::_thesis: (P \/ Q) " Y = (P " Y) \/ (Q " Y) set R = P \/ Q; set LH = (P \/ Q) " Y; set RH = (P " Y) \/ (Q " Y); reconsider PP = P null Q, QQ = Q null P as Subset of (P \/ Q) ; now__::_thesis:_for_x_being_set_st_x_in_(P_\/_Q)_"_Y_holds_ x_in_(P_"_Y)_\/_(Q_"_Y) let x be set ; ::_thesis: ( x in (P \/ Q) " Y implies x in (P " Y) \/ (Q " Y) ) assume x in (P \/ Q) " Y ; ::_thesis: x in (P " Y) \/ (Q " Y) then consider y being set such that C0: ( [x,y] in P \/ Q & y in Y ) by RELAT_1:def_14; set z = [x,y]; ( ( [x,y] in P & y in Y ) or ( [x,y] in Q & y in Y ) ) by C0, XBOOLE_0:def_3; then ( x in P " Y or x in Q " Y ) by RELAT_1:def_14; hence x in (P " Y) \/ (Q " Y) by XBOOLE_0:def_3; ::_thesis: verum end; then B0: (P \/ Q) " Y c= (P " Y) \/ (Q " Y) by TARSKI:def_3; reconsider PX = PP " Y, QX = QQ " Y as Subset of ((P \/ Q) " Y) by RELAT_1:144; PX \/ QX c= (P \/ Q) " Y ; hence (P \/ Q) " Y = (P " Y) \/ (Q " Y) by B0, XBOOLE_0:def_10; ::_thesis: verum end; Lm4: for A, B being set holds chi (A,B) = (B --> 0) +* ((A /\ B) --> 1) proof let A, B be set ; ::_thesis: chi (A,B) = (B --> 0) +* ((A /\ B) --> 1) set f = B --> 0; set g = (A /\ B) --> 1; set IT = (B --> 0) +* ((A /\ B) --> 1); B1: ( dom (B --> 0) = B & dom ((A /\ B) --> 1) = A /\ B & dom ((B --> 0) +* ((A /\ B) --> 1)) = (dom (B --> 0)) \/ (dom ((A /\ B) --> 1)) ) by FUNCOP_1:13, FUNCT_4:def_1; B0: dom ((B --> 0) +* ((A /\ B) --> 1)) = B by B1, XBOOLE_1:22; now__::_thesis:_for_x_being_set_st_x_in_B_holds_ (_(_x_in_A_implies_((B_-->_0)_+*_((A_/\_B)_-->_1))_._x_=_1_)_&_(_not_x_in_A_implies_((B_-->_0)_+*_((A_/\_B)_-->_1))_._x_=_{}_)_) let x be set ; ::_thesis: ( x in B implies ( ( x in A implies ((B --> 0) +* ((A /\ B) --> 1)) . x = 1 ) & ( not x in A implies ((B --> 0) +* ((A /\ B) --> 1)) . x = {} ) ) ) assume Z0: x in B ; ::_thesis: ( ( x in A implies ((B --> 0) +* ((A /\ B) --> 1)) . x = 1 ) & ( not x in A implies ((B --> 0) +* ((A /\ B) --> 1)) . x = {} ) ) then C0: ( x in B & x in dom ((B --> 0) +* ((A /\ B) --> 1)) & x in (dom (B --> 0)) \/ (dom ((A /\ B) --> 1)) ) by B1, XBOOLE_1:22; thus ( x in A implies ((B --> 0) +* ((A /\ B) --> 1)) . x = 1 ) ::_thesis: ( not x in A implies ((B --> 0) +* ((A /\ B) --> 1)) . x = {} ) proof assume Z1: x in A ; ::_thesis: ((B --> 0) +* ((A /\ B) --> 1)) . x = 1 then D0: x in A /\ B by Z0, XBOOLE_0:def_4; x in dom ((A /\ B) --> 1) by Z1, Z0, B1, XBOOLE_0:def_4; then ((B --> 0) +* ((A /\ B) --> 1)) . x = ((A /\ B) --> 1) . x by C0, FUNCT_4:def_1 .= 1 by D0, FUNCOP_1:7 ; hence ((B --> 0) +* ((A /\ B) --> 1)) . x = 1 ; ::_thesis: verum end; thus ( not x in A implies ((B --> 0) +* ((A /\ B) --> 1)) . x = {} ) ::_thesis: verum proof assume not x in A ; ::_thesis: ((B --> 0) +* ((A /\ B) --> 1)) . x = {} then not x in A /\ B ; then not x in dom ((A /\ B) --> 1) ; then ((B --> 0) +* ((A /\ B) --> 1)) . x = (B --> 0) . x by C0, FUNCT_4:def_1 .= 0 by Z0, FUNCOP_1:7 ; hence ((B --> 0) +* ((A /\ B) --> 1)) . x = {} ; ::_thesis: verum end; end; hence chi (A,B) = (B --> 0) +* ((A /\ B) --> 1) by B0, FUNCT_3:def_3; ::_thesis: verum end; Lm10: for A, B being set holds chi (A,B) = ((B \ A) --> 0) +* ((A /\ B) --> 1) proof let A, B be set ; ::_thesis: chi (A,B) = ((B \ A) --> 0) +* ((A /\ B) --> 1) set Z = B \ A; set O = A /\ B; set f = B --> 0; set g = (A /\ B) --> 1; set IT = chi (A,B); reconsider BB = B /\ B, OO = A /\ B, ZZ = B \ A as Subset of B ; reconsider OOO = (A /\ B) /\ (A /\ B) as Subset of (A /\ B) ; B4: ( (A /\ B) \/ (B \ A) = B & dom (chi (A,B)) = BB ) by FUNCT_3:def_3, XBOOLE_1:51; B0: ( B /\ OO = OO & (B \ A) /\ (A /\ B) = {} & B /\ ZZ = ZZ ) ; B1: ( ((B --> 0) +* ((A /\ B) --> 1)) | (B \ A) = ((B --> 0) | (B \ A)) +* (((A /\ B) --> 1) | (B \ A)) & ((B --> 0) +* ((A /\ B) --> 1)) | (A /\ B) = ((B --> 0) | (A /\ B)) +* (((A /\ B) --> 1) | (A /\ B)) ) by FUNCT_4:71; B2: ( (B --> 0) | (B \ A) = (B /\ (B \ A)) --> 0 & ((A /\ B) --> 1) | (B \ A) = {} --> 1 & (B --> 0) | (A /\ B) = OOO --> 0 & ((A /\ B) --> 1) | (A /\ B) = (A /\ B) --> 1 ) by B0, FUNCOP_1:12; then ( dom ((B --> 0) | (A /\ B)) = OOO & dom (((A /\ B) --> 1) | (A /\ B)) = A /\ B ) by FUNCOP_1:13; then B3: ((B --> 0) | (A /\ B)) +* (((A /\ B) --> 1) | (A /\ B)) = ((A /\ B) --> 1) | (A /\ B) by FUNCT_4:19; thus chi (A,B) = ((chi (A,B)) | (B \ A)) +* ((chi (A,B)) | (A /\ B)) by B4, FUNCT_4:70 .= (((B --> 0) +* ((A /\ B) --> 1)) | (B \ A)) +* ((chi (A,B)) | (A /\ B)) by Lm4 .= (((B /\ (B \ A)) --> 0) +* {}) +* (((A /\ B) --> 1) | (A /\ B)) by B1, Lm4, B2, B3 .= ((B \ A) --> 0) +* ((A /\ B) --> 1) ; ::_thesis: verum end; Lm29: for A, B being set holds chi (A,B) = ((B \ A) --> 0) \/ ((A /\ B) --> 1) proof let A, B be set ; ::_thesis: chi (A,B) = ((B \ A) --> 0) \/ ((A /\ B) --> 1) set f = (B \ A) --> 0; set g = (A /\ B) --> 1; (B \ A) /\ (A /\ B) = {} ; then B \ A misses A /\ B by XBOOLE_0:def_7; then (B \ A) --> 0 tolerates (A /\ B) --> 1 by FUNCOP_1:87; then ((B \ A) --> 0) +* ((A /\ B) --> 1) = ((B \ A) --> 0) \/ ((A /\ B) --> 1) by FUNCT_4:30; hence chi (A,B) = ((B \ A) --> 0) \/ ((A /\ B) --> 1) by Lm10; ::_thesis: verum end; theorem :: FOMODEL0:24 for A, B being set holds ( (chi (A,B)) " {0} = B \ A & (chi (A,B)) " {1} = A /\ B ) proof let A, B be set ; ::_thesis: ( (chi (A,B)) " {0} = B \ A & (chi (A,B)) " {1} = A /\ B ) set f = (B \ A) --> 0; set g = (A /\ B) --> 1; set IT = chi (A,B); B0: ( 0 in {0} & 1 in {1} & not 1 in {0} & not 0 in {1} ) by TARSKI:def_1; B2: ( ((B \ A) --> 0) " {1} = {} & ((A /\ B) --> 1) " {0} = {} ) by B0, FUNCOP_1:16; thus (chi (A,B)) " {0} = (((B \ A) --> 0) \/ ((A /\ B) --> 1)) " {0} by Lm29 .= (((B \ A) --> 0) " {0}) \/ (((A /\ B) --> 1) " {0}) by Th23 .= B \ A by B0, B2, FUNCOP_1:14 ; ::_thesis: (chi (A,B)) " {1} = A /\ B thus (chi (A,B)) " {1} = (((B \ A) --> 0) \/ ((A /\ B) --> 1)) " {1} by Lm29 .= (((B \ A) --> 0) " {1}) \/ (((A /\ B) --> 1) " {1}) by Th23 .= A /\ B by B0, B2, FUNCOP_1:14 ; ::_thesis: verum end; theorem :: FOMODEL0:25 for x being set for f being Function for y being non empty set holds ( y = f . x iff x in f " {y} ) proof let x be set ; ::_thesis: for f being Function for y being non empty set holds ( y = f . x iff x in f " {y} ) let f be Function; ::_thesis: for y being non empty set holds ( y = f . x iff x in f " {y} ) let y be non empty set ; ::_thesis: ( y = f . x iff x in f " {y} ) thus ( y = f . x implies x in f " {y} ) ::_thesis: ( x in f " {y} implies y = f . x ) proof assume y = f . x ; ::_thesis: x in f " {y} then ( x in dom f & f . x in {y} ) by FUNCT_1:def_2, TARSKI:def_1; hence x in f " {y} by FUNCT_1:def_7; ::_thesis: verum end; assume x in f " {y} ; ::_thesis: y = f . x then ( x in dom f & f . x in {y} ) by FUNCT_1:def_7; hence y = f . x by TARSKI:def_1; ::_thesis: verum end; theorem :: FOMODEL0:26 for Y being set for f being Function st f is Y -valued & f is FinSequence-like holds f is FinSequence of Y by Lm45; registration let Y be set ; let X be Subset of Y; cluster Relation-like X -valued -> Y -valued for set ; coherence for b1 being Relation st b1 is X -valued holds b1 is Y -valued proof let R be Relation; ::_thesis: ( R is X -valued implies R is Y -valued ) assume R is X -valued ; ::_thesis: R is Y -valued then ( rng R c= X & X c= Y ) by RELAT_1:def_19; then rng R c= Y by XBOOLE_1:1; hence R is Y -valued by RELAT_1:def_19; ::_thesis: verum end; end; Lm46: for Y being set for R being b1 -defined total Relation ex f being Function of Y,(rng R) st ( f c= R & dom f = Y ) proof let Y be set ; ::_thesis: for R being Y -defined total Relation ex f being Function of Y,(rng R) st ( f c= R & dom f = Y ) set X = Y; let R be Y -defined total Relation; ::_thesis: ex f being Function of Y,(rng R) st ( f c= R & dom f = Y ) B0: dom R = Y by PARTFUN1:def_2; defpred S1[ set , set ] means [\$1,\$2] in R; B1: for x being set st x in Y holds ex y being set st S1[x,y] by B0, XTUPLE_0:def_12; consider f being Function such that B2: ( dom f = Y & ( for x being set st x in Y holds S1[x,f . x] ) ) from CLASSES1:sch_1(B1); B3: f = { [x,(f . x)] where x is Element of dom f : x in dom f } by Th20; Z1: now__::_thesis:_for_z_being_set_st_z_in_f_holds_ z_in_R let z be set ; ::_thesis: ( z in f implies z in R ) assume z in f ; ::_thesis: z in R then consider x being Element of dom f such that C0: ( z = [x,(f . x)] & x in dom f ) by B3; thus z in R by C0, B2; ::_thesis: verum end; then f c= R by TARSKI:def_3; then rng f c= rng R by RELAT_1:11; then reconsider g = f as Function of Y,(rng R) by B2, FUNCT_2:67, RELSET_1:4; take g ; ::_thesis: ( g c= R & dom g = Y ) thus ( g c= R & dom g = Y ) by Z1, B2, TARSKI:def_3; ::_thesis: verum end; Lm47: for R being Relation for f being Function st dom f c= dom R & R c= f holds R = f proof let R be Relation; ::_thesis: for f being Function st dom f c= dom R & R c= f holds R = f let f be Function; ::_thesis: ( dom f c= dom R & R c= f implies R = f ) set X = dom f; assume B4: ( dom f c= dom R & R c= f ) ; ::_thesis: R = f then B2: ( dom f c= dom R & dom R c= dom f ) by RELAT_1:11; then B3: dom f = dom R by XBOOLE_0:def_10; reconsider RR = R as dom f -defined Relation by B2, RELAT_1:def_18; reconsider P = RR as dom f -defined total Relation by B3, PARTFUN1:def_2; consider g being Function of (dom f),(rng P) such that B0: ( g c= P & dom g = dom f ) by Lm46; f c= R by B0, B4, GRFUNC_1:3, XBOOLE_1:1; hence R = f by B4, XBOOLE_0:def_10; ::_thesis: verum end; Lm48: for Y being set for R, P being Relation for Q being b1 -defined Relation st Q is total & R is Y -defined & ((P * Q) * (Q ~)) * R is Function-like & rng P c= dom R holds ((P * Q) * (Q ~)) * R = P * R proof let Y be set ; ::_thesis: for R, P being Relation for Q being Y -defined Relation st Q is total & R is Y -defined & ((P * Q) * (Q ~)) * R is Function-like & rng P c= dom R holds ((P * Q) * (Q ~)) * R = P * R let R, P be Relation; ::_thesis: for Q being Y -defined Relation st Q is total & R is Y -defined & ((P * Q) * (Q ~)) * R is Function-like & rng P c= dom R holds ((P * Q) * (Q ~)) * R = P * R let Q be Y -defined Relation; ::_thesis: ( Q is total & R is Y -defined & ((P * Q) * (Q ~)) * R is Function-like & rng P c= dom R implies ((P * Q) * (Q ~)) * R = P * R ) assume Q is total ; ::_thesis: ( not R is Y -defined or not ((P * Q) * (Q ~)) * R is Function-like or not rng P c= dom R or ((P * Q) * (Q ~)) * R = P * R ) then reconsider QQ = Q as Y -defined total Relation ; set tQ = QQ ~ ; assume R is Y -defined ; ::_thesis: ( not ((P * Q) * (Q ~)) * R is Function-like or not rng P c= dom R or ((P * Q) * (Q ~)) * R = P * R ) then reconsider RR = R as Y -defined Relation ; assume ((P * Q) * (Q ~)) * R is Function-like ; ::_thesis: ( not rng P c= dom R or ((P * Q) * (Q ~)) * R = P * R ) then reconsider f = ((P * Q) * (QQ ~)) * R as Function ; B0: f = (P * Q) * ((QQ ~) * R) by RELAT_1:36 .= P * (Q * ((QQ ~) * R)) by RELAT_1:36 .= P * ((Q * (QQ ~)) * RR) by RELAT_1:36 ; (id Y) * RR c= (Q * (QQ ~)) * RR by Th21, RELAT_1:30; then Z1: RR | Y c= (Q * (QQ ~)) * RR by RELAT_1:65; assume rng P c= dom R ; ::_thesis: ((P * Q) * (Q ~)) * R = P * R then B1: dom (P * R) = dom P by RELAT_1:27; ( dom (P * (Q * (QQ ~))) c= dom P & dom (((P * Q) * (QQ ~)) * R) c= dom ((P * Q) * (QQ ~)) ) by RELAT_1:25; then ( dom ((P * Q) * (QQ ~)) c= dom P & dom f c= dom ((P * Q) * (QQ ~)) ) by RELAT_1:36; then dom f c= dom (P * R) by B1, XBOOLE_1:1; hence ((P * Q) * (Q ~)) * R = P * R by Z1, B0, Lm47, RELAT_1:29; ::_thesis: verum end; theorem :: FOMODEL0:27 for B, A being set for U1, U2 being non empty set for Q being quasi_total Relation of B,U1 for R being quasi_total Relation of B,U2 for P being Relation of A,B st ((P * Q) * (Q ~)) * R is Function-like holds ((P * Q) * (Q ~)) * R = P * R proof let B, A be set ; ::_thesis: for U1, U2 being non empty set for Q being quasi_total Relation of B,U1 for R being quasi_total Relation of B,U2 for P being Relation of A,B st ((P * Q) * (Q ~)) * R is Function-like holds ((P * Q) * (Q ~)) * R = P * R let U1, U2 be non empty set ; ::_thesis: for Q being quasi_total Relation of B,U1 for R being quasi_total Relation of B,U2 for P being Relation of A,B st ((P * Q) * (Q ~)) * R is Function-like holds ((P * Q) * (Q ~)) * R = P * R let Q be quasi_total Relation of B,U1; ::_thesis: for R being quasi_total Relation of B,U2 for P being Relation of A,B st ((P * Q) * (Q ~)) * R is Function-like holds ((P * Q) * (Q ~)) * R = P * R let R be quasi_total Relation of B,U2; ::_thesis: for P being Relation of A,B st ((P * Q) * (Q ~)) * R is Function-like holds ((P * Q) * (Q ~)) * R = P * R let P be Relation of A,B; ::_thesis: ( ((P * Q) * (Q ~)) * R is Function-like implies ((P * Q) * (Q ~)) * R = P * R ) reconsider QQ = Q as B -defined total Relation ; reconsider RR = R as B -defined total Relation ; Z0: ( dom R = B & rng P c= B ) by PARTFUN1:def_2; assume ((P * Q) * (Q ~)) * R is Function-like ; ::_thesis: ((P * Q) * (Q ~)) * R = P * R hence ((P * Q) * (Q ~)) * R = P * R by Z0, Lm48; ::_thesis: verum end; theorem :: FOMODEL0:28 for p, q being FinSequence st not p is empty holds (p ^ q) . 1 = p . 1 proof let p, q be FinSequence; ::_thesis: ( not p is empty implies (p ^ q) . 1 = p . 1 ) assume not p is empty ; ::_thesis: (p ^ q) . 1 = p . 1 then reconsider p = p as non empty FinSequence ; set n = len p; ( 1 <= 1 & 1 <= len p ) by NAT_1:14; then 1 in Seg (len p) ; then 1 in dom p by FINSEQ_1:def_3; hence (p ^ q) . 1 = p . 1 by FINSEQ_1:def_7; ::_thesis: verum end; registration let U be non empty set ; let p, q be U -valued FinSequence; clusterp ^ q -> U -valued for FinSequence; coherence for b1 being FinSequence st b1 = p ^ q holds b1 is U -valued proof reconsider pp = p, qq = q as FinSequence of U by Lm45; pp ^ qq is U -valued ; hence for b1 being FinSequence st b1 = p ^ q holds b1 is U -valued ; ::_thesis: verum end; end; definition let U be non empty set ; let X be set ; redefine attr X is U -prefix means :: FOMODEL0:def 20 for p1, q1, p2, q2 being U -valued FinSequence st p1 in X & p2 in X & p1 ^ q1 = p2 ^ q2 holds ( p1 = p2 & q1 = q2 ); compatibility ( X is U -prefix iff for p1, q1, p2, q2 being U -valued FinSequence st p1 in X & p2 in X & p1 ^ q1 = p2 ^ q2 holds ( p1 = p2 & q1 = q2 ) ) proof set f = U -concatenation ; set D = U * ; defpred S1[ set ] means \$1 is FinSequence of U; defpred S2[] means for p1, q1, p2, q2 being U -valued FinSequence st p1 in X & p2 in X & p1 ^ q1 = p2 ^ q2 holds ( p1 = p2 & q1 = q2 ); thus ( X is U -prefix implies S2[] ) ::_thesis: ( ( for p1, q1, p2, q2 being U -valued FinSequence st p1 in X & p2 in X & p1 ^ q1 = p2 ^ q2 holds ( p1 = p2 & q1 = q2 ) ) implies X is U -prefix ) proof assume X is U -prefix ; ::_thesis: S2[] then B2: X is U -concatenation -unambiguous by DefPrefix; let p1, q1, p2, q2 be U -valued FinSequence; ::_thesis: ( p1 in X & p2 in X & p1 ^ q1 = p2 ^ q2 implies ( p1 = p2 & q1 = q2 ) ) Z0: ( S1[p1] & S1[p2] & S1[q1] & S1[q2] ) by Lm45; assume Z: ( p1 in X & p2 in X ) ; ::_thesis: ( not p1 ^ q1 = p2 ^ q2 or ( p1 = p2 & q1 = q2 ) ) ( q1 in U * & q2 in U * & p1 in U * & p2 in U * ) by Z0, FINSEQ_1:def_11; then B1: ( p1 in X /\ (U *) & p2 in X /\ (U *) & q1 in U * & q2 in U * ) by Z, XBOOLE_0:def_4; assume p1 ^ q1 = p2 ^ q2 ; ::_thesis: ( p1 = p2 & q1 = q2 ) then (U -concatenation) . (p1,q1) = p2 ^ q2 by Th4 .= (U -concatenation) . (p2,q2) by Th4 ; hence ( p1 = p2 & q1 = q2 ) by B2, DefUnambiguous2, B1; ::_thesis: verum end; assume B3: S2[] ; ::_thesis: X is U -prefix now__::_thesis:_for_x1,_x2,_d1,_d2_being_set_st_x1_in_X_/\_(U_*)_&_x2_in_X_/\_(U_*)_&_d1_in_U_*_&_d2_in_U_*_&_(U_-concatenation)_._(x1,d1)_=_(U_-concatenation)_._(x2,d2)_holds_ (_x1_=_x2_&_d1_=_d2_) let x1, x2, d1, d2 be set ; ::_thesis: ( x1 in X /\ (U *) & x2 in X /\ (U *) & d1 in U * & d2 in U * & (U -concatenation) . (x1,d1) = (U -concatenation) . (x2,d2) implies ( x1 = x2 & d1 = d2 ) ) assume C0: ( x1 in X /\ (U *) & x2 in X /\ (U *) & d1 in U * & d2 in U * ) ; ::_thesis: ( (U -concatenation) . (x1,d1) = (U -concatenation) . (x2,d2) implies ( x1 = x2 & d1 = d2 ) ) then reconsider x11 = x1, x22 = x2, d11 = d1, d22 = d2 as Element of U * ; assume (U -concatenation) . (x1,d1) = (U -concatenation) . (x2,d2) ; ::_thesis: ( x1 = x2 & d1 = d2 ) then x11 ^ d11 = (U -concatenation) . (x22,d22) by Th4 .= x22 ^ d22 by Th4 ; hence ( x1 = x2 & d1 = d2 ) by B3, C0; ::_thesis: verum end; then X is U -concatenation -unambiguous by DefUnambiguous2; hence X is U -prefix by DefPrefix; ::_thesis: verum end; end; :: deftheorem defines -prefix FOMODEL0:def_20_:_ for U being non empty set for X being set holds ( X is U -prefix iff for p1, q1, p2, q2 being b1 -valued FinSequence st p1 in X & p2 in X & p1 ^ q1 = p2 ^ q2 holds ( p1 = p2 & q1 = q2 ) ); registration let X be set ; cluster -> X -valued for Element of X * ; coherence for b1 being Element of X * holds b1 is X -valued ; end; registration let U be non empty set ; let m be Nat; let X be U -prefix set ; cluster(U -multiCat) .: (m -tuples_on X) -> U -prefix for set ; coherence for b1 being set st b1 = (U -multiCat) .: (m -tuples_on X) holds b1 is U -prefix by Lm25; end; theorem Th29: :: FOMODEL0:29 for Y, X being set holds ( X \+\ Y = {} iff X = Y ) proof let Y, X be set ; ::_thesis: ( X \+\ Y = {} iff X = Y ) set Z = X \+\ Y; set Z1 = X \ Y; set Z2 = Y \ X; thus ( X \+\ Y = {} implies X = Y ) ::_thesis: ( X = Y implies X \+\ Y = {} ) proof assume X \+\ Y = {} ; ::_thesis: X = Y then ( X \ Y = {} & Y \ X = {} ) ; then ( X c= Y & Y c= X ) by XBOOLE_1:37; hence X = Y by XBOOLE_0:def_10; ::_thesis: verum end; assume X = Y ; ::_thesis: X \+\ Y = {} hence X \+\ Y = {} ; ::_thesis: verum end; registration let x be set ; cluster(id {x}) \+\ {[x,x]} -> empty for set ; coherence for b1 being set st b1 = (id {x}) \+\ {[x,x]} holds b1 is empty proof id {x} = {[x,x]} by SYSREL:13; hence for b1 being set st b1 = (id {x}) \+\ {[x,x]} holds b1 is empty ; ::_thesis: verum end; end; registration let x, y be set ; cluster(x .--> y) \+\ {[x,y]} -> empty for set ; coherence for b1 being set st b1 = (x .--> y) \+\ {[x,y]} holds b1 is empty proof x .--> y = {[x,y]} by ZFMISC_1:29; hence for b1 being set st b1 = (x .--> y) \+\ {[x,y]} holds b1 is empty ; ::_thesis: verum end; end; registration let x be set ; cluster(id {x}) \+\ (x .--> x) -> empty for set ; coherence for b1 being set st b1 = (id {x}) \+\ (x .--> x) holds b1 is empty proof ( (id {x}) \+\ {[x,x]} = {} & (x .--> x) \+\ {[x,x]} = {} ) ; hence for b1 being set st b1 = (id {x}) \+\ (x .--> x) holds b1 is empty by Th29; ::_thesis: verum end; end; theorem :: FOMODEL0:30 for D being non empty set for x being set holds ( x in (D *) \ {{}} iff ( x is b1 -valued FinSequence & not x is empty ) ) proof let D be non empty set ; ::_thesis: for x being set holds ( x in (D *) \ {{}} iff ( x is D -valued FinSequence & not x is empty ) ) let x be set ; ::_thesis: ( x in (D *) \ {{}} iff ( x is D -valued FinSequence & not x is empty ) ) ( ( x is D -valued FinSequence & not x is empty ) iff x is non empty FinSequence of D ) by Lm45; hence ( x in (D *) \ {{}} iff ( x is D -valued FinSequence & not x is empty ) ) by Lm2; ::_thesis: verum end; theorem Th31: :: FOMODEL0:31 for D being non empty set for d being Element of D for f being BinOp of D holds ( (MultPlace f) . <*d*> = d & ( for x being b1 -valued FinSequence st not x is empty holds (MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d) ) ) proof let D be non empty set ; ::_thesis: for d being Element of D for f being BinOp of D holds ( (MultPlace f) . <*d*> = d & ( for x being D -valued FinSequence st not x is empty holds (MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d) ) ) let d be Element of D; ::_thesis: for f being BinOp of D holds ( (MultPlace f) . <*d*> = d & ( for x being D -valued FinSequence st not x is empty holds (MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d) ) ) let f be BinOp of D; ::_thesis: ( (MultPlace f) . <*d*> = d & ( for x being D -valued FinSequence st not x is empty holds (MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d) ) ) set F = MultPlace f; thus (MultPlace f) . <*d*> = d by LmMultPlace; ::_thesis: for x being D -valued FinSequence st not x is empty holds (MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d) let x be D -valued FinSequence; ::_thesis: ( not x is empty implies (MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d) ) assume not x is empty ; ::_thesis: (MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d) then reconsider xx = x as non empty FinSequence of D by Lm45; (MultPlace f) . (xx ^ <*d*>) = f . (((MultPlace f) . xx),d) by LmMultPlace; hence (MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d) ; ::_thesis: verum end; registration let p be FinSequence; let x, y be set ; clusterp +~ (x,y) -> FinSequence-like ; coherence p +~ (x,y) is FinSequence-like proof set IT = p +~ (x,y); dom (p +~ (x,y)) = dom p by FUNCT_4:99 .= Seg (len p) by FINSEQ_1:def_3 ; hence p +~ (x,y) is FinSequence-like by FINSEQ_1:def_2; ::_thesis: verum end; end; definition let x, y be set ; let p be FinSequence; func(x,y) -SymbolSubstIn p -> FinSequence equals :: FOMODEL0:def 21 p +~ (x,y); coherence p +~ (x,y) is FinSequence ; end; :: deftheorem defines -SymbolSubstIn FOMODEL0:def_21_:_ for x, y being set for p being FinSequence holds (x,y) -SymbolSubstIn p = p +~ (x,y); registration let x, y be set ; let m be Nat; let p be m -element FinSequence; cluster(x,y) -SymbolSubstIn p -> m -element for FinSequence; coherence for b1 being FinSequence st b1 = (x,y) -SymbolSubstIn p holds b1 is m -element proof set IT = (x,y) -SymbolSubstIn p; reconsider mm = m as Element of NAT by ORDINAL1:def_12; dom ((x,y) -SymbolSubstIn p) = dom p by FUNCT_4:99 .= Seg (len p) by FINSEQ_1:def_3 .= Seg mm by CARD_1:def_7 ; then len ((x,y) -SymbolSubstIn p) = mm by FINSEQ_1:def_3; hence for b1 being FinSequence st b1 = (x,y) -SymbolSubstIn p holds b1 is m -element by CARD_1:def_7; ::_thesis: verum end; end; registration let x be set ; let U be non empty set ; let u be Element of U; let p be U -valued FinSequence; cluster(x,u) -SymbolSubstIn p -> U -valued for FinSequence; coherence for b1 being FinSequence st b1 = (x,u) -SymbolSubstIn p holds b1 is U -valued ; end; definition let X, x, y be set ; let p be X -valued FinSequence; :: original: -SymbolSubstIn redefine func(x,y) -SymbolSubstIn p -> FinSequence equals :: FOMODEL0:def 22 ((id X) +* (x,y)) * p; compatibility for b1 being FinSequence holds ( b1 = (x,y) -SymbolSubstIn p iff b1 = ((id X) +* (x,y)) * p ) proof rng p c= X ; hence for b1 being FinSequence holds ( b1 = (x,y) -SymbolSubstIn p iff b1 = ((id X) +* (x,y)) * p ) by FUNCT_7:116; ::_thesis: verum end; end; :: deftheorem defines -SymbolSubstIn FOMODEL0:def_22_:_ for X, x, y being set for p being b1 -valued FinSequence holds (x,y) -SymbolSubstIn p = ((id X) +* (x,y)) * p; definition let U be non empty set ; let x be set ; let u be Element of U; let q be U -valued FinSequence; :: original: -SymbolSubstIn redefine func(x,u) -SymbolSubstIn q -> FinSequence of U; coherence (x,u) -SymbolSubstIn q is FinSequence of U by Lm45; end; Lm53: for x2 being set for U being non empty set for u, u1 being Element of U holds ( ( u = u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*x2*> ) & ( u <> u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*u*> ) ) proof let x2 be set ; ::_thesis: for U being non empty set for u, u1 being Element of U holds ( ( u = u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*x2*> ) & ( u <> u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*u*> ) ) let U be non empty set ; ::_thesis: for u, u1 being Element of U holds ( ( u = u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*x2*> ) & ( u <> u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*u*> ) ) let u, u1 be Element of U; ::_thesis: ( ( u = u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*x2*> ) & ( u <> u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*u*> ) ) set X = U; set s = u; set s1 = u1; set s2 = x2; set w = <*u*>; set IT = (u1,x2) -SymbolSubstIn <*u*>; set f1 = 1 .--> u1; set f2 = 1 .--> x2; set f = 1 .--> u; set subst = u1 .--> x2; set I = id U; set w1 = <*u1*>; set w2 = <*x2*>; Z0: ( <*u*> \+\ (1 .--> u) = {} & <*x2*> \+\ (1 .--> x2) = {} & <*u1*> \+\ (1 .--> u1) = {} ) ; then B0: ( <*u*> = 1 .--> u & <*x2*> = 1 .--> x2 & <*u1*> = 1 .--> u1 ) by Th29; B2: ( dom (u1 .--> x2) = {u1} & dom (1 .--> x2) = {1} & dom (1 .--> u1) = {1} & dom (1 .--> u) = {1} & rng (1 .--> u) = {u} ) by FUNCOP_1:8, FUNCOP_1:13; u1 in {u1} by TARSKI:def_1; then B5: (u1 .--> x2) . u1 = x2 by FUNCOP_1:7; B3: (u1,x2) -SymbolSubstIn <*u*> = <*u*> +* ((u1 .--> x2) * (1 .--> u)) by Z0, Th29; thus ( u = u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*x2*> ) ::_thesis: ( u <> u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*u*> ) proof assume C0: u = u1 ; ::_thesis: (u1,x2) -SymbolSubstIn <*u*> = <*x2*> then u in dom (u1 .--> x2) by B2, TARSKI:def_1; then (u1,x2) -SymbolSubstIn <*u*> = (1 .--> u) +* (1 .--> x2) by C0, B0, B5, FUNCOP_1:17 .= <*x2*> by B0, B2, FUNCT_4:19 ; hence (u1,x2) -SymbolSubstIn <*u*> = <*x2*> ; ::_thesis: verum end; assume u <> u1 ; ::_thesis: (u1,x2) -SymbolSubstIn <*u*> = <*u*> then (u1 .--> x2) * (1 .--> u) = {} by B2, RELAT_1:44, ZFMISC_1:11; then (u1,x2) -SymbolSubstIn <*u*> = <*u*> +* {} by B3; hence (u1,x2) -SymbolSubstIn <*u*> = <*u*> ; ::_thesis: verum end; Lm50: for x being set for U being non empty set for u being Element of U for q1, q2 being b2 -valued FinSequence holds (x,u) -SymbolSubstIn (q1 ^ q2) = ((x,u) -SymbolSubstIn q1) ^ ((x,u) -SymbolSubstIn q2) proof let x be set ; ::_thesis: for U being non empty set for u being Element of U for q1, q2 being b1 -valued FinSequence holds (x,u) -SymbolSubstIn (q1 ^ q2) = ((x,u) -SymbolSubstIn q1) ^ ((x,u) -SymbolSubstIn q2) let U be non empty set ; ::_thesis: for u being Element of U for q1, q2 being U -valued FinSequence holds (x,u) -SymbolSubstIn (q1 ^ q2) = ((x,u) -SymbolSubstIn q1) ^ ((x,u) -SymbolSubstIn q2) let u be Element of U; ::_thesis: for q1, q2 being U -valued FinSequence holds (x,u) -SymbolSubstIn (q1 ^ q2) = ((x,u) -SymbolSubstIn q1) ^ ((x,u) -SymbolSubstIn q2) let q1, q2 be U -valued FinSequence; ::_thesis: (x,u) -SymbolSubstIn (q1 ^ q2) = ((x,u) -SymbolSubstIn q1) ^ ((x,u) -SymbolSubstIn q2) set s1 = x; set s2 = u; set w1 = q1; set w2 = q2; set w = q1 ^ q2; set IT1 = (x,u) -SymbolSubstIn q1; set IT2 = (x,u) -SymbolSubstIn q2; set IT = (x,u) -SymbolSubstIn (q1 ^ q2); set f = x .--> u; set I = id U; reconsider g = (id U) +* (x,u) as Function of U,U ; reconsider w11 = q1, w22 = q2, ww = q1 ^ q2 as FinSequence of U by Lm45; thus (x,u) -SymbolSubstIn (q1 ^ q2) = (g * w11) ^ (g * w22) by FINSEQOP:9 .= ((x,u) -SymbolSubstIn q1) ^ ((x,u) -SymbolSubstIn q2) ; ::_thesis: verum end; definition let U be non empty set ; let x be set ; let u be Element of U; set D = U * ; deffunc H1( Element of U * ) -> FinSequence of U = (x,u) -SymbolSubstIn \$1; funcx SubstWith u -> Function of (U *),(U *) means :DefSubst: :: FOMODEL0:def 23 for q being U -valued FinSequence holds it . q = (x,u) -SymbolSubstIn q; existence ex b1 being Function of (U *),(U *) st for q being U -valued FinSequence holds b1 . q = (x,u) -SymbolSubstIn q proof A: for x being Element of U * holds H1(x) is Element of U * by FINSEQ_1:def_11; consider f being Function of (U *),(U *) such that B0: for x being Element of U * holds f . x = H1(x) from FUNCT_2:sch_9(A); take f ; ::_thesis: for q being U -valued FinSequence holds f . q = (x,u) -SymbolSubstIn q now__::_thesis:_for_q_being_U_-valued_FinSequence_holds_f_._q_=_(x,u)_-SymbolSubstIn_q let q be U -valued FinSequence; ::_thesis: f . q = (x,u) -SymbolSubstIn q reconsider qq = q as FinSequence of U by Lm45; reconsider qqq = qq as Element of U * by FINSEQ_1:def_11; f . qqq = H1(qqq) by B0; hence f . q = (x,u) -SymbolSubstIn q ; ::_thesis: verum end; hence for q being U -valued FinSequence holds f . q = (x,u) -SymbolSubstIn q ; ::_thesis: verum end; uniqueness for b1, b2 being Function of (U *),(U *) st ( for q being U -valued FinSequence holds b1 . q = (x,u) -SymbolSubstIn q ) & ( for q being U -valued FinSequence holds b2 . q = (x,u) -SymbolSubstIn q ) holds b1 = b2 proof let IT1, IT2 be Function of (U *),(U *); ::_thesis: ( ( for q being U -valued FinSequence holds IT1 . q = (x,u) -SymbolSubstIn q ) & ( for q being U -valued FinSequence holds IT2 . q = (x,u) -SymbolSubstIn q ) implies IT1 = IT2 ) assume B1: for q being U -valued FinSequence holds IT1 . q = (x,u) -SymbolSubstIn q ; ::_thesis: ( ex q being U -valued FinSequence st not IT2 . q = (x,u) -SymbolSubstIn q or IT1 = IT2 ) assume B2: for q being U -valued FinSequence holds IT2 . q = (x,u) -SymbolSubstIn q ; ::_thesis: IT1 = IT2 now__::_thesis:_for_w_being_Element_of_U_*_holds_IT1_._w_=_IT2_._w let w be Element of U * ; ::_thesis: IT1 . w = IT2 . w thus IT1 . w = H1(w) by B1 .= IT2 . w by B2 ; ::_thesis: verum end; hence IT1 = IT2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem DefSubst defines SubstWith FOMODEL0:def_23_:_ for U being non empty set for x being set for u being Element of U for b4 being Function of (U *),(U *) holds ( b4 = x SubstWith u iff for q being b1 -valued FinSequence holds b4 . q = (x,u) -SymbolSubstIn q ); Lm54: for U being non empty set for u, u1, u2 being Element of U holds ( ( u = u1 implies (u1 SubstWith u2) . <*u*> = <*u2*> ) & ( u <> u1 implies (u1 SubstWith u2) . <*u*> = <*u*> ) ) proof let U be non empty set ; ::_thesis: for u, u1, u2 being Element of U holds ( ( u = u1 implies (u1 SubstWith u2) . <*u*> = <*u2*> ) & ( u <> u1 implies (u1 SubstWith u2) . <*u*> = <*u*> ) ) let u, u1, u2 be Element of U; ::_thesis: ( ( u = u1 implies (u1 SubstWith u2) . <*u*> = <*u2*> ) & ( u <> u1 implies (u1 SubstWith u2) . <*u*> = <*u*> ) ) set e = u1 SubstWith u2; set es = (u1,u2) -SymbolSubstIn <*u*>; (u1,u2) -SymbolSubstIn <*u*> = (u1 SubstWith u2) . <*u*> by DefSubst; hence ( ( u = u1 implies (u1 SubstWith u2) . <*u*> = <*u2*> ) & ( u <> u1 implies (u1 SubstWith u2) . <*u*> = <*u*> ) ) by Lm53; ::_thesis: verum end; registration let U be non empty set ; let x be set ; let u be Element of U; clusterx SubstWith u -> FinSequence-yielding for Function; coherence for b1 being Function st b1 = x SubstWith u holds b1 is FinSequence-yielding proof set e = x SubstWith u; now__::_thesis:_for_y_being_set_st_y_in_dom_(x_SubstWith_u)_holds_ (x_SubstWith_u)_._y_is_FinSequence let y be set ; ::_thesis: ( y in dom (x SubstWith u) implies (x SubstWith u) . y is FinSequence ) assume y in dom (x SubstWith u) ; ::_thesis: (x SubstWith u) . y is FinSequence then reconsider yy = y as Element of U * ; thus (x SubstWith u) . y is FinSequence ; ::_thesis: verum end; hence for b1 being Function st b1 = x SubstWith u holds b1 is FinSequence-yielding by PRE_POLY:def_3; ::_thesis: verum end; end; registration let F be FinSequence-yielding Function; let x be set ; clusterF . x -> FinSequence-like ; coherence F . x is FinSequence-like proof percases ( x in dom F or not x in dom F ) ; suppose x in dom F ; ::_thesis: F . x is FinSequence-like hence F . x is FinSequence-like by PRE_POLY:def_3; ::_thesis: verum end; suppose not x in dom F ; ::_thesis: F . x is FinSequence-like hence F . x is FinSequence-like by FUNCT_1:def_2; ::_thesis: verum end; end; end; end; Lm55: for x being set for U being non empty set for u being Element of U for q1, q2 being b2 -valued FinSequence holds (x SubstWith u) . (q1 ^ q2) = ((x SubstWith u) . q1) ^ ((x SubstWith u) . q2) proof let x be set ; ::_thesis: for U being non empty set for u being Element of U for q1, q2 being b1 -valued FinSequence holds (x SubstWith u) . (q1 ^ q2) = ((x SubstWith u) . q1) ^ ((x SubstWith u) . q2) let U be non empty set ; ::_thesis: for u being Element of U for q1, q2 being U -valued FinSequence holds (x SubstWith u) . (q1 ^ q2) = ((x SubstWith u) . q1) ^ ((x SubstWith u) . q2) let u be Element of U; ::_thesis: for q1, q2 being U -valued FinSequence holds (x SubstWith u) . (q1 ^ q2) = ((x SubstWith u) . q1) ^ ((x SubstWith u) . q2) let q1, q2 be U -valued FinSequence; ::_thesis: (x SubstWith u) . (q1 ^ q2) = ((x SubstWith u) . q1) ^ ((x SubstWith u) . q2) set e = x SubstWith u; set w1 = q1; set w2 = q2; set w = q1 ^ q2; set W1 = (x,u) -SymbolSubstIn q1; set W2 = (x,u) -SymbolSubstIn q2; set W = (x,u) -SymbolSubstIn (q1 ^ q2); ( (x SubstWith u) . q1 = (x,u) -SymbolSubstIn q1 & (x SubstWith u) . q2 = (x,u) -SymbolSubstIn q2 & (x SubstWith u) . (q1 ^ q2) = (x,u) -SymbolSubstIn (q1 ^ q2) ) by DefSubst; hence (x SubstWith u) . (q1 ^ q2) = ((x SubstWith u) . q1) ^ ((x SubstWith u) . q2) by Lm50; ::_thesis: verum end; registration let U be non empty set ; let x be set ; let u be Element of U; let m be Nat; let p be U -valued m -element FinSequence; cluster(x SubstWith u) . p -> m -element for FinSequence; coherence for b1 being FinSequence st b1 = (x SubstWith u) . p holds b1 is m -element proof (x SubstWith u) . p = (x,u) -SymbolSubstIn p by DefSubst; hence for b1 being FinSequence st b1 = (x SubstWith u) . p holds b1 is m -element ; ::_thesis: verum end; end; registration let U be non empty set ; let x be set ; let u be Element of U; let e be empty set ; cluster(x SubstWith u) . e -> empty for set ; coherence for b1 being set st b1 = (x SubstWith u) . e holds b1 is empty proof rng e = U /\ {} ; then reconsider ee = e as U -valued 0 -element FinSequence by RELAT_1:def_19; for X being set holds (X SubstWith u) . ee is 0 -element ; hence for b1 being set st b1 = (x SubstWith u) . e holds b1 is empty ; ::_thesis: verum end; end; registration let U be non empty set ; clusterU -multiCat -> FinSequence-yielding for Function; coherence for b1 being Function st b1 = U -multiCat holds b1 is FinSequence-yielding proof set f = U -multiCat ; set C = U * ; set D = (U *) * ; now__::_thesis:_for_x_being_set_st_x_in_dom_(U_-multiCat)_holds_ (U_-multiCat)_._x_is_FinSequence let x be set ; ::_thesis: ( x in dom (U -multiCat) implies (U -multiCat) . x is FinSequence ) assume x in dom (U -multiCat) ; ::_thesis: (U -multiCat) . x is FinSequence then reconsider xx = x as Element of dom (U -multiCat) ; thus (U -multiCat) . x is FinSequence ; ::_thesis: verum end; hence for b1 being Function st b1 = U -multiCat holds b1 is FinSequence-yielding by PRE_POLY:def_3; ::_thesis: verum end; end; registration let U be non empty set ; cluster Relation-like NAT -defined U -valued Function-like non empty finite FinSequence-like FinSubsequence-like countable finite-support for set ; existence not for b1 being U -valued FinSequence holds b1 is empty proof take <* the Element of U*> ; ::_thesis: not <* the Element of U*> is empty thus not <* the Element of U*> is empty ; ::_thesis: verum end; end; registration let U be non empty set ; let m1 be non zero Nat; let n be Nat; let p be U -valued m1 + n -element FinSequence; cluster{(p . m1)} \ U -> empty for set ; coherence for b1 being set st b1 = {(p . m1)} \ U holds b1 is empty proof consider m being Nat such that B0: m1 = m + 1 by NAT_1:6; set IT = {(p . m1)} \ U; set M = m1 + n; p in (m1 + n) -tuples_on U by Th16; then p is Element of Funcs ((Seg (m1 + n)),U) by Lm21; then reconsider f = p as Function of (Seg (m1 + n)),U ; ( 1 <= m + 1 & m + 1 <= (m + 1) + n ) by NAT_1:11; then reconsider ms = m1 as Element of Seg (m1 + n) by B0, FINSEQ_1:1; f . ms in U ; hence for b1 being set st b1 = {(p . m1)} \ U holds b1 is empty by ZFMISC_1:60; ::_thesis: verum end; end; registration let U be non empty set ; let m, n be Nat; let p be (m + 1) + n -element Element of U * ; cluster{(p . (m + 1))} \ U -> empty for set ; coherence for b1 being set st b1 = {(p . (m + 1))} \ U holds b1 is empty ; end; registration let x be set ; cluster<*x*> \+\ {[1,x]} -> empty for set ; coherence for b1 being set st b1 = <*x*> \+\ {[1,x]} holds b1 is empty ; end; registration let m be Nat; let p be m + 1 -element FinSequence; cluster((p | (Seg m)) ^ <*(p . (m + 1))*>) \+\ p -> empty for set ; coherence for b1 being set st b1 = ((p | (Seg m)) ^ <*(p . (m + 1))*>) \+\ p holds b1 is empty proof set q = p | (Seg m); len p = m + 1 by CARD_1:def_7; then p = (p | (Seg m)) ^ <*(p . (m + 1))*> by FINSEQ_3:55; hence for b1 being set st b1 = ((p | (Seg m)) ^ <*(p . (m + 1))*>) \+\ p holds b1 is empty ; ::_thesis: verum end; end; registration let m, n be Nat; let p be m + n -element FinSequence; clusterp | (Seg m) -> m -element for FinSequence; coherence for b1 being FinSequence st b1 = p | (Seg m) holds b1 is m -element proof reconsider mm = m as Element of NAT by ORDINAL1:def_12; set q = p | (Seg m); set N = m + n; ( m + 0 <= m + n & len p = m + n ) by CARD_1:def_7, XREAL_1:7; then ( Seg m c= Seg (m + n) & dom p = Seg (m + n) ) by FINSEQ_1:5, FINSEQ_1:def_3; then reconsider M = Seg m as Subset of (dom p) ; dom (p | (Seg m)) = M null (dom p) by RELAT_1:61 .= Seg mm ; then len (p | (Seg m)) = mm by FINSEQ_1:def_3; hence for b1 being FinSequence st b1 = p | (Seg m) holds b1 is m -element by CARD_1:def_7; ::_thesis: verum end; end; Lm51: for R being Relation holds ( R is {{}} -valued iff R is empty-yielding ) proof let R be Relation; ::_thesis: ( R is {{}} -valued iff R is empty-yielding ) ( R is {{}} -valued iff rng R c= {{}} ) by RELAT_1:def_19; hence ( R is {{}} -valued iff R is empty-yielding ) by RELAT_1:def_15; ::_thesis: verum end; registration cluster Relation-like {{}} -valued -> empty-yielding for set ; coherence for b1 being Relation st b1 is {{}} -valued holds b1 is empty-yielding by Lm51; cluster Relation-like empty-yielding -> {{}} -valued for set ; coherence for b1 being Relation st b1 is empty-yielding holds b1 is {{}} -valued by Lm51; end; theorem Th32: :: FOMODEL0:32 for x being set for U being non empty set holds (U -multiCat) . x = (MultPlace (U -concatenation)) . x proof let x be set ; ::_thesis: for U being non empty set holds (U -multiCat) . x = (MultPlace (U -concatenation)) . x let U be non empty set ; ::_thesis: (U -multiCat) . x = (MultPlace (U -concatenation)) . x set D = U * ; set f = U -concatenation ; set F = MultPlace (U -concatenation); set G = U -multiCat ; reconsider g = {} .--> {} as {{}} -valued Function ; ( dom (U -concatenation) = [:(U *),(U *):] & dom (MultPlace (U -concatenation)) = ((U *) *) \ {{}} & dom (U -multiCat) = (U *) * ) by FUNCT_2:def_1; then reconsider dF = dom (MultPlace (U -concatenation)) as Subset of (dom (U -multiCat)) ; percases ( x in dom (MultPlace (U -concatenation)) or not x in dom (MultPlace (U -concatenation)) ) ; suppose x in dom (MultPlace (U -concatenation)) ; ::_thesis: (U -multiCat) . x = (MultPlace (U -concatenation)) . x hence (U -multiCat) . x = (MultPlace (U -concatenation)) . x by FUNCT_4:13; ::_thesis: verum end; supposeC0: not x in dom (MultPlace (U -concatenation)) ; ::_thesis: (U -multiCat) . x = (MultPlace (U -concatenation)) . x hence (U -multiCat) . x = g . x by FUNCT_4:11 .= (MultPlace (U -concatenation)) . x by C0, FUNCT_1:def_2 ; ::_thesis: verum end; end; end; theorem Th33: :: FOMODEL0:33 for U being non empty set for p being FinSequence for q being b1 -valued FinSequence st p is U * -valued holds (U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q proof let U be non empty set ; ::_thesis: for p being FinSequence for q being U -valued FinSequence st p is U * -valued holds (U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q let p be FinSequence; ::_thesis: for q being U -valued FinSequence st p is U * -valued holds (U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q let q be U -valued FinSequence; ::_thesis: ( p is U * -valued implies (U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q ) set C = U -multiCat ; set g = U -concatenation ; set G = MultPlace (U -concatenation); q is FinSequence of U by Lm45; then reconsider qq = q as Element of U * by FINSEQ_1:def_11; percases ( p is empty or not p is empty ) ; suppose p is empty ; ::_thesis: ( p is U * -valued implies (U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q ) then reconsider e = p as empty set ; C0: ( ((U -multiCat) . e) ^ q = q & (U -multiCat) . (e ^ <*q*>) = (U -multiCat) . <*q*> ) ; (U -multiCat) . (e ^ <*q*>) = (MultPlace (U -concatenation)) . <*qq*> by Th32 .= qq by Th31 ; hence ( p is U * -valued implies (U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q ) by C0; ::_thesis: verum end; supposeC0: not p is empty ; ::_thesis: ( p is U * -valued implies (U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q ) assume p is U * -valued ; ::_thesis: (U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q then reconsider pp = p as U * -valued non empty FinSequence by C0; pp is non empty FinSequence of U * by Lm45; then reconsider ppp = pp as non empty Element of (U *) * by FINSEQ_1:def_11; (U -multiCat) . (pp ^ <*q*>) = (MultPlace (U -concatenation)) . (pp ^ <*qq*>) by Th32 .= (U -concatenation) . (((MultPlace (U -concatenation)) . pp),qq) by Th31 .= (U -concatenation) . (((U -multiCat) . ppp),q) by Th32 .= ((U -multiCat) . p) ^ q by Th4 ; hence (U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q ; ::_thesis: verum end; end; end; Lm52: for x being set for U being non empty set for u being Element of U for p being FinSequence st p is U * -valued holds (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p) proof let x be set ; ::_thesis: for U being non empty set for u being Element of U for p being FinSequence st p is U * -valued holds (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p) let U be non empty set ; ::_thesis: for u being Element of U for p being FinSequence st p is U * -valued holds (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p) let u be Element of U; ::_thesis: for p being FinSequence st p is U * -valued holds (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p) let p be FinSequence; ::_thesis: ( p is U * -valued implies (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p) ) set S = U; set C = U -multiCat ; set SS = U; set strings = U * ; set e = x SubstWith u; set m = len p; set F = U -firstChar ; set FF = (U *) -firstChar ; set g = U -concatenation ; set G = MultPlace (U -concatenation); defpred S1[ Nat] means for p being U * -valued \$1 -element FinSequence holds (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p); B10: S1[ 0 ] ; B11: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) set n1 = n + 1; assume C0: S1[n] ; ::_thesis: S1[n + 1] let p be U * -valued n + 1 -element FinSequence; ::_thesis: (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p) reconsider q = p | (Seg n) as U * -valued n -element FinSequence ; q is n -element FinSequence of U * by Lm45; then reconsider qq = q as n -element Element of (U *) * by FINSEQ_1:def_11; p is (n + 1) + 0 -element ; then {(p . (n + 1))} \ (U *) = {} ; then reconsider z = p . (n + 1) as Element of U * by ZFMISC_1:60; reconsider f = (x SubstWith u) . z as Element of U * ; (q ^ <*z*>) \+\ p = {} ; then C1: q ^ <*z*> = p by Th29; (U -multiCat) . ((x SubstWith u) * p) = (U -multiCat) . (((x SubstWith u) * qq) ^ <*f*>) by C1, FINSEQOP:8 .= ((U -multiCat) . ((x SubstWith u) * qq)) ^ f by Th33 .= ((x SubstWith u) . ((U -multiCat) . qq)) ^ f by C0 .= (x SubstWith u) . (((U -multiCat) . qq) ^ z) by Lm55 .= (x SubstWith u) . ((U -multiCat) . p) by Th33, C1 ; hence (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p) ; ::_thesis: verum end; B1: for n being Nat holds S1[n] from NAT_1:sch_2(B10, B11); assume p is U * -valued ; ::_thesis: (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p) then reconsider pp = p as U * -valued len p -element FinSequence by CARD_1:def_7; (x SubstWith u) . ((U -multiCat) . pp) = (U -multiCat) . ((x SubstWith u) * pp) by B1; hence (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p) ; ::_thesis: verum end; registration let Y be set ; let X be Subset of Y; let R be Y -defined total Relation; clusterR | X -> X -defined total for X -defined Relation; coherence for b1 being X -defined Relation st b1 = R | X holds b1 is total proof set IT = R | X; dom R = Y by PARTFUN1:def_2; then B0: dom (R | X) = X null Y by RELAT_1:61; reconsider ITT = R | X as X -defined Relation ; thus for b1 being X -defined Relation st b1 = R | X holds b1 is total by B0, PARTFUN1:def_2; ::_thesis: verum end; end; theorem :: FOMODEL0:34 for x2 being set for U being non empty set for u, u1 being Element of U holds ( ( u = u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*x2*> ) & ( u <> u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*u*> ) ) by Lm53; theorem :: FOMODEL0:35 for U being non empty set for u, u1, u2 being Element of U holds ( ( u = u1 implies (u1 SubstWith u2) . <*u*> = <*u2*> ) & ( u <> u1 implies (u1 SubstWith u2) . <*u*> = <*u*> ) ) by Lm54; theorem :: FOMODEL0:36 for x being set for U being non empty set for u being Element of U for q1, q2 being b2 -valued FinSequence holds (x SubstWith u) . (q1 ^ q2) = ((x SubstWith u) . q1) ^ ((x SubstWith u) . q2) by Lm55; theorem :: FOMODEL0:37 for x being set for U being non empty set for u being Element of U for p being FinSequence st p is U * -valued holds (x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p) by Lm52; theorem :: FOMODEL0:38 for U being non empty set holds (U -concatenation) .: (id (1 -tuples_on U)) = { <*u,u*> where u is Element of U : verum } proof let U be non empty set ; ::_thesis: (U -concatenation) .: (id (1 -tuples_on U)) = { <*u,u*> where u is Element of U : verum } set f = U -concatenation ; set U1 = 1 -tuples_on U; set D = id (1 -tuples_on U); set U2 = 2 -tuples_on U; set A = (U -concatenation) .: (id (1 -tuples_on U)); set B = { <*u,u*> where u is Element of U : verum } ; ( id (1 -tuples_on U) c= [:(1 -tuples_on U),(1 -tuples_on U):] & 1 -tuples_on U c= U * ) by FINSEQ_2:142; then [:(1 -tuples_on U),(1 -tuples_on U):] c= [:(U *),(U *):] by ZFMISC_1:96; then reconsider DD = id (1 -tuples_on U) as Subset of [:(U *),(U *):] by XBOOLE_1:1; B2: 1 -tuples_on U = { <*u*> where u is Element of U : verum } by FINSEQ_2:96; B0: ( dom (id (1 -tuples_on U)) = 1 -tuples_on U & dom (U -concatenation) = [:(U *),(U *):] ) by FUNCT_2:def_1; then B1: id (1 -tuples_on U) = { [x,((id (1 -tuples_on U)) . x)] where x is Element of 1 -tuples_on U : x in 1 -tuples_on U } by Th20; now__::_thesis:_for_y_being_set_st_y_in_(U_-concatenation)_.:_(id_(1_-tuples_on_U))_holds_ y_in__{__<*u,u*>_where_u_is_Element_of_U_:_verum__}_ let y be set ; ::_thesis: ( y in (U -concatenation) .: (id (1 -tuples_on U)) implies y in { <*u,u*> where u is Element of U : verum } ) assume y in (U -concatenation) .: (id (1 -tuples_on U)) ; ::_thesis: y in { <*u,u*> where u is Element of U : verum } then consider x being set such that C0: ( x in dom (U -concatenation) & x in id (1 -tuples_on U) & y = (U -concatenation) . x ) by FUNCT_1:def_6; consider p being Element of 1 -tuples_on U such that C2: ( x = [p,((id (1 -tuples_on U)) . p)] & p in 1 -tuples_on U ) by C0, B1; consider u being Element of U such that C3: p = <*u*> by C2, B2; reconsider pp = p as FinSequence of U ; {((id (1 -tuples_on U)) . p)} \ {p} is empty ; then y = (U -concatenation) . (pp,pp) by C0, C2, ZFMISC_1:15; then y = <*u,u*> by Th4, C3; hence y in { <*u,u*> where u is Element of U : verum } ; ::_thesis: verum end; then B3: (U -concatenation) .: (id (1 -tuples_on U)) c= { <*u,u*> where u is Element of U : verum } by TARSKI:def_3; now__::_thesis:_for_y_being_set_st_y_in__{__<*u,u*>_where_u_is_Element_of_U_:_verum__}__holds_ y_in_(U_-concatenation)_.:_(id_(1_-tuples_on_U)) let y be set ; ::_thesis: ( y in { <*u,u*> where u is Element of U : verum } implies y in (U -concatenation) .: (id (1 -tuples_on U)) ) assume y in { <*u,u*> where u is Element of U : verum } ; ::_thesis: y in (U -concatenation) .: (id (1 -tuples_on U)) then consider u being Element of U such that C0: y = <*u,u*> ; reconsider p = <*u*> as Element of 1 -tuples_on U by FINSEQ_2:98; reconsider pp = p as FinSequence of U ; ( [p,((id (1 -tuples_on U)) . p)] = [p,p] & p in 1 -tuples_on U ) by FUNCT_1:18; then [p,p] in id (1 -tuples_on U) by B1; then reconsider dd = [p,p] as Element of id (1 -tuples_on U) ; Z0: dd in DD null [:(U *),(U *):] ; y = (U -concatenation) . (pp,pp) by C0, Th4 .= (U -concatenation) . dd ; hence y in (U -concatenation) .: (id (1 -tuples_on U)) by Z0, B0, FUNCT_1:def_6; ::_thesis: verum end; then { <*u,u*> where u is Element of U : verum } c= (U -concatenation) .: (id (1 -tuples_on U)) by TARSKI:def_3; hence (U -concatenation) .: (id (1 -tuples_on U)) = { <*u,u*> where u is Element of U : verum } by B3, XBOOLE_0:def_10; ::_thesis: verum end; registration let f be Function; let U be non empty set ; let u be Element of U; cluster((f | U) . u) \+\ (f . u) -> empty for set ; coherence for b1 being set st b1 = ((f | U) . u) \+\ (f . u) holds b1 is empty proof (f | U) . u = f . u by FUNCT_1:49; hence for b1 being set st b1 = ((f | U) . u) \+\ (f . u) holds b1 is empty ; ::_thesis: verum end; end; registration let f be Function; let U1, U2 be non empty set ; let u be Element of U1; let g be Function of U1,U2; cluster((f * g) . u) \+\ (f . (g . u)) -> empty for set ; coherence for b1 being set st b1 = ((f * g) . u) \+\ (f . (g . u)) holds b1 is empty proof dom g = U1 by FUNCT_2:def_1; then (f * g) . u = f . (g . u) by FUNCT_1:13; hence for b1 being set st b1 = ((f * g) . u) \+\ (f . (g . u)) holds b1 is empty ; ::_thesis: verum end; end; registration cluster integer non negative -> natural integer for set ; coherence for b1 being integer number st not b1 is negative holds b1 is natural proof let i be integer number ; ::_thesis: ( not i is negative implies i is natural ) assume not i is negative ; ::_thesis: i is natural then i in NAT by INT_1:3; hence i is natural ; ::_thesis: verum end; end; registration let x, y be real number ; cluster(max (x,y)) - x -> ext-real non negative for ext-real number ; coherence for b1 being ext-real number st b1 = (max (x,y)) - x holds not b1 is negative proof set z = max (x,y); x <= max (x,y) by XXREAL_0:25; then x + (- x) <= (max (x,y)) + (- x) by XREAL_1:6; then 0 <= (max (x,y)) - x ; hence for b1 being ext-real number st b1 = (max (x,y)) - x holds not b1 is negative ; ::_thesis: verum end; end; theorem :: FOMODEL0:39 for x being set st x is boolean holds ( x = 1 iff x <> 0 ) by XBOOLEAN:def_3; registration let Y be set ; let X be Subset of Y; clusterX \ Y -> empty for set ; coherence for b1 being set st b1 = X \ Y holds b1 is empty by XBOOLE_1:37; end; registration let x, y be set ; cluster{x} \ {x,y} -> empty for set ; coherence for b1 being set st b1 = {x} \ {x,y} holds b1 is empty proof x in {x,y} by TARSKI:def_2; hence for b1 being set st b1 = {x} \ {x,y} holds b1 is empty by ZFMISC_1:60; ::_thesis: verum end; cluster([x,y] `1) \+\ x -> empty for set ; coherence for b1 being set st b1 = ([x,y] `1) \+\ x holds b1 is empty proof thus for b1 being set st b1 = ([x,y] `1) \+\ x holds b1 is empty ; ::_thesis: verum end; end; registration let x, y be set ; cluster([x,y] `2) \+\ y -> empty for set ; coherence for b1 being set st b1 = ([x,y] `2) \+\ y holds b1 is empty proof thus for b1 being set st b1 = ([x,y] `2) \+\ y holds b1 is empty ; ::_thesis: verum end; end; registration let n be positive Nat; let X be non empty set ; cluster Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like countable finite-support for Element of (X *) \ {{}}; existence ex b1 being Element of (X *) \ {{}} st b1 is n -element proof consider m being Nat such that B0: n = m + 1 by NAT_1:6; set x = the Element of (m + 1) -tuples_on X; reconsider mm = m + 1 as Element of NAT by ORDINAL1:def_12; Z0: ( the Element of (m + 1) -tuples_on X in mm -tuples_on X & mm -tuples_on X c= X * ) by FINSEQ_2:134; not the Element of (m + 1) -tuples_on X in {{}} ; then reconsider xx = the Element of (m + 1) -tuples_on X as Element of (X *) \ {{}} by Z0, XBOOLE_0:def_5; take xx ; ::_thesis: xx is n -element thus xx is n -element by B0; ::_thesis: verum end; end; registration let m1 be non zero Nat; cluster Relation-like Function-like m1 + 0 -element FinSequence-like -> non empty for set ; coherence for b1 being FinSequence st b1 is m1 + 0 -element holds not b1 is empty proof let p be FinSequence; ::_thesis: ( p is m1 + 0 -element implies not p is empty ) assume p is m1 + 0 -element ; ::_thesis: not p is empty then len p = m1 by CARD_1:def_7; hence not p is empty ; ::_thesis: verum end; end; registration let R be Relation; let x be set ; clusterR null x -> Relation-like for set ; coherence for b1 being set st b1 = R null x holds b1 is Relation-like ; end; registration let f be Function-like set ; let x be set ; clusterf null x -> Function-like for set ; coherence for b1 being set st b1 = f null x holds b1 is Function-like ; end; registration let p be FinSequence-like Relation; let x be set ; clusterp null x -> FinSequence-like for Relation; coherence for b1 being Relation st b1 = p null x holds b1 is FinSequence-like ; end; registration let p be FinSequence; let x be set ; clusterp null x -> len p -element for FinSequence; coherence for b1 being FinSequence st b1 = p null x holds b1 is len p -element by CARD_1:def_7; end; registration let p be non empty FinSequence; cluster len p -> non zero for number ; coherence for b1 being number st b1 = len p holds not b1 is empty ; end; registration let R be Relation; let X be set ; clusterR | X -> X -defined for Relation; coherence for b1 being Relation st b1 = R | X holds b1 is X -defined proof dom (R | X) c= X by RELAT_1:58; hence for b1 being Relation st b1 = R | X holds b1 is X -defined by RELAT_1:def_18; ::_thesis: verum end; end; registration let x be set ; let e be empty set ; clustere null x -> empty for set ; coherence for b1 being set st b1 = e null x holds b1 is empty ; end; registration let X be set ; let e be empty set ; clustere null X -> X -valued for Relation; coherence for b1 being Relation st b1 = e null X holds b1 is X -valued proof rng e = (rng e) /\ X ; hence for b1 being Relation st b1 = e null X holds b1 is X -valued by RELAT_1:def_19; ::_thesis: verum end; end; registration let Y be non empty FinSequence-membered set ; cluster Relation-like Y -valued Function-like -> FinSequence-yielding for set ; coherence for b1 being Function st b1 is Y -valued holds b1 is FinSequence-yielding proof let f be Function; ::_thesis: ( f is Y -valued implies f is FinSequence-yielding ) assume f is Y -valued ; ::_thesis: f is FinSequence-yielding then B0: rng f c= Y by RELAT_1:def_19; now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_is_FinSequence let x be set ; ::_thesis: ( x in dom f implies f . x is FinSequence ) assume C0: x in dom f ; ::_thesis: f . x is FinSequence then reconsider D = dom f as non empty set ; reconsider xx = x as Element of D by C0; reconsider ff = f as Function of D,Y by B0, FUNCT_2:2; ff . xx in Y ; hence f . x is FinSequence ; ::_thesis: verum end; hence f is FinSequence-yielding by PRE_POLY:def_3; ::_thesis: verum end; end; registration let X, Y be set ; cluster -> FinSequence-yielding for Element of Funcs (X,(Y *)); coherence for b1 being Element of Funcs (X,(Y *)) holds b1 is FinSequence-yielding ; end; theorem Th40: :: FOMODEL0:40 for X, x being set for f being Function st f is X * -valued holds f . x in X * proof let X, x be set ; ::_thesis: for f being Function st f is X * -valued holds f . x in X * let f be Function; ::_thesis: ( f is X * -valued implies f . x in X * ) assume f is X * -valued ; ::_thesis: f . x in X * then B0: rng f c= X * by RELAT_1:def_19; percases ( x in dom f or not x in dom f ) ; supposeC0: x in dom f ; ::_thesis: f . x in X * then reconsider D = dom f as non empty set ; reconsider e = x as Element of D by C0; reconsider ff = f as Function of D,(X *) by B0, FUNCT_2:2; ff . e is Element of X * ; hence f . x in X * ; ::_thesis: verum end; suppose not x in dom f ; ::_thesis: f . x in X * then f . x = {} by FUNCT_1:def_2; hence f . x in X * by FINSEQ_1:49; ::_thesis: verum end; end; end; registration let m, n be Nat; let p be m -element FinSequence; clusterp null n -> Seg (m + n) -defined for Relation; coherence for b1 being Relation st b1 = p null n holds b1 is Seg (m + n) -defined proof dom p = Seg (len p) by FINSEQ_1:def_3; then ( m + 0 <= m + n & dom p = Seg m ) by CARD_1:def_7, XREAL_1:6; then dom p c= Seg (m + n) by FINSEQ_1:5; hence for b1 being Relation st b1 = p null n holds b1 is Seg (m + n) -defined by RELAT_1:def_18; ::_thesis: verum end; end; Lm56: for m being Nat for p1, p2, q1, q2 being FinSequence st p1 is m -element & q1 is m -element & p1 ^ p2 = q1 ^ q2 holds ( p1 = q1 & p2 = q2 ) proof let m be Nat; ::_thesis: for p1, p2, q1, q2 being FinSequence st p1 is m -element & q1 is m -element & p1 ^ p2 = q1 ^ q2 holds ( p1 = q1 & p2 = q2 ) let p1, p2, q1, q2 be FinSequence; ::_thesis: ( p1 is m -element & q1 is m -element & p1 ^ p2 = q1 ^ q2 implies ( p1 = q1 & p2 = q2 ) ) set P = p1 ^ p2; set Q = q1 ^ q2; assume ( p1 is m -element & q1 is m -element ) ; ::_thesis: ( not p1 ^ p2 = q1 ^ q2 or ( p1 = q1 & p2 = q2 ) ) then reconsider x = p1, y = q1 as m -element FinSequence ; ( Seg (len p1) = dom p1 & Seg (len q1) = dom q1 ) by FINSEQ_1:def_3; then B0: ( dom x = Seg m & dom y = Seg m ) by CARD_1:def_7; assume B1: p1 ^ p2 = q1 ^ q2 ; ::_thesis: ( p1 = q1 & p2 = q2 ) ( x null 0 is Seg (m + 0) -defined & y null 0 is Seg (m + 0) -defined ) ; then reconsider p11 = p1, q11 = q1 as Seg m -defined FinSequence ; Z0: p11 null (Seg m) = (q11 ^ q2) | (Seg m) by B0, B1, FINSEQ_6:11 .= q11 null (Seg m) by B0, FINSEQ_6:11 ; hence p1 = q1 ; ::_thesis: p2 = q2 thus p2 = q2 by Z0, B1, FINSEQ_1:33; ::_thesis: verum end; registration let m, n be Nat; let p be m -element FinSequence; let q be n -element FinSequence; clusterp ^ q -> m + n -element for FinSequence; coherence for b1 being FinSequence st b1 = p ^ q holds b1 is m + n -element proof reconsider mm = m, nn = n as Element of NAT by ORDINAL1:def_12; reconsider pp = p as mm -element FinSequence ; reconsider qq = q as nn -element FinSequence ; pp ^ qq is mm + nn -element ; hence for b1 being FinSequence st b1 = p ^ q holds b1 is m + n -element ; ::_thesis: verum end; end; theorem :: FOMODEL0:41 for m being Nat for p1, p2, q1, q2 being FinSequence st p1 is m -element & q1 is m -element & ( p1 ^ p2 = q1 ^ q2 or p2 ^ p1 = q2 ^ q1 ) holds ( p1 = q1 & p2 = q2 ) proof let m be Nat; ::_thesis: for p1, p2, q1, q2 being FinSequence st p1 is m -element & q1 is m -element & ( p1 ^ p2 = q1 ^ q2 or p2 ^ p1 = q2 ^ q1 ) holds ( p1 = q1 & p2 = q2 ) let p1, p2, q1, q2 be FinSequence; ::_thesis: ( p1 is m -element & q1 is m -element & ( p1 ^ p2 = q1 ^ q2 or p2 ^ p1 = q2 ^ q1 ) implies ( p1 = q1 & p2 = q2 ) ) set m1 = len p1; set m2 = len p2; set n1 = len q1; set n2 = len q2; assume ( p1 is m -element & q1 is m -element ) ; ::_thesis: ( ( not p1 ^ p2 = q1 ^ q2 & not p2 ^ p1 = q2 ^ q1 ) or ( p1 = q1 & p2 = q2 ) ) then reconsider p11 = p1, q11 = q1 as m -element FinSequence ; reconsider p22 = p2 null p2 as len p2 -element FinSequence ; reconsider q22 = q2 null q2 as len q2 -element FinSequence ; set PA = p11 ^ p22; set PB = p22 ^ p11; set QA = q11 ^ q22; set QB = q22 ^ q11; B0: ( len (p11 ^ p22) = m + (len p2) & len (p22 ^ p11) = (len p2) + m & len (q11 ^ q22) = m + (len q2) & len (q22 ^ q11) = (len q2) + m ) by CARD_1:def_7; assume Z1: ( p1 ^ p2 = q1 ^ q2 or p2 ^ p1 = q2 ^ q1 ) ; ::_thesis: ( p1 = q1 & p2 = q2 ) then B2: ( p11 ^ p22 = q11 ^ q22 or p22 ^ p11 = q22 ^ q11 ) ; reconsider q22 = q22 as len p2 -element FinSequence by Z1, B0; ( p22 is len p2 -element & q22 is len p2 -element ) ; hence ( p1 = q1 & p2 = q2 ) by B2, Lm56; ::_thesis: verum end; theorem :: FOMODEL0:42 for x being set for U, U1 being non empty set st (U -multiCat) . x is U1 -valued & x in (U *) * holds x is FinSequence of U1 * proof let x be set ; ::_thesis: for U, U1 being non empty set st (U -multiCat) . x is U1 -valued & x in (U *) * holds x is FinSequence of U1 * let U, U1 be non empty set ; ::_thesis: ( (U -multiCat) . x is U1 -valued & x in (U *) * implies x is FinSequence of U1 * ) set C = U -multiCat ; set f = U -concatenation ; set F = MultPlace (U -concatenation); set D = U * ; {} null (U *) is U * -valued Relation ; then reconsider e = {} as U * -valued FinSequence ; defpred S1[ Nat] means for p being U * -valued \$1 + 1 -element FinSequence st (U -multiCat) . p is U1 -valued holds p is U1 * -valued ; B0: S1[ 0 ] proof let p be U * -valued 0 + 1 -element FinSequence; ::_thesis: ( (U -multiCat) . p is U1 -valued implies p is U1 * -valued ) reconsider ppp = p as U * -valued 1 + 0 -element FinSequence ; {(ppp . 1)} \ (U *) = {} ; then reconsider p1 = p . 1 as Element of U * by ZFMISC_1:60; Z0: len p = 1 by CARD_1:def_7; p = {} ^ <*(p . 1)*> by Z0, FINSEQ_1:40; then C0: (U -multiCat) . p = ((U -multiCat) . e) ^ p1 by Th33 .= {} ^ (p . 1) .= p . 1 ; p is 1 -element FinSequence of U * by Lm45; then reconsider pp = p as 1 -element Element of (U *) * by FINSEQ_1:def_11; assume (U -multiCat) . p is U1 -valued ; ::_thesis: p is U1 * -valued then reconsider u1 = (U -multiCat) . pp as FinSequence of U1 by Lm45; u1 = p . 1 by C0; then reconsider q = p . 1 as Element of U1 * by FINSEQ_1:def_11; <*q*> is FinSequence of U1 * ; hence p is U1 * -valued by Z0, FINSEQ_1:40; ::_thesis: verum end; B1: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) reconsider NN = n + 1 as non zero Element of NAT by ORDINAL1:def_12; assume C1: S1[n] ; ::_thesis: S1[n + 1] let p be U * -valued (n + 1) + 1 -element FinSequence; ::_thesis: ( (U -multiCat) . p is U1 -valued implies p is U1 * -valued ) assume C0: (U -multiCat) . p is U1 -valued ; ::_thesis: p is U1 * -valued reconsider pp = p null p as U * -valued n + 2 -element FinSequence ; reconsider ppp = pp as U * -valued NN + 1 -element FinSequence ; reconsider pppp = ppp as U * -valued (NN + 1) + 0 -element FinSequence ; reconsider p1 = ppp | (Seg NN) as U * -valued NN -element FinSequence ; {(pppp . (NN + 1))} \ (U *) = {} ; then reconsider u = ppp . (NN + 1) as Element of U * by ZFMISC_1:60; Z0: ppp \+\ (p1 ^ <*(ppp . (NN + 1))*>) = {} ; then p = p1 ^ <*u*> by Th29; then C2: (U -multiCat) . p = ((U -multiCat) . p1) ^ u by Th33; then ( rng ((U -multiCat) . p) c= U1 & rng ((U -multiCat) . p1) c= rng ((U -multiCat) . p) ) by C0, FINSEQ_1:29, RELAT_1:def_19; then rng ((U -multiCat) . p1) c= U1 by XBOOLE_1:1; then reconsider q = (U -multiCat) . p1 as U1 -valued FinSequence by RELAT_1:def_19; q is U1 -valued ; then reconsider p11 = p1 as U1 * -valued NN -element FinSequence by C1; ( rng u c= rng ((U -multiCat) . p) & rng ((U -multiCat) . p) c= U1 ) by C2, C0, FINSEQ_1:30, RELAT_1:def_19; then rng u c= U1 by XBOOLE_1:1; then u is U1 -valued by RELAT_1:def_19; then u is FinSequence of U1 by Lm45; then reconsider uu = u as Element of U1 * by FINSEQ_1:def_11; p11 ^ <*uu*> is U1 * -valued ; hence p is U1 * -valued by Z0, Th29; ::_thesis: verum end; B3: for n being Nat holds S1[n] from NAT_1:sch_2(B0, B1); assume B2: ( (U -multiCat) . x is U1 -valued & x in (U *) * ) ; ::_thesis: x is FinSequence of U1 * percases ( x is empty or not x is empty ) ; suppose x is empty ; ::_thesis: x is FinSequence of U1 * then reconsider xx = x as empty set ; xx null (U1 *) is U1 * -valued FinSequence ; hence x is FinSequence of U1 * by Lm45; ::_thesis: verum end; suppose not x is empty ; ::_thesis: x is FinSequence of U1 * then reconsider xx = x as U * -valued non empty FinSequence by B2; consider m being Nat such that C0: len xx = m + 1 by NAT_1:6; xx null {} is m + 1 -element by C0; then reconsider xxx = xx as U * -valued m + 1 -element FinSequence ; xxx is U1 * -valued by B2, B3; hence x is FinSequence of U1 * by Lm45; ::_thesis: verum end; end; end; registration let m be Nat; cluster Relation-like Function-like m + 1 -element FinSequence-like -> non empty for set ; coherence for b1 being FinSequence st b1 is m + 1 -element holds not b1 is empty proof let p be FinSequence; ::_thesis: ( p is m + 1 -element implies not p is empty ) set M = m + 1; assume p is m + 1 -element ; ::_thesis: not p is empty then reconsider pp = p as (m + 1) + 0 -element FinSequence ; not pp is empty ; hence not p is empty ; ::_thesis: verum end; end; registration let U be non empty set ; let u be Element of U; cluster((id U) . u) \+\ u -> empty for set ; coherence for b1 being set st b1 = ((id U) . u) \+\ u holds b1 is empty proof {((id U) . u)} \ {u} = {} ; then (id U) . u = u by ZFMISC_1:15; hence for b1 being set st b1 = ((id U) . u) \+\ u holds b1 is empty ; ::_thesis: verum end; end; registration let U be non empty set ; let p be U -valued non empty FinSequence; cluster{(p . 1)} \ U -> empty for set ; coherence for b1 being set st b1 = {(p . 1)} \ U holds b1 is empty proof consider m being Nat such that B0: len p = m + 1 by NAT_1:6; reconsider pp = p as U -valued 1 + m -element FinSequence by B0, CARD_1:def_7; {(pp . 1)} \ U = {} ; hence for b1 being set st b1 = {(p . 1)} \ U holds b1 is empty ; ::_thesis: verum end; end; theorem :: FOMODEL0:43 for x1, x2, y1, y2 being set for f being Function holds ( ( x1 = x2 implies (f +* (x1 .--> y1)) +* (x2 .--> y2) = f +* (x2 .--> y2) ) & ( x1 <> x2 implies (f +* (x1 .--> y1)) +* (x2 .--> y2) = (f +* (x2 .--> y2)) +* (x1 .--> y1) ) ) proof let x1, x2, y1, y2 be set ; ::_thesis: for f being Function holds ( ( x1 = x2 implies (f +* (x1 .--> y1)) +* (x2 .--> y2) = f +* (x2 .--> y2) ) & ( x1 <> x2 implies (f +* (x1 .--> y1)) +* (x2 .--> y2) = (f +* (x2 .--> y2)) +* (x1 .--> y1) ) ) let f be Function; ::_thesis: ( ( x1 = x2 implies (f +* (x1 .--> y1)) +* (x2 .--> y2) = f +* (x2 .--> y2) ) & ( x1 <> x2 implies (f +* (x1 .--> y1)) +* (x2 .--> y2) = (f +* (x2 .--> y2)) +* (x1 .--> y1) ) ) set f1 = x1 .--> y1; set f2 = x2 .--> y2; set LH = (f +* (x1 .--> y1)) +* (x2 .--> y2); hereby ::_thesis: ( x1 <> x2 implies (f +* (x1 .--> y1)) +* (x2 .--> y2) = (f +* (x2 .--> y2)) +* (x1 .--> y1) ) assume x1 = x2 ; ::_thesis: (f +* (x1 .--> y1)) +* (x2 .--> y2) = f +* (x2 .--> y2) then {x1} = dom (x2 .--> y2) by FUNCOP_1:13; then dom (x1 .--> y1) = dom (x2 .--> y2) by FUNCOP_1:13; then (x1 .--> y1) +* (x2 .--> y2) = x2 .--> y2 by FUNCT_4:19; hence (f +* (x1 .--> y1)) +* (x2 .--> y2) = f +* (x2 .--> y2) by FUNCT_4:14; ::_thesis: verum end; assume x1 <> x2 ; ::_thesis: (f +* (x1 .--> y1)) +* (x2 .--> y2) = (f +* (x2 .--> y2)) +* (x1 .--> y1) then {x1} misses {x2} by ZFMISC_1:11; then x1 .--> y1 tolerates x2 .--> y2 by FUNCOP_1:87; then f +* ((x1 .--> y1) +* (x2 .--> y2)) = f +* ((x2 .--> y2) +* (x1 .--> y1)) by FUNCT_4:34 .= (f +* (x2 .--> y2)) +* (x1 .--> y1) by FUNCT_4:14 ; hence (f +* (x1 .--> y1)) +* (x2 .--> y2) = (f +* (x2 .--> y2)) +* (x1 .--> y1) by FUNCT_4:14; ::_thesis: verum end; registration let X be set ; let U be non empty set ; cluster Relation-like X -defined U -valued Function-like total for set ; existence ex b1 being X -defined Function st ( b1 is U -valued & b1 is total ) proof take the total PartFunc of X,U ; ::_thesis: ( the total PartFunc of X,U is U -valued & the total PartFunc of X,U is total ) thus ( the total PartFunc of X,U is U -valued & the total PartFunc of X,U is total ) ; ::_thesis: verum end; end; registration let X be set ; let U be non empty set ; let P be X -defined U -valued total Relation; let Q be U -defined total Relation; clusterP * Q -> X -defined total for X -defined Relation; coherence for b1 being X -defined Relation st b1 = P * Q holds b1 is total proof ( rng P c= U & dom Q = U ) by PARTFUN1:def_2; then dom (P * Q) = dom P by RELAT_1:27 .= X by PARTFUN1:def_2 ; hence for b1 being X -defined Relation st b1 = P * Q holds b1 is total by PARTFUN1:def_2; ::_thesis: verum end; end; theorem :: FOMODEL0:44 for X being set for p, p1, p2 being FinSequence st (p ^ p1) ^ p2 is X -valued holds ( p2 is X -valued & p1 is X -valued & p is X -valued ) proof let X be set ; ::_thesis: for p, p1, p2 being FinSequence st (p ^ p1) ^ p2 is X -valued holds ( p2 is X -valued & p1 is X -valued & p is X -valued ) let p, p1, p2 be FinSequence; ::_thesis: ( (p ^ p1) ^ p2 is X -valued implies ( p2 is X -valued & p1 is X -valued & p is X -valued ) ) set q = (p ^ p1) ^ p2; assume (p ^ p1) ^ p2 is X -valued ; ::_thesis: ( p2 is X -valued & p1 is X -valued & p is X -valued ) then ( rng ((p ^ p1) ^ p2) c= X & rng (p ^ p1) c= rng ((p ^ p1) ^ p2) & rng p2 c= rng ((p ^ p1) ^ p2) ) by FINSEQ_1:29, FINSEQ_1:30, RELAT_1:def_19; then ( rng p2 c= X & rng p c= rng (p ^ p1) & rng p1 c= rng (p ^ p1) & rng (p ^ p1) c= X ) by FINSEQ_1:29, FINSEQ_1:30, XBOOLE_1:1; then ( rng p c= X & rng p1 c= X & rng p2 c= X ) by XBOOLE_1:1; hence ( p2 is X -valued & p1 is X -valued & p is X -valued ) by RELAT_1:def_19; ::_thesis: verum end; registration let X be set ; let R be Relation; clusterR null X -> X \/ (rng R) -valued for Relation; coherence for b1 being Relation st b1 = R null X holds b1 is X \/ (rng R) -valued proof (rng R) null X c= (rng R) \/ X ; hence for b1 being Relation st b1 = R null X holds b1 is X \/ (rng R) -valued by RELAT_1:def_19; ::_thesis: verum end; end; registration let X, Y be functional set ; clusterX \/ Y -> functional ; coherence X \/ Y is functional proof now__::_thesis:_for_x_being_set_st_x_in_X_\/_Y_holds_ x_is_Function let x be set ; ::_thesis: ( x in X \/ Y implies x is Function ) assume x in X \/ Y ; ::_thesis: x is Function then ( x in X or x in Y ) by XBOOLE_0:def_3; hence x is Function ; ::_thesis: verum end; hence X \/ Y is functional by FUNCT_1:def_13; ::_thesis: verum end; end; registration cluster FinSequence-membered -> finite-membered for set ; coherence for b1 being set st b1 is FinSequence-membered holds b1 is finite-membered proof let X be set ; ::_thesis: ( X is FinSequence-membered implies X is finite-membered ) assume B0: X is FinSequence-membered ; ::_thesis: X is finite-membered for x being set st x in X holds x is finite by B0; hence X is finite-membered by FINSET_1:def_6; ::_thesis: verum end; end; definition let X be functional set ; func SymbolsOf X -> set equals :: FOMODEL0:def 24 union { (rng x) where x is Element of X \/ {{}} : x in X } ; coherence union { (rng x) where x is Element of X \/ {{}} : x in X } is set ; end; :: deftheorem defines SymbolsOf FOMODEL0:def_24_:_ for X being functional set holds SymbolsOf X = union { (rng x) where x is Element of X \/ {{}} : x in X } ; Lm58: for X being functional set st X is finite & X is finite-membered holds SymbolsOf X is finite proof let X be functional set ; ::_thesis: ( X is finite & X is finite-membered implies SymbolsOf X is finite ) set Y = X \/ {{}}; set F = { (rng y) where y is Element of X \/ {{}} : y in X } ; assume B0: X is finite ; ::_thesis: ( not X is finite-membered or SymbolsOf X is finite ) { (rng y) where y is Element of X \/ {{}} : y in X } is finite from FRAENKEL:sch_21(B0); then reconsider FF = { (rng y) where y is Element of X \/ {{}} : y in X } as finite set ; assume X is finite-membered ; ::_thesis: SymbolsOf X is finite then reconsider YY = X \/ {{}} as finite-membered set ; now__::_thesis:_for_y_being_set_st_y_in__{__(rng_y)_where_y_is_Element_of_X_\/_{{}}_:_y_in_X__}__holds_ y_is_finite let y be set ; ::_thesis: ( y in { (rng y) where y is Element of X \/ {{}} : y in X } implies y is finite ) assume y in { (rng y) where y is Element of X \/ {{}} : y in X } ; ::_thesis: y is finite then consider x being Element of X \/ {{}} such that C0: ( y = rng x & x in X ) ; reconsider xx = x as Element of YY ; xx is finite ; hence y is finite by C0; ::_thesis: verum end; then reconsider FFF = FF as finite finite-membered set by FINSET_1:def_6; union FFF is finite ; hence SymbolsOf X is finite ; ::_thesis: verum end; registration cluster non empty trivial FinSequence-membered for set ; existence ex b1 being set st ( b1 is trivial & b1 is FinSequence-membered & not b1 is empty ) proof take { the Element of the non empty set * } ; ::_thesis: ( { the Element of the non empty set * } is trivial & { the Element of the non empty set * } is FinSequence-membered & not { the Element of the non empty set * } is empty ) thus ( { the Element of the non empty set * } is trivial & { the Element of the non empty set * } is FinSequence-membered & not { the Element of the non empty set * } is empty ) ; ::_thesis: verum end; end; registration let X be functional finite finite-membered set ; cluster SymbolsOf X -> finite ; coherence SymbolsOf X is finite by Lm58; end; registration let X be finite FinSequence-membered set ; cluster SymbolsOf X -> finite ; coherence SymbolsOf X is finite ; end; theorem :: FOMODEL0:45 for f being Function holds SymbolsOf {f} = rng f proof let f be Function; ::_thesis: SymbolsOf {f} = rng f set P = f; set X = {f}; set F = { (rng x) where x is Element of {f} \/ {{}} : x in {f} } ; set LH = union { (rng x) where x is Element of {f} \/ {{}} : x in {f} } ; set RH = rng f; {f} null {{}} c= {f} \/ {{}} ; then reconsider XX = {f} as Subset of ({f} \/ {{}}) ; reconsider PP = f as Element of XX by TARSKI:def_1; reconsider PPP = PP as Element of {f} \/ {{}} by TARSKI:def_3; now__::_thesis:_for_y_being_set_st_y_in_union__{__(rng_x)_where_x_is_Element_of_{f}_\/_{{}}_:_x_in_{f}__}__holds_ y_in_rng_f let y be set ; ::_thesis: ( y in union { (rng x) where x is Element of {f} \/ {{}} : x in {f} } implies y in rng f ) assume y in union { (rng x) where x is Element of {f} \/ {{}} : x in {f} } ; ::_thesis: y in rng f then consider z being set such that C0: ( y in z & z in { (rng x) where x is Element of {f} \/ {{}} : x in {f} } ) by TARSKI:def_4; consider x being Element of {f} \/ {{}} such that C1: ( z = rng x & x in {f} ) by C0; thus y in rng f by C0, C1, TARSKI:def_1; ::_thesis: verum end; then B0: union { (rng x) where x is Element of {f} \/ {{}} : x in {f} } c= rng f by TARSKI:def_3; now__::_thesis:_for_y_being_set_st_y_in_rng_f_holds_ y_in_union__{__(rng_x)_where_x_is_Element_of_{f}_\/_{{}}_:_x_in_{f}__}_ let y be set ; ::_thesis: ( y in rng f implies y in union { (rng x) where x is Element of {f} \/ {{}} : x in {f} } ) assume y in rng f ; ::_thesis: y in union { (rng x) where x is Element of {f} \/ {{}} : x in {f} } then ( y in rng PP & rng PPP in { (rng x) where x is Element of {f} \/ {{}} : x in {f} } ) ; hence y in union { (rng x) where x is Element of {f} \/ {{}} : x in {f} } by TARSKI:def_4; ::_thesis: verum end; then rng f c= union { (rng x) where x is Element of {f} \/ {{}} : x in {f} } by TARSKI:def_3; hence SymbolsOf {f} = rng f by B0, XBOOLE_0:def_10; ::_thesis: verum end; registration let z be non zero complex number ; cluster|.z.| -> ext-real positive for ext-real number ; coherence for b1 being ext-real number st b1 = abs z holds b1 is positive by COMPLEX1:47; end; scheme :: FOMODEL0:sch 1 Sc1{ F1() -> set , F2() -> set , F3( set ) -> set } : { F3(x) where x is Element of F1() : x in F1() } = { F3(x) where x is Element of F2() : x in F1() } provided B0: F1() c= F2() proof set LH = { F3(x) where x is Element of F1() : x in F1() } ; set RH = { F3(x) where x is Element of F2() : x in F1() } ; now__::_thesis:_for_y_being_set_st_y_in__{__F3(x)_where_x_is_Element_of_F1()_:_x_in_F1()__}__holds_ y_in__{__F3(x)_where_x_is_Element_of_F2()_:_x_in_F1()__}_ let y be set ; ::_thesis: ( y in { F3(x) where x is Element of F1() : x in F1() } implies y in { F3(x) where x is Element of F2() : x in F1() } ) assume y in { F3(x) where x is Element of F1() : x in F1() } ; ::_thesis: y in { F3(x) where x is Element of F2() : x in F1() } then consider x being Element of F1() such that C0: ( y = F3(x) & x in F1() ) ; reconsider xx = x as Element of F2() by C0, B0; ( y = F3(xx) & xx in F1() ) by C0; hence y in { F3(x) where x is Element of F2() : x in F1() } ; ::_thesis: verum end; then B1: { F3(x) where x is Element of F1() : x in F1() } c= { F3(x) where x is Element of F2() : x in F1() } by TARSKI:def_3; now__::_thesis:_for_y_being_set_st_y_in__{__F3(x)_where_x_is_Element_of_F2()_:_x_in_F1()__}__holds_ y_in__{__F3(x)_where_x_is_Element_of_F1()_:_x_in_F1()__}_ let y be set ; ::_thesis: ( y in { F3(x) where x is Element of F2() : x in F1() } implies y in { F3(x) where x is Element of F1() : x in F1() } ) assume y in { F3(x) where x is Element of F2() : x in F1() } ; ::_thesis: y in { F3(x) where x is Element of F1() : x in F1() } then consider x being Element of F2() such that C2: ( y = F3(x) & x in F1() ) ; reconsider xx = x as Element of F1() by C2; thus y in { F3(x) where x is Element of F1() : x in F1() } by C2; ::_thesis: verum end; then { F3(x) where x is Element of F2() : x in F1() } c= { F3(x) where x is Element of F1() : x in F1() } by TARSKI:def_3; hence { F3(x) where x is Element of F1() : x in F1() } = { F3(x) where x is Element of F2() : x in F1() } by B1, XBOOLE_0:def_10; ::_thesis: verum end; definition let X be functional set ; redefine func SymbolsOf X equals :: FOMODEL0:def 25 union { (rng x) where x is Element of X : x in X } ; compatibility for b1 being set holds ( b1 = SymbolsOf X iff b1 = union { (rng x) where x is Element of X : x in X } ) proof set F1 = { (rng x) where x is Element of X : x in X } ; set F2 = { (rng x) where x is Element of X \/ {{}} : x in X } ; X null {{}} c= X \/ {{}} ; then B0: X c= X \/ {{}} ; { (rng x) where x is Element of X : x in X } = { (rng x) where x is Element of X \/ {{}} : x in X } from FOMODEL0:sch_1(B0); hence for b1 being set holds ( b1 = SymbolsOf X iff b1 = union { (rng x) where x is Element of X : x in X } ) ; ::_thesis: verum end; end; :: deftheorem defines SymbolsOf FOMODEL0:def_25_:_ for X being functional set holds SymbolsOf X = union { (rng x) where x is Element of X : x in X } ; Lm57: for B being functional set for A being Subset of B holds { (rng x) where x is Element of A : x in A } c= { (rng x) where x is Element of B : x in B } proof let B be functional set ; ::_thesis: for A being Subset of B holds { (rng x) where x is Element of A : x in A } c= { (rng x) where x is Element of B : x in B } let A be Subset of B; ::_thesis: { (rng x) where x is Element of A : x in A } c= { (rng x) where x is Element of B : x in B } set AF = { (rng x) where x is Element of A : x in A } ; set BF = { (rng x) where x is Element of B : x in B } ; now__::_thesis:_for_y_being_set_st_y_in__{__(rng_x)_where_x_is_Element_of_A_:_x_in_A__}__holds_ y_in__{__(rng_x)_where_x_is_Element_of_B_:_x_in_B__}_ let y be set ; ::_thesis: ( y in { (rng x) where x is Element of A : x in A } implies y in { (rng x) where x is Element of B : x in B } ) assume y in { (rng x) where x is Element of A : x in A } ; ::_thesis: y in { (rng x) where x is Element of B : x in B } then consider x being Element of A such that C0: ( y = rng x & x in A ) ; reconsider xb = x as Element of B by C0; thus y in { (rng x) where x is Element of B : x in B } by C0; ::_thesis: verum end; hence { (rng x) where x is Element of A : x in A } c= { (rng x) where x is Element of B : x in B } by TARSKI:def_3; ::_thesis: verum end; theorem :: FOMODEL0:46 for B being functional set for A being Subset of B holds SymbolsOf A c= SymbolsOf B by Lm57, ZFMISC_1:77; theorem :: FOMODEL0:47 for A, B being functional set holds SymbolsOf (A \/ B) = (SymbolsOf A) \/ (SymbolsOf B) proof let A, B be functional set ; ::_thesis: SymbolsOf (A \/ B) = (SymbolsOf A) \/ (SymbolsOf B) set AF = { (rng x) where x is Element of A : x in A } ; set BF = { (rng x) where x is Element of B : x in B } ; set F = { (rng x) where x is Element of A \/ B : x in A \/ B } ; ( A null B c= A \/ B & B null A c= A \/ B ) ; then reconsider AFF = { (rng x) where x is Element of A : x in A } , BFF = { (rng x) where x is Element of B : x in B } as Subset of { (rng x) where x is Element of A \/ B : x in A \/ B } by Lm57; B0: AFF \/ BFF c= { (rng x) where x is Element of A \/ B : x in A \/ B } ; now__::_thesis:_for_y_being_set_st_y_in__{__(rng_x)_where_x_is_Element_of_A_\/_B_:_x_in_A_\/_B__}__\__{__(rng_x)_where_x_is_Element_of_B_:_x_in_B__}__holds_ y_in__{__(rng_x)_where_x_is_Element_of_A_:_x_in_A__}_ let y be set ; ::_thesis: ( y in { (rng x) where x is Element of A \/ B : x in A \/ B } \ { (rng x) where x is Element of B : x in B } implies y in { (rng x) where x is Element of A : x in A } ) assume y in { (rng x) where x is Element of A \/ B : x in A \/ B } \ { (rng x) where x is Element of B : x in B } ; ::_thesis: y in { (rng x) where x is Element of A : x in A } then C1: ( y in { (rng x) where x is Element of A \/ B : x in A \/ B } & not y in { (rng x) where x is Element of B : x in B } ) by XBOOLE_0:def_5; then consider x being Element of A \/ B such that C0: ( y = rng x & x in A \/ B ) ; not x in B by C0, C1; then C2: x in A null {{}} by C0, XBOOLE_0:def_3; then reconsider xx = x as Element of A \/ {{}} ; thus y in { (rng x) where x is Element of A : x in A } by C2, C0; ::_thesis: verum end; then { (rng x) where x is Element of A \/ B : x in A \/ B } \ { (rng x) where x is Element of B : x in B } c= { (rng x) where x is Element of A : x in A } by TARSKI:def_3; then ( { (rng x) where x is Element of A \/ B : x in A \/ B } \ { (rng x) where x is Element of B : x in B } ) \/ { (rng x) where x is Element of B : x in B } c= { (rng x) where x is Element of A : x in A } \/ { (rng x) where x is Element of B : x in B } by XBOOLE_1:9; then { (rng x) where x is Element of A \/ B : x in A \/ B } null BFF c= { (rng x) where x is Element of A : x in A } \/ { (rng x) where x is Element of B : x in B } by XBOOLE_1:39; then B1: { (rng x) where x is Element of A : x in A } \/ { (rng x) where x is Element of B : x in B } = { (rng x) where x is Element of A \/ B : x in A \/ B } by B0, XBOOLE_0:def_10; thus SymbolsOf (A \/ B) = (SymbolsOf A) \/ (SymbolsOf B) by B1, ZFMISC_1:78; ::_thesis: verum end; registration let X be set ; let F be Subset of (bool X); cluster(union F) \ X -> empty for set ; coherence for b1 being set st b1 = (union F) \ X holds b1 is empty ; end; theorem Th48: :: FOMODEL0:48 for X, Y being set holds X = (X \ Y) \/ (X /\ Y) proof let X, Y be set ; ::_thesis: X = (X \ Y) \/ (X /\ Y) reconsider x = X \ Y as Subset of X ; X = x \/ (X \ x) by XBOOLE_1:45 .= x \/ (X /\ Y) by XBOOLE_1:48 ; hence X = (X \ Y) \/ (X /\ Y) ; ::_thesis: verum end; theorem :: FOMODEL0:49 for A, B being set for m, n being Nat st m -tuples_on A meets n -tuples_on B holds m = n by Lm18; theorem :: FOMODEL0:50 for D being non empty set for B, A being set st B is D -prefix & A c= B holds A is D -prefix by Lm59; theorem :: FOMODEL0:51 for f, g being Function holds ( f c= g iff for x being set st x in dom f holds ( x in dom g & f . x = g . x ) ) proof let f, g be Function; ::_thesis: ( f c= g iff for x being set st x in dom f holds ( x in dom g & f . x = g . x ) ) defpred S1[] means for x being set st x in dom f holds x in dom g; defpred S2[] means for x being set st x in dom f holds f . x = g . x; defpred S3[] means for x being set st x in dom f holds ( x in dom g & f . x = g . x ); ( S1[] & S2[] iff ( dom f c= dom g & S2[] ) ) by TARSKI:def_3; hence ( f c= g iff for x being set st x in dom f holds ( x in dom g & f . x = g . x ) ) by GRFUNC_1:2; ::_thesis: verum end; registration let U be non empty set ; cluster non empty -> non empty-yielding for Element of ((U *) \ {{}}) * ; coherence for b1 being Element of ((U *) \ {{}}) * st not b1 is empty holds not b1 is empty-yielding proof set D = ((U *) \ {{}}) * ; let p be Element of ((U *) \ {{}}) * ; ::_thesis: ( not p is empty implies not p is empty-yielding ) assume not p is empty ; ::_thesis: not p is empty-yielding then consider m being Nat such that B0: m + 1 = len p by NAT_1:6; reconsider pp = p as (U *) \ {{}} -valued 1 + m -element FinSequence by B0, CARD_1:def_7; {(pp . 1)} \ ((U *) \ {{}}) = {} ; then pp . 1 in (U *) \ {{}} by ZFMISC_1:60; then ( p . 1 in U * & not p . 1 in {{}} ) by XBOOLE_0:def_5; then p . 1 <> {} by TARSKI:def_1; hence not p is empty-yielding ; ::_thesis: verum end; end; registration let e be empty set ; cluster -> empty for Element of e * ; coherence for b1 being Element of e * holds b1 is empty ; end; theorem Th52: :: FOMODEL0:52 for x being set for U1, U2 being non empty set for p being FinSequence holds ( ( (U1 -multiCat) . x <> {} & (U2 -multiCat) . x <> {} implies (U1 -multiCat) . x = (U2 -multiCat) . x ) & ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {} * -valued ) ) proof let x be set ; ::_thesis: for U1, U2 being non empty set for p being FinSequence holds ( ( (U1 -multiCat) . x <> {} & (U2 -multiCat) . x <> {} implies (U1 -multiCat) . x = (U2 -multiCat) . x ) & ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {} * -valued ) ) let U1, U2 be non empty set ; ::_thesis: for p being FinSequence holds ( ( (U1 -multiCat) . x <> {} & (U2 -multiCat) . x <> {} implies (U1 -multiCat) . x = (U2 -multiCat) . x ) & ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {} * -valued ) ) let p be FinSequence; ::_thesis: ( ( (U1 -multiCat) . x <> {} & (U2 -multiCat) . x <> {} implies (U1 -multiCat) . x = (U2 -multiCat) . x ) & ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {} * -valued ) ) reconsider e = {} as Element of {{}} by TARSKI:def_1; defpred S1[ Nat] means for U1, U2 being non empty set for p being FinSequence st p is \$1 + 1 -element holds ( ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) & ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) ); A0: S1[ 0 ] proof let U1, U2 be non empty set ; ::_thesis: for p being FinSequence st p is 0 + 1 -element holds ( ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) & ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) ) let p be FinSequence; ::_thesis: ( p is 0 + 1 -element implies ( ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) & ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) ) ) set C1 = U1 -multiCat ; set C2 = U2 -multiCat ; B2: ( dom (U1 -multiCat) = (U1 *) * & dom (U2 -multiCat) = (U2 *) * ) by FUNCT_2:def_1; {} /\ U1 = {} ; then reconsider EE = {} as Subset of U1 ; {} /\ U2 = {} ; then reconsider EE2 = {} as Subset of U2 ; reconsider E2 = EE2 * as non empty Subset of (U2 *) ; reconsider eu2 = {} as Element of E2 by TARSKI:def_1; reconsider E = EE * as non empty Subset of (U1 *) ; reconsider euu = {} as Element of E by TARSKI:def_1; assume p is 0 + 1 -element ; ::_thesis: ( ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) & ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) ) then reconsider pp = p as 1 + 0 -element FinSequence ; len pp = 1 by CARD_1:def_7; then B0: p = {} ^ <*(p . 1)*> by FINSEQ_1:40 .= euu ^ <*(p . 1)*> ; hereby ::_thesis: ( ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) & ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) ) assume p is {} * -valued ; ::_thesis: (U1 -multiCat) . p = {} then p = euu ^ <*euu*> by B0; hence (U1 -multiCat) . p = ((U1 -multiCat) . euu) ^ euu by Th33 .= {} ^ {} .= {} ; ::_thesis: verum end; hereby ::_thesis: ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) assume D0: ( (U1 -multiCat) . p = {} & p is U1 * -valued ) ; ::_thesis: p is {{}} -valued then reconsider ppp = pp as U1 * -valued non empty FinSequence ; {(ppp . 1)} \ (U1 *) = {} ; then reconsider l = pp . 1 as Element of U1 * by ZFMISC_1:60; (U1 -multiCat) . p = ((U1 -multiCat) . euu) ^ l by Th33, B0 .= {} ^ l .= l ; then p = euu ^ <*euu*> by B0, D0; hence p is {{}} -valued ; ::_thesis: verum end; hereby ::_thesis: verum assume ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} ) ; ::_thesis: (U1 -multiCat) . p = (U2 -multiCat) . p then D0: ( p in (U1 *) * & p in (U2 *) * ) by B2, FUNCT_1:def_2; reconsider p1 = pp as U1 * -valued non empty FinSequence by D0; reconsider p2 = pp as U2 * -valued non empty FinSequence by D0; Z0: ( {(p1 . 1)} \ (U1 *) = {} & {(p2 . 1)} \ (U2 *) = {} ) ; reconsider u1 = p1 . 1 as Element of U1 * by Z0, ZFMISC_1:60; reconsider u2 = p2 . 1 as Element of U2 * by Z0, ZFMISC_1:60; D2: (U1 -multiCat) . p = ((U1 -multiCat) . euu) ^ u1 by B0, Th33 .= {} ^ u1 .= u1 ; (U2 -multiCat) . p = ((U2 -multiCat) . eu2) ^ u2 by B0, Th33 .= {} ^ u1 .= u1 ; hence (U1 -multiCat) . p = (U2 -multiCat) . p by D2; ::_thesis: verum end; end; A1: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume D2: S1[n] ; ::_thesis: S1[n + 1] let U1, U2 be non empty set ; ::_thesis: for p being FinSequence st p is (n + 1) + 1 -element holds ( ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) & ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) ) set C1 = U1 -multiCat ; set C2 = U2 -multiCat ; B0: ( dom (U1 -multiCat) = (U1 *) * & dom (U2 -multiCat) = (U2 *) * ) by FUNCT_2:def_1; let p be FinSequence; ::_thesis: ( p is (n + 1) + 1 -element implies ( ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) & ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) ) ) assume D0: p is (n + 1) + 1 -element ; ::_thesis: ( ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) & ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) ) thus ( p is {} * -valued implies (U1 -multiCat) . p = {} ) ::_thesis: ( ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) & ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) ) proof {} /\ U1 = {} ; then reconsider EE = {} as Subset of U1 ; reconsider E = EE * as non empty Subset of (U1 *) ; assume p is {} * -valued ; ::_thesis: (U1 -multiCat) . p = {} then reconsider pp = p as {} * -valued ((n + 1) + 1) + 0 -element FinSequence by D0; reconsider p1 = pp | (Seg (n + 1)) as E -valued n + 1 -element FinSequence ; {(pp . ((n + 1) + 1))} \ ({} *) = {} ; then reconsider x1 = pp . ((n + 1) + 1) as Element of E by ZFMISC_1:60; pp \+\ (p1 ^ <*x1*>) = {} ; then ( pp = p1 ^ <*x1*> & p1 is U1 * -valued ) by Th29; then (U1 -multiCat) . pp = ((U1 -multiCat) . p1) ^ x1 by Th33 .= ((U1 -multiCat) . p1) ^ {} .= {} by D2 ; hence (U1 -multiCat) . p = {} ; ::_thesis: verum end; thus ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) ::_thesis: ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) proof assume E0: ( (U1 -multiCat) . p = {} & p is U1 * -valued ) ; ::_thesis: p is {{}} -valued then reconsider pp = p as U1 * -valued ((n + 1) + 1) + 0 -element FinSequence by D0; reconsider p1 = pp | (Seg (n + 1)) as U1 * -valued n + 1 -element FinSequence ; {(pp . ((n + 1) + 1))} \ (U1 *) = {} ; then reconsider x1 = pp . ((n + 1) + 1) as Element of U1 * by ZFMISC_1:60; Z0: pp \+\ (p1 ^ <*x1*>) = {} ; then pp = p1 ^ <*x1*> by Th29; then ((U1 -multiCat) . p1) ^ x1 = {} by Th33, E0; then ( (U1 -multiCat) . p1 = {} & x1 = e ) ; then ( (U1 -multiCat) . p1 = {} & <*x1*> = <*e*> ) ; then reconsider p11 = p1, x11 = <*x1*> as {{}} -valued FinSequence by D2; p11 ^ x11 is {{}} -valued ; hence p is {{}} -valued by Z0, Th29; ::_thesis: verum end; assume D4: ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} ) ; ::_thesis: (U1 -multiCat) . p = (U2 -multiCat) . p then p in (U1 *) * by B0, FUNCT_1:def_2; then reconsider p1 = p as U1 * -valued ((n + 1) + 1) + 0 -element FinSequence by D0; reconsider q1 = p1 | (Seg (n + 1)) as U1 * -valued n + 1 -element FinSequence ; {(p1 . ((n + 1) + 1))} \ (U1 *) = {} ; then reconsider x1 = p1 . ((n + 1) + 1) as Element of U1 * by ZFMISC_1:60; p in (U2 *) * by D4, B0, FUNCT_1:def_2; then reconsider p2 = p as U2 * -valued ((n + 1) + 1) + 0 -element FinSequence by D0; reconsider q2 = p2 | (Seg (n + 1)) as U2 * -valued n + 1 -element FinSequence ; {(p2 . ((n + 1) + 1))} \ (U2 *) = {} ; then reconsider x2 = p2 . ((n + 1) + 1) as Element of U2 * by ZFMISC_1:60; ( p1 \+\ (q1 ^ <*x1*>) = {} & p2 \+\ (q2 ^ <*x2*>) = {} ) ; then ( p1 = q1 ^ <*x1*> & p2 = q2 ^ <*x2*> ) by Th29; then D1: ( (U1 -multiCat) . p1 = ((U1 -multiCat) . q1) ^ x1 & (U2 -multiCat) . p2 = ((U2 -multiCat) . q2) ^ x2 ) by Th33; assume D3: (U1 -multiCat) . p <> (U2 -multiCat) . p ; ::_thesis: contradiction then ( (U1 -multiCat) . q1 = {} or (U2 -multiCat) . q2 = {} ) by D2, D1; then q1 is {{}} -valued by D2; then ( (U1 -multiCat) . q1 = {} & (U2 -multiCat) . q2 = {} ) by D2; hence contradiction by D3, D1; ::_thesis: verum end; A2: for n being Nat holds S1[n] from NAT_1:sch_2(A0, A1); set C1 = U1 -multiCat ; set C2 = U2 -multiCat ; A10: ( dom (U1 -multiCat) = (U1 *) * & dom (U2 -multiCat) = (U2 *) * ) by FUNCT_2:def_1; hereby ::_thesis: ( ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {} * -valued ) ) assume A12: ( (U1 -multiCat) . x <> {} & (U2 -multiCat) . x <> {} ) ; ::_thesis: (U1 -multiCat) . x = (U2 -multiCat) . x then ( x in (U1 *) * & x <> {} ) by A10, FUNCT_1:def_2; then reconsider p = x as non empty FinSequence ; consider m being Nat such that A11: len p = m + 1 by NAT_1:6; reconsider pp = p as m + 1 -element FinSequence by A11, CARD_1:def_7; ( (U1 -multiCat) . pp <> {} & (U2 -multiCat) . pp <> {} implies (U1 -multiCat) . pp = (U2 -multiCat) . pp ) by A2; hence (U1 -multiCat) . x = (U2 -multiCat) . x by A12; ::_thesis: verum end; hereby ::_thesis: ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {} * -valued ) assume D0: p is {} * -valued ; ::_thesis: (U1 -multiCat) . p = {} percases ( p = {} or not p = {} ) ; suppose p = {} ; ::_thesis: (U1 -multiCat) . p = {} hence (U1 -multiCat) . p = {} ; ::_thesis: verum end; suppose not p = {} ; ::_thesis: (U1 -multiCat) . p = {} then consider m being Nat such that E0: m + 1 = len p by NAT_1:6; reconsider pp = p as m + 1 -element FinSequence by E0, CARD_1:def_7; (U1 -multiCat) . pp = {} by D0, A2; hence (U1 -multiCat) . p = {} ; ::_thesis: verum end; end; end; assume D1: ( (U1 -multiCat) . p = {} & p is U1 * -valued ) ; ::_thesis: p is {} * -valued percases ( p = {} or not p = {} ) ; suppose p = {} ; ::_thesis: p is {} * -valued hence p is {} * -valued ; ::_thesis: verum end; suppose not p = {} ; ::_thesis: p is {} * -valued then consider m being Nat such that E0: m + 1 = len p by NAT_1:6; reconsider pp = p as m + 1 -element FinSequence by E0, CARD_1:def_7; pp is {} * -valued by D1, A2; hence p is {} * -valued ; ::_thesis: verum end; end; end; registration let U be non empty set ; let x be set ; cluster(U -multiCat) . x -> U -valued ; coherence (U -multiCat) . x is U -valued proof (U -multiCat) . x in U * by Th40; hence (U -multiCat) . x is U -valued ; ::_thesis: verum end; end; definition let x be set ; funcx null -> set equals :: FOMODEL0:def 26 x; coherence x is set ; end; :: deftheorem defines null FOMODEL0:def_26_:_ for x being set holds x null = x; registration let Y be with_non-empty_elements set ; cluster Relation-like Y -valued non empty -> non empty-yielding Y -valued for set ; coherence for b1 being Y -valued Relation st not b1 is empty holds not b1 is empty-yielding proof let R be Y -valued Relation; ::_thesis: ( not R is empty implies not R is empty-yielding ) assume not R is empty ; ::_thesis: not R is empty-yielding then reconsider Y0 = rng R as non empty set ; set y = the Element of Y0; now__::_thesis:_not_Y0_c=_{{}} assume Y0 c= {{}} ; ::_thesis: contradiction then ( the Element of Y0 in {{}} & the Element of Y0 in Y ) by TARSKI:def_3; hence contradiction ; ::_thesis: verum end; hence not R is empty-yielding by RELAT_1:def_15; ::_thesis: verum end; end; registration let X be set ; clusterX \ {{}} -> with_non-empty_elements ; coherence X \ {{}} is with_non-empty_elements proof {} in {{}} by TARSKI:def_1; then not {} in X \ {{}} by XBOOLE_0:def_5; hence X \ {{}} is with_non-empty_elements by SETFAM_1:def_8; ::_thesis: verum end; end; registration let X be with_non-empty_elements set ; cluster -> with_non-empty_elements for Element of bool X; coherence for b1 being Subset of X holds b1 is with_non-empty_elements proof let Y be Subset of X; ::_thesis: Y is with_non-empty_elements not {} in Y ; hence Y is with_non-empty_elements by SETFAM_1:def_8; ::_thesis: verum end; end; registration let U be non empty set ; clusterU * -> infinite for set ; coherence for b1 being set st b1 = U * holds not b1 is finite proof omega c= card (U *) by CARD_4:14; hence for b1 being set st b1 = U * holds not b1 is finite ; ::_thesis: verum end; end; registration let U be non empty set ; clusterU * -> with_non-empty_element ; coherence not U * is empty-membered ; end; registration let X be with_non-empty_element set ; cluster non empty with_non-empty_elements for Element of bool X; existence ex b1 being Subset of X st ( b1 is with_non-empty_elements & not b1 is empty ) proof take { the non empty Element of X} ; ::_thesis: ( { the non empty Element of X} is with_non-empty_elements & not { the non empty Element of X} is empty ) thus ( { the non empty Element of X} is with_non-empty_elements & not { the non empty Element of X} is empty ) ; ::_thesis: verum end; end; Lm60: for Y being set for U being non empty set for p being FinSequence st p <> {} & p is Y -valued & Y c= U * & Y is with_non-empty_elements holds (U -multiCat) . p <> {} proof let Y be set ; ::_thesis: for U being non empty set for p being FinSequence st p <> {} & p is Y -valued & Y c= U * & Y is with_non-empty_elements holds (U -multiCat) . p <> {} let U be non empty set ; ::_thesis: for p being FinSequence st p <> {} & p is Y -valued & Y c= U * & Y is with_non-empty_elements holds (U -multiCat) . p <> {} let p be FinSequence; ::_thesis: ( p <> {} & p is Y -valued & Y c= U * & Y is with_non-empty_elements implies (U -multiCat) . p <> {} ) assume p <> {} ; ::_thesis: ( not p is Y -valued or not Y c= U * or not Y is with_non-empty_elements or (U -multiCat) . p <> {} ) then reconsider pp = p as non empty FinSequence ; assume B0: ( p is Y -valued & Y c= U * & Y is with_non-empty_elements ) ; ::_thesis: (U -multiCat) . p <> {} then ( rng pp c= Y & Y c= U * ) by RELAT_1:def_19; then reconsider YY = Y as non empty with_non-empty_elements Subset of (U *) by B0; reconsider pp = pp as YY -valued non empty FinSequence by B0; ( pp is U * -valued & not pp is {} * -valued ) ; hence (U -multiCat) . p <> {} by Th52; ::_thesis: verum end; theorem :: FOMODEL0:53 for Y being set for U1, U2 being non empty set for p being FinSequence st U1 c= U2 & Y c= U1 * & p is Y -valued & p <> {} & Y is with_non-empty_elements holds (U1 -multiCat) . p = (U2 -multiCat) . p proof let Y be set ; ::_thesis: for U1, U2 being non empty set for p being FinSequence st U1 c= U2 & Y c= U1 * & p is Y -valued & p <> {} & Y is with_non-empty_elements holds (U1 -multiCat) . p = (U2 -multiCat) . p let U1, U2 be non empty set ; ::_thesis: for p being FinSequence st U1 c= U2 & Y c= U1 * & p is Y -valued & p <> {} & Y is with_non-empty_elements holds (U1 -multiCat) . p = (U2 -multiCat) . p let p be FinSequence; ::_thesis: ( U1 c= U2 & Y c= U1 * & p is Y -valued & p <> {} & Y is with_non-empty_elements implies (U1 -multiCat) . p = (U2 -multiCat) . p ) assume U1 c= U2 ; ::_thesis: ( not Y c= U1 * or not p is Y -valued or not p <> {} or not Y is with_non-empty_elements or (U1 -multiCat) . p = (U2 -multiCat) . p ) then reconsider U11 = U1 as non empty Subset of U2 ; assume Y c= U1 * ; ::_thesis: ( not p is Y -valued or not p <> {} or not Y is with_non-empty_elements or (U1 -multiCat) . p = (U2 -multiCat) . p ) then reconsider Y1 = Y as Subset of (U11 *) ; reconsider Y2 = Y1 as Subset of (U2 *) by XBOOLE_1:1; assume p is Y -valued ; ::_thesis: ( not p <> {} or not Y is with_non-empty_elements or (U1 -multiCat) . p = (U2 -multiCat) . p ) then reconsider p1 = p as Y1 -valued FinSequence ; reconsider p2 = p1 as Y2 -valued FinSequence ; assume ( p <> {} & Y is with_non-empty_elements ) ; ::_thesis: (U1 -multiCat) . p = (U2 -multiCat) . p then ( (U1 -multiCat) . p1 <> {} & (U2 -multiCat) . p2 <> {} ) by Lm60; hence (U1 -multiCat) . p = (U2 -multiCat) . p by Th52; ::_thesis: verum end; theorem :: FOMODEL0:54 for x, X being set for U being non empty set st ex p being FinSequence st ( x = p & p is X * -valued ) holds (U -multiCat) . x is X -valued proof let x, X be set ; ::_thesis: for U being non empty set st ex p being FinSequence st ( x = p & p is X * -valued ) holds (U -multiCat) . x is X -valued let U be non empty set ; ::_thesis: ( ex p being FinSequence st ( x = p & p is X * -valued ) implies (U -multiCat) . x is X -valued ) set C = U -multiCat ; B1: dom (U -multiCat) = (U *) * by FUNCT_2:def_1; given p being FinSequence such that B0: ( x = p & p is X * -valued ) ; ::_thesis: (U -multiCat) . x is X -valued x is FinSequence of X * by B0, Lm45; then reconsider px = x as Element of (X *) * by FINSEQ_1:def_11; percases ( (U -multiCat) . p <> {} or (U -multiCat) . p = {} ) ; supposeC1: (U -multiCat) . p <> {} ; ::_thesis: (U -multiCat) . x is X -valued then ( p in (U *) * & p <> {} ) by B1, FUNCT_1:def_2; then reconsider pp = x as non empty FinSequence of U * by Lm45, B0; C0: ( pp is X * -valued & not pp is {} * -valued ) by Th52, B0, C1; reconsider XX = X as non empty set by Th52, B0, C1; set CX = XX -multiCat ; reconsider pxx = px as Element of (XX *) * ; (XX -multiCat) . pp <> {} by Th52, C0; hence (U -multiCat) . x is X -valued by Th52, C1, B0; ::_thesis: verum end; suppose (U -multiCat) . p = {} ; ::_thesis: (U -multiCat) . x is X -valued then reconsider e = (U -multiCat) . p as empty set ; rng e c= X by XBOOLE_1:2; hence (U -multiCat) . x is X -valued by B0, RELAT_1:def_19; ::_thesis: verum end; end; end; registration let X be set ; let m be Nat; cluster(m -tuples_on X) \ (X *) -> empty for set ; coherence for b1 being set st b1 = (m -tuples_on X) \ (X *) holds b1 is empty proof reconsider mm = m as Element of NAT by ORDINAL1:def_12; mm -tuples_on X c= X * by FINSEQ_2:134; hence for b1 being set st b1 = (m -tuples_on X) \ (X *) holds b1 is empty ; ::_thesis: verum end; end; theorem :: FOMODEL0:55 for A, B being set holds (A /\ B) * = (A *) /\ (B *) proof let A, B be set ; ::_thesis: (A /\ B) * = (A *) /\ (B *) set X = A /\ B; reconsider XA = A /\ B as Subset of A ; reconsider XB = A /\ B as Subset of B ; ( XA * c= A * & XB * c= B * ) ; then B0: (A /\ B) * c= (A *) /\ (B *) by XBOOLE_1:19; now__::_thesis:_for_x_being_set_st_x_in_(A_*)_/\_(B_*)_holds_ x_in_(A_/\_B)_* let x be set ; ::_thesis: ( x in (A *) /\ (B *) implies x in (A /\ B) * ) assume C0: x in (A *) /\ (B *) ; ::_thesis: x in (A /\ B) * reconsider pa = x as A -valued FinSequence by C0; set m = len pa; set mA = (len pa) -tuples_on A; set mB = (len pa) -tuples_on B; set mX = (len pa) -tuples_on (A /\ B); ((len pa) -tuples_on (A /\ B)) \ ((A /\ B) *) = {} ; then C1: (len pa) -tuples_on (A /\ B) c= (A /\ B) * by XBOOLE_1:37; reconsider pb = x as B -valued FinSequence by C0; ( pa is len pa -element & pb is len pa -element ) by CARD_1:def_7; then ( pa in (len pa) -tuples_on A & pb in (len pa) -tuples_on B ) by Th16; then pa in ((len pa) -tuples_on A) /\ ((len pa) -tuples_on B) by XBOOLE_0:def_4; then pa in (len pa) -tuples_on (A /\ B) by Lm24; hence x in (A /\ B) * by C1; ::_thesis: verum end; then (A *) /\ (B *) c= (A /\ B) * by TARSKI:def_3; hence (A /\ B) * = (A *) /\ (B *) by B0, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: FOMODEL0:56 for X being set for P, Q being Relation holds (P \/ Q) | X = (P | X) \/ (Q | X) proof let X be set ; ::_thesis: for P, Q being Relation holds (P \/ Q) | X = (P | X) \/ (Q | X) let P, Q be Relation; ::_thesis: (P \/ Q) | X = (P | X) \/ (Q | X) set R1 = P | X; set R2 = Q | X; set R = P \/ Q; set LH = (P \/ Q) | X; set RH = (P | X) \/ (Q | X); ( (P null Q) | X c= (P \/ Q) | X & (Q null P) | X c= (P \/ Q) | X ) by RELAT_1:76; then B0: (P | X) \/ (Q | X) c= (P \/ Q) | X by XBOOLE_1:8; now__::_thesis:_for_z_being_set_st_z_in_(P_\/_Q)_|_X_holds_ z_in_(P_|_X)_\/_(Q_|_X) let z be set ; ::_thesis: ( z in (P \/ Q) | X implies z in (P | X) \/ (Q | X) ) assume C1: z in (P \/ Q) | X ; ::_thesis: z in (P | X) \/ (Q | X) then consider x, y being set such that C2: z = [x,y] by RELAT_1:def_1; C0: ( x in X & [x,y] in P \/ Q ) by C1, C2, RELAT_1:def_11; ( ( x in X & [x,y] in P ) or ( x in X & [x,y] in Q ) ) by C0, XBOOLE_0:def_3; then ( [x,y] in P | X or [x,y] in Q | X ) by RELAT_1:def_11; hence z in (P | X) \/ (Q | X) by C2, XBOOLE_0:def_3; ::_thesis: verum end; then (P \/ Q) | X c= (P | X) \/ (Q | X) by TARSKI:def_3; hence (P \/ Q) | X = (P | X) \/ (Q | X) by B0, XBOOLE_0:def_10; ::_thesis: verum end; registration let X be set ; cluster(bool X) \ X -> non empty for set ; coherence for b1 being set st b1 = (bool X) \ X holds not b1 is empty proof not bool X c= X by CARD_1:25; hence for b1 being set st b1 = (bool X) \ X holds not b1 is empty by XBOOLE_1:37; ::_thesis: verum end; end; registration let X be set ; let R be Relation; clusterR null X -> X \/ (dom R) -defined for Relation; coherence for b1 being Relation st b1 = R null X holds b1 is X \/ (dom R) -defined proof (dom R) null X c= (dom R) \/ X ; hence for b1 being Relation st b1 = R null X holds b1 is X \/ (dom R) -defined by RELAT_1:def_18; ::_thesis: verum end; end; theorem :: FOMODEL0:57 for X being set for f, g being Function holds (f | X) +* g = (f | (X \ (dom g))) \/ g proof let X be set ; ::_thesis: for f, g being Function holds (f | X) +* g = (f | (X \ (dom g))) \/ g let f, g be Function; ::_thesis: (f | X) +* g = (f | (X \ (dom g))) \/ g set f1 = f | (X \ (dom g)); set a1 = g; ( dom (f | (X \ (dom g))) c= X \ (dom g) & X \ (dom g) misses dom g ) by XBOOLE_1:79; then B0: f | (X \ (dom g)) tolerates g by PARTFUN1:56, XBOOLE_1:63; (f | X) +* g = (f | ((X \ (dom g)) \/ (X /\ (dom g)))) +* g by Th48 .= ((f | (X \ (dom g))) +* (f | (X /\ (dom g)))) +* g by FUNCT_4:78 .= (f | (X \ (dom g))) +* ((f | (X /\ (dom g))) +* ((g null {}) null ({} \/ (dom g)))) by FUNCT_4:14 .= (f | (X \ (dom g))) +* (((f | X) | (dom g)) +* (g | (dom g))) by RELAT_1:71 .= (f | (X \ (dom g))) +* (((f | X) +* g) | (dom g)) by FUNCT_4:71 .= (f | (X \ (dom g))) +* g by FUNCT_4:23 .= (f | (X \ (dom g))) \/ g by B0, FUNCT_4:30 ; hence (f | X) +* g = (f | (X \ (dom g))) \/ g ; ::_thesis: verum end; registration let X be set ; let f be X -defined Function; let g be X -defined total Function; identifyf +* g with g null f; compatibility f +* g = g null f proof ( dom g = X & dom f c= X ) by PARTFUN1:def_2; hence f +* g = g null f by FUNCT_4:19; ::_thesis: verum end; identifyg null f with f +* g; compatibility g null f = f +* g ; end; theorem Th58: :: FOMODEL0:58 for y, X, A being set st not y in proj2 X holds [:A,{y}:] misses X proof let y, X, A be set ; ::_thesis: ( not y in proj2 X implies [:A,{y}:] misses X ) set X2 = proj2 X; set Y = [:A,{y}:]; set Z = X /\ [:A,{y}:]; assume B0: not y in proj2 X ; ::_thesis: [:A,{y}:] misses X assume [:A,{y}:] meets X ; ::_thesis: contradiction then X /\ [:A,{y}:] <> {} by XBOOLE_0:def_7; then consider z being set such that B1: z in X /\ [:A,{y}:] by XBOOLE_0:def_1; set x1 = z `1 ; set y1 = z `2 ; ( z `1 in A & z `2 in {y} & z = [(z `1),(z `2)] & z in X ) by B1, MCART_1:10, MCART_1:21; then ( z `2 = y & z `2 in proj2 X ) by TARSKI:def_1, XTUPLE_0:def_13; hence contradiction by B0; ::_thesis: verum end; definition let X be set ; funcX -freeCountableSet -> set equals :: FOMODEL0:def 27 [:NAT,{ the Element of (bool (proj2 X)) \ (proj2 X)}:]; coherence [:NAT,{ the Element of (bool (proj2 X)) \ (proj2 X)}:] is set ; end; :: deftheorem defines -freeCountableSet FOMODEL0:def_27_:_ for X being set holds X -freeCountableSet = [:NAT,{ the Element of (bool (proj2 X)) \ (proj2 X)}:]; theorem Th59: :: FOMODEL0:59 for X being set holds ( (X -freeCountableSet) /\ X = {} & X -freeCountableSet is infinite ) proof let X be set ; ::_thesis: ( (X -freeCountableSet) /\ X = {} & X -freeCountableSet is infinite ) set X2 = proj2 X; set Y = (bool (proj2 X)) \ (proj2 X); set y = the Element of (bool (proj2 X)) \ (proj2 X); set IT = X -freeCountableSet ; not the Element of (bool (proj2 X)) \ (proj2 X) in proj2 X by XBOOLE_0:def_5; then X -freeCountableSet misses X by Th58; hence (X -freeCountableSet) /\ X = {} by XBOOLE_0:def_7; ::_thesis: X -freeCountableSet is infinite thus X -freeCountableSet is infinite ; ::_thesis: verum end; registration let X be set ; clusterX -freeCountableSet -> infinite for set ; coherence for b1 being set st b1 = X -freeCountableSet holds not b1 is finite ; end; registration let X be set ; cluster(X -freeCountableSet) /\ X -> empty ; coherence (X -freeCountableSet) /\ X is empty by Th59; end; registration let X be set ; clusterX -freeCountableSet -> countable for set ; coherence for b1 being set st b1 = X -freeCountableSet holds b1 is countable by CARD_4:7; end; registration clusterNAT \ INT -> empty ; coherence NAT \ INT is empty by NUMBERS:17; end; registration let x be set ; let p be FinSequence; cluster((<*x*> ^ p) . 1) \+\ x -> empty for set ; coherence for b1 being set st b1 = ((<*x*> ^ p) . 1) \+\ x holds b1 is empty proof (<*x*> ^ p) . 1 = x by FINSEQ_1:41; hence for b1 being set st b1 = ((<*x*> ^ p) . 1) \+\ x holds b1 is empty ; ::_thesis: verum end; end; registration let m be Nat; let m0 be zero number ; let p be m -element FinSequence; clusterp null m0 -> Seg (m + m0) -defined total for Seg (m + m0) -defined Relation; coherence for b1 being Seg (m + m0) -defined Relation st b1 = p null m0 holds b1 is total proof let q be Seg (m + m0) -defined Relation; ::_thesis: ( q = p null m0 implies q is total ) assume q = p null m0 ; ::_thesis: q is total then dom q = Seg (m + m0) by FINSEQ_1:89; hence q is total by PARTFUN1:def_2; ::_thesis: verum end; end; registration let U be non empty set ; let q1, q2 be U -valued FinSequence; cluster((U -multiCat) . <*q1,q2*>) \+\ (q1 ^ q2) -> empty for set ; coherence for b1 being set st b1 = ((U -multiCat) . <*q1,q2*>) \+\ (q1 ^ q2) holds b1 is empty proof reconsider f = U -concatenation as BinOp of (U *) ; q1 is FinSequence of U by Lm45; then reconsider q11 = q1 as Element of U * by FINSEQ_1:def_11; set F = MultPlace f; set p = <*q11*>; set C = U -multiCat ; (U -multiCat) . <*q1,q2*> = ((U -multiCat) . <*q11*>) ^ q2 by Th33 .= ((MultPlace f) . <*q11*>) ^ q2 by Th32 .= q1 ^ q2 by LmMultPlace ; hence for b1 being set st b1 = ((U -multiCat) . <*q1,q2*>) \+\ (q1 ^ q2) holds b1 is empty ; ::_thesis: verum end; end;