:: MARGREL1 semantic presentation begin definition let B be non empty set ; let A be set ; let b be Element of B; :: original: --> redefine funcA --> b -> Function of A,B; coherence A --> b is Function of A,B proof set f = A --> b; A1: dom (A --> b) = A by FUNCOP_1:13; thus A --> b is Function of A,B by A1; ::_thesis: verum end; end; definition let IT be FinSequence-membered set ; redefine attr IT is with_common_domain means :Def1: :: MARGREL1:def 1 for a, b being FinSequence st a in IT & b in IT holds len a = len b; compatibility ( IT is with_common_domain iff for a, b being FinSequence st a in IT & b in IT holds len a = len b ) proof thus ( IT is with_common_domain implies for a, b being FinSequence st a in IT & b in IT holds len a = len b ) ::_thesis: ( ( for a, b being FinSequence st a in IT & b in IT holds len a = len b ) implies IT is with_common_domain ) proof assume A1: IT is with_common_domain ; ::_thesis: for a, b being FinSequence st a in IT & b in IT holds len a = len b let a, b be FinSequence; ::_thesis: ( a in IT & b in IT implies len a = len b ) assume ( a in IT & b in IT ) ; ::_thesis: len a = len b then dom a = dom b by A1, CARD_3:def_10; hence len a = len b by FINSEQ_3:29; ::_thesis: verum end; assume A2: for a, b being FinSequence st a in IT & b in IT holds len a = len b ; ::_thesis: IT is with_common_domain let f, g be Function; :: according to CARD_3:def_10 ::_thesis: ( not f in IT or not g in IT or dom f = dom g ) assume A3: ( f in IT & g in IT ) ; ::_thesis: dom f = dom g then reconsider f = f, g = g as FinSequence ; len f = len g by A2, A3; hence dom f = dom g by FINSEQ_3:29; ::_thesis: verum end; end; :: deftheorem Def1 defines with_common_domain MARGREL1:def_1_:_ for IT being FinSequence-membered set holds ( IT is with_common_domain iff for a, b being FinSequence st a in IT & b in IT holds len a = len b ); registration cluster FinSequence-membered with_common_domain for set ; existence ex b1 being set st ( b1 is FinSequence-membered & b1 is with_common_domain ) proof take {} ; ::_thesis: ( {} is FinSequence-membered & {} is with_common_domain ) thus ( ( for x being set st x in {} holds x is FinSequence ) & ( for a, b being FinSequence st a in {} & b in {} holds len a = len b ) ) ; :: according to FINSEQ_1:def_18,MARGREL1:def_1 ::_thesis: verum end; end; definition mode relation is FinSequence-membered with_common_domain set ; end; theorem :: MARGREL1:1 for X being set for p being relation st X c= p holds X is relation ; theorem :: MARGREL1:2 for a being FinSequence holds {a} is relation proof let a be FinSequence; ::_thesis: {a} is relation for z being set st z in {a} holds z is FinSequence by TARSKI:def_1; then reconsider X = {a} as FinSequence-membered set by FINSEQ_1:def_18; X is with_common_domain ; hence {a} is relation ; ::_thesis: verum end; scheme :: MARGREL1:sch 1 relexist{ F1() -> set , P1[ FinSequence] } : ex r being relation st for a being FinSequence holds ( a in r iff ( a in F1() & P1[a] ) ) provided A1: for a, b being FinSequence st P1[a] & P1[b] holds len a = len b proof defpred S1[ set ] means ex a being FinSequence st ( P1[a] & \$1 = a ); consider X being set such that A2: for x being set holds ( x in X iff ( x in F1() & S1[x] ) ) from XBOOLE_0:sch_1(); X is FinSequence-membered proof let x be set ; :: according to FINSEQ_1:def_18 ::_thesis: ( not x in X or x is set ) assume x in X ; ::_thesis: x is set then ex a being FinSequence st ( P1[a] & x = a ) by A2; hence x is set ; ::_thesis: verum end; then reconsider X = X as FinSequence-membered set ; X is with_common_domain proof let a be FinSequence; :: according to MARGREL1:def_1 ::_thesis: for b being FinSequence st a in X & b in X holds len a = len b let b be FinSequence; ::_thesis: ( a in X & b in X implies len a = len b ) assume that A3: a in X and A4: b in X ; ::_thesis: len a = len b A5: ex d being FinSequence st ( P1[d] & b = d ) by A2, A4; ex c being FinSequence st ( P1[c] & a = c ) by A2, A3; hence len a = len b by A1, A5; ::_thesis: verum end; then reconsider r = X as relation ; for a being FinSequence holds ( a in r iff ( a in F1() & P1[a] ) ) proof let a be FinSequence; ::_thesis: ( a in r iff ( a in F1() & P1[a] ) ) now__::_thesis:_(_a_in_r_implies_(_a_in_F1()_&_P1[a]_)_) assume A6: a in r ; ::_thesis: ( a in F1() & P1[a] ) then ex c being FinSequence st ( P1[c] & a = c ) by A2; hence ( a in F1() & P1[a] ) by A2, A6; ::_thesis: verum end; hence ( a in r iff ( a in F1() & P1[a] ) ) by A2; ::_thesis: verum end; hence ex r being relation st for a being FinSequence holds ( a in r iff ( a in F1() & P1[a] ) ) ; ::_thesis: verum end; definition let p, r be relation; redefine pred p = r means :: MARGREL1:def 2 for a being FinSequence holds ( a in p iff a in r ); compatibility ( p = r iff for a being FinSequence holds ( a in p iff a in r ) ) proof thus ( p = r implies for a being FinSequence holds ( a in p iff a in r ) ) ; ::_thesis: ( ( for a being FinSequence holds ( a in p iff a in r ) ) implies p = r ) thus ( ( for a being FinSequence holds ( a in p iff a in r ) ) implies p = r ) ::_thesis: verum proof assume for a being FinSequence holds ( a in p iff a in r ) ; ::_thesis: p = r then for x being set holds ( x in p iff x in r ) ; hence p = r by TARSKI:1; ::_thesis: verum end; end; end; :: deftheorem defines = MARGREL1:def_2_:_ for p, r being relation holds ( p = r iff for a being FinSequence holds ( a in p iff a in r ) ); registration cluster empty -> with_common_domain for set ; coherence for b1 being set st b1 is empty holds b1 is with_common_domain proof let X be set ; ::_thesis: ( X is empty implies X is with_common_domain ) assume A1: X is empty ; ::_thesis: X is with_common_domain then for a, b being FinSequence st a in X & b in X holds len a = len b ; hence X is with_common_domain by Def1, A1; ::_thesis: verum end; end; theorem Th3: :: MARGREL1:3 for p being relation st ( for a being FinSequence holds not a in p ) holds p = {} proof let p be relation; ::_thesis: ( ( for a being FinSequence holds not a in p ) implies p = {} ) assume A1: for a being FinSequence holds not a in p ; ::_thesis: p = {} assume p <> {} ; ::_thesis: contradiction then ex x being set st x in p by XBOOLE_0:def_1; hence contradiction by A1; ::_thesis: verum end; definition let p be relation; assume A1: p <> {} ; func the_arity_of p -> Element of NAT means :: MARGREL1:def 3 for a being FinSequence st a in p holds it = len a; existence ex b1 being Element of NAT st for a being FinSequence st a in p holds b1 = len a proof consider c being FinSequence such that A2: c in p by A1, Th3; for a being FinSequence st a in p holds len c = len a by A2, Def1; hence ex b1 being Element of NAT st for a being FinSequence st a in p holds b1 = len a ; ::_thesis: verum end; uniqueness for b1, b2 being Element of NAT st ( for a being FinSequence st a in p holds b1 = len a ) & ( for a being FinSequence st a in p holds b2 = len a ) holds b1 = b2 proof let n1, n2 be Element of NAT ; ::_thesis: ( ( for a being FinSequence st a in p holds n1 = len a ) & ( for a being FinSequence st a in p holds n2 = len a ) implies n1 = n2 ) assume that A3: for a being FinSequence st a in p holds n1 = len a and A4: for a being FinSequence st a in p holds n2 = len a ; ::_thesis: n1 = n2 consider a being FinSequence such that A5: a in p by A1, Th3; len a = n1 by A3, A5; hence n1 = n2 by A4, A5; ::_thesis: verum end; end; :: deftheorem defines the_arity_of MARGREL1:def_3_:_ for p being relation st p <> {} holds for b2 being Element of NAT holds ( b2 = the_arity_of p iff for a being FinSequence st a in p holds b2 = len a ); definition let k be Element of NAT ; mode relation_length of k -> relation means :: MARGREL1:def 4 for a being FinSequence st a in it holds len a = k; existence ex b1 being relation st for a being FinSequence st a in b1 holds len a = k proof take {} ; ::_thesis: for a being FinSequence st a in {} holds len a = k thus for a being FinSequence st a in {} holds len a = k ; ::_thesis: verum end; end; :: deftheorem defines relation_length MARGREL1:def_4_:_ for k being Element of NAT for b2 being relation holds ( b2 is relation_length of k iff for a being FinSequence st a in b2 holds len a = k ); definition let X be set ; mode relation of X -> relation means :: MARGREL1:def 5 for a being FinSequence st a in it holds rng a c= X; existence ex b1 being relation st for a being FinSequence st a in b1 holds rng a c= X proof take {} ; ::_thesis: for a being FinSequence st a in {} holds rng a c= X thus for a being FinSequence st a in {} holds rng a c= X ; ::_thesis: verum end; end; :: deftheorem defines relation MARGREL1:def_5_:_ for X being set for b2 being relation holds ( b2 is relation of X iff for a being FinSequence st a in b2 holds rng a c= X ); theorem Th4: :: MARGREL1:4 for X being set holds {} is relation of X proof let X be set ; ::_thesis: {} is relation of X thus for a being FinSequence st a in {} holds rng a c= X ; :: according to MARGREL1:def_5 ::_thesis: verum end; theorem Th5: :: MARGREL1:5 for k being Element of NAT holds {} is relation_length of k proof let k be Element of NAT ; ::_thesis: {} is relation_length of k thus for a being FinSequence st a in {} holds len a = k ; :: according to MARGREL1:def_4 ::_thesis: verum end; definition let X be set ; let k be Element of NAT ; mode relation of X,k -> relation means :: MARGREL1:def 6 ( it is relation of X & it is relation_length of k ); existence ex b1 being relation st ( b1 is relation of X & b1 is relation_length of k ) proof take {} ; ::_thesis: ( {} is relation of X & {} is relation_length of k ) thus ( {} is relation of X & {} is relation_length of k ) by Th4, Th5; ::_thesis: verum end; end; :: deftheorem defines relation MARGREL1:def_6_:_ for X being set for k being Element of NAT for b3 being relation holds ( b3 is relation of X,k iff ( b3 is relation of X & b3 is relation_length of k ) ); definition let D be non empty set ; func relations_on D -> set means :Def7: :: MARGREL1:def 7 for X being set holds ( X in it iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) ); existence ex b1 being set st for X being set holds ( X in b1 iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) ) proof defpred S1[ set ] means ex Y being set st ( Y = \$1 & Y c= D * & ( for a, b being FinSequence of D st a in Y & b in Y holds len a = len b ) ); consider A being set such that A1: for x being set holds ( x in A iff ( x in bool (D *) & S1[x] ) ) from XBOOLE_0:sch_1(); take A ; ::_thesis: for X being set holds ( X in A iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) ) for X being set holds ( X in A iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) ) proof let X be set ; ::_thesis: ( X in A iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) ) thus ( X in A implies ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) ) ::_thesis: ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) implies X in A ) proof assume X in A ; ::_thesis: ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) then ex Y being set st ( Y = X & Y c= D * & ( for a, b being FinSequence of D st a in Y & b in Y holds len a = len b ) ) by A1; hence ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) ; ::_thesis: verum end; thus ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) implies X in A ) by A1; ::_thesis: verum end; hence for X being set holds ( X in A iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for X being set holds ( X in b1 iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) ) ) & ( for X being set holds ( X in b2 iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) ) ) holds b1 = b2 proof let A1, A2 be set ; ::_thesis: ( ( for X being set holds ( X in A1 iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) ) ) & ( for X being set holds ( X in A2 iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) ) ) implies A1 = A2 ) assume that A2: for X being set holds ( X in A1 iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) ) and A3: for X being set holds ( X in A2 iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) ) ; ::_thesis: A1 = A2 for x being set holds ( x in A1 iff x in A2 ) proof let x be set ; ::_thesis: ( x in A1 iff x in A2 ) thus ( x in A1 implies x in A2 ) ::_thesis: ( x in A2 implies x in A1 ) proof assume A4: x in A1 ; ::_thesis: x in A2 then A5: for a, b being FinSequence of D st a in x & b in x holds len a = len b by A2; x c= D * by A2, A4; hence x in A2 by A3, A5; ::_thesis: verum end; thus ( x in A2 implies x in A1 ) ::_thesis: verum proof assume A6: x in A2 ; ::_thesis: x in A1 then A7: for a, b being FinSequence of D st a in x & b in x holds len a = len b by A3; x c= D * by A3, A6; hence x in A1 by A2, A7; ::_thesis: verum end; end; hence A1 = A2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def7 defines relations_on MARGREL1:def_7_:_ for D being non empty set for b2 being set holds ( b2 = relations_on D iff for X being set holds ( X in b2 iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) ) ); registration let D be non empty set ; cluster relations_on D -> non empty ; coherence not relations_on D is empty proof A1: for a, b being FinSequence of D st a in {} & b in {} holds len a = len b ; defpred S1[ set ] means ex Y being set st ( Y = D & Y c= D * & ( for a, b being FinSequence of D st a in Y & b in Y holds len a = len b ) ); consider XX being set such that A2: for x being set holds ( x in XX iff ( x in bool (D *) & S1[x] ) ) from XBOOLE_0:sch_1(); {} c= D * by XBOOLE_1:2; then reconsider A = XX as non empty set by A2, A1; for X being set holds ( X in A iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) ) proof let X be set ; ::_thesis: ( X in A iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) ) thus ( X in A implies ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) ) ::_thesis: ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) implies X in A ) proof assume X in A ; ::_thesis: ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) then ex Y being set st ( Y = X & Y c= D * & ( for a, b being FinSequence of D st a in Y & b in Y holds len a = len b ) ) by A2; hence ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) ) ; ::_thesis: verum end; thus ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds len a = len b ) implies X in A ) by A2; ::_thesis: verum end; hence not relations_on D is empty by Def7; ::_thesis: verum end; end; definition let D be non empty set ; mode relation of D is Element of relations_on D; end; theorem :: MARGREL1:6 for D being non empty set for X being set for r being Element of relations_on D st X c= r holds X is Element of relations_on D proof let D be non empty set ; ::_thesis: for X being set for r being Element of relations_on D st X c= r holds X is Element of relations_on D let X be set ; ::_thesis: for r being Element of relations_on D st X c= r holds X is Element of relations_on D let r be Element of relations_on D; ::_thesis: ( X c= r implies X is Element of relations_on D ) assume A1: X c= r ; ::_thesis: X is Element of relations_on D then A2: for a, b being FinSequence of D st a in X & b in X holds len a = len b by Def7; r c= D * by Def7; then X c= D * by A1, XBOOLE_1:1; hence X is Element of relations_on D by A2, Def7; ::_thesis: verum end; theorem :: MARGREL1:7 for D being non empty set for a being FinSequence of D holds {a} is Element of relations_on D proof let D be non empty set ; ::_thesis: for a being FinSequence of D holds {a} is Element of relations_on D let a be FinSequence of D; ::_thesis: {a} is Element of relations_on D A1: for a1, a2 being FinSequence of D st a1 in {a} & a2 in {a} holds len a1 = len a2 proof let a1, a2 be FinSequence of D; ::_thesis: ( a1 in {a} & a2 in {a} implies len a1 = len a2 ) assume that A2: a1 in {a} and A3: a2 in {a} ; ::_thesis: len a1 = len a2 a1 = a by A2, TARSKI:def_1; hence len a1 = len a2 by A3, TARSKI:def_1; ::_thesis: verum end; a in D * by FINSEQ_1:def_11; then {a} c= D * by ZFMISC_1:31; hence {a} is Element of relations_on D by A1, Def7; ::_thesis: verum end; theorem :: MARGREL1:8 for D being non empty set for x, y being Element of D holds {<*x,y*>} is Element of relations_on D proof let D be non empty set ; ::_thesis: for x, y being Element of D holds {<*x,y*>} is Element of relations_on D let x, y be Element of D; ::_thesis: {<*x,y*>} is Element of relations_on D A1: for a1, a2 being FinSequence of D st a1 in {<*x,y*>} & a2 in {<*x,y*>} holds len a1 = len a2 proof let a1, a2 be FinSequence of D; ::_thesis: ( a1 in {<*x,y*>} & a2 in {<*x,y*>} implies len a1 = len a2 ) assume that A2: a1 in {<*x,y*>} and A3: a2 in {<*x,y*>} ; ::_thesis: len a1 = len a2 a1 = <*x,y*> by A2, TARSKI:def_1; hence len a1 = len a2 by A3, TARSKI:def_1; ::_thesis: verum end; <*x*> ^ <*y*> is FinSequence of D ; then <*x,y*> in D * by FINSEQ_1:def_11; then {<*x,y*>} c= D * by ZFMISC_1:31; hence {<*x,y*>} is Element of relations_on D by A1, Def7; ::_thesis: verum end; definition let D be non empty set ; let p, r be Element of relations_on D; :: original: = redefine predp = r means :Def8: :: MARGREL1:def 8 for a being FinSequence of D holds ( a in p iff a in r ); compatibility ( p = r iff for a being FinSequence of D holds ( a in p iff a in r ) ) proof thus ( p = r implies for a being FinSequence of D holds ( a in p iff a in r ) ) ; ::_thesis: ( ( for a being FinSequence of D holds ( a in p iff a in r ) ) implies p = r ) thus ( ( for a being FinSequence of D holds ( a in p iff a in r ) ) implies p = r ) ::_thesis: verum proof assume A1: for a being FinSequence of D holds ( a in p iff a in r ) ; ::_thesis: p = r now__::_thesis:_for_x_being_set_holds_ (_x_in_p_iff_x_in_r_) let x be set ; ::_thesis: ( x in p iff x in r ) A2: now__::_thesis:_(_x_in_r_implies_x_in_p_) assume A3: x in r ; ::_thesis: x in p r is Subset of (D *) by Def7; then x is FinSequence of D by A3, FINSEQ_1:def_11; hence x in p by A1, A3; ::_thesis: verum end; now__::_thesis:_(_x_in_p_implies_x_in_r_) assume A4: x in p ; ::_thesis: x in r p is Subset of (D *) by Def7; then x is FinSequence of D by A4, FINSEQ_1:def_11; hence x in r by A1, A4; ::_thesis: verum end; hence ( x in p iff x in r ) by A2; ::_thesis: verum end; hence p = r by TARSKI:1; ::_thesis: verum end; end; end; :: deftheorem Def8 defines = MARGREL1:def_8_:_ for D being non empty set for p, r being Element of relations_on D holds ( p = r iff for a being FinSequence of D holds ( a in p iff a in r ) ); scheme :: MARGREL1:sch 2 relDexist{ F1() -> non empty set , P1[ FinSequence of F1()] } : ex r being Element of relations_on F1() st for a being FinSequence of F1() holds ( a in r iff P1[a] ) provided A1: for a, b being FinSequence of F1() st P1[a] & P1[b] holds len a = len b proof defpred S1[ set ] means ex a being FinSequence of F1() st ( P1[a] & \$1 = a ); consider X being set such that A2: for x being set holds ( x in X iff ( x in F1() * & S1[x] ) ) from XBOOLE_0:sch_1(); A3: for a, b being FinSequence of F1() st a in X & b in X holds len a = len b proof let a, b be FinSequence of F1(); ::_thesis: ( a in X & b in X implies len a = len b ) assume that A4: a in X and A5: b in X ; ::_thesis: len a = len b A6: ex d being FinSequence of F1() st ( P1[d] & b = d ) by A2, A5; ex c being FinSequence of F1() st ( P1[c] & a = c ) by A2, A4; hence len a = len b by A1, A6; ::_thesis: verum end; for x being set st x in X holds x in F1() * by A2; then X c= F1() * by TARSKI:def_3; then reconsider r = X as Element of relations_on F1() by A3, Def7; for a being FinSequence of F1() holds ( a in r iff P1[a] ) proof let a be FinSequence of F1(); ::_thesis: ( a in r iff P1[a] ) A7: now__::_thesis:_(_P1[a]_implies_a_in_r_) A8: a in F1() * by FINSEQ_1:def_11; assume P1[a] ; ::_thesis: a in r hence a in r by A2, A8; ::_thesis: verum end; now__::_thesis:_(_a_in_r_implies_P1[a]_) assume a in r ; ::_thesis: P1[a] then ex c being FinSequence of F1() st ( P1[c] & a = c ) by A2; hence P1[a] ; ::_thesis: verum end; hence ( a in r iff P1[a] ) by A7; ::_thesis: verum end; hence ex r being Element of relations_on F1() st for a being FinSequence of F1() holds ( a in r iff P1[a] ) ; ::_thesis: verum end; definition let D be non empty set ; func empty_rel D -> Element of relations_on D means :Def9: :: MARGREL1:def 9 for a being FinSequence of D holds not a in it; existence ex b1 being Element of relations_on D st for a being FinSequence of D holds not a in b1 proof defpred S1[ FinSequence of D] means contradiction; A1: for a, b being FinSequence of D st S1[a] & S1[b] holds len a = len b ; consider r being Element of relations_on D such that A2: for a being FinSequence of D holds ( a in r iff S1[a] ) from MARGREL1:sch_2(A1); take r ; ::_thesis: for a being FinSequence of D holds not a in r thus for a being FinSequence of D holds not a in r by A2; ::_thesis: verum end; uniqueness for b1, b2 being Element of relations_on D st ( for a being FinSequence of D holds not a in b1 ) & ( for a being FinSequence of D holds not a in b2 ) holds b1 = b2 proof let r1, r2 be Element of relations_on D; ::_thesis: ( ( for a being FinSequence of D holds not a in r1 ) & ( for a being FinSequence of D holds not a in r2 ) implies r1 = r2 ) assume that A3: for a being FinSequence of D holds not a in r1 and A4: for a being FinSequence of D holds not a in r2 ; ::_thesis: r1 = r2 for a being FinSequence of D holds ( a in r1 iff a in r2 ) by A3, A4; hence r1 = r2 by Def8; ::_thesis: verum end; end; :: deftheorem Def9 defines empty_rel MARGREL1:def_9_:_ for D being non empty set for b2 being Element of relations_on D holds ( b2 = empty_rel D iff for a being FinSequence of D holds not a in b2 ); theorem :: MARGREL1:9 for D being non empty set holds empty_rel D = {} proof let D be non empty set ; ::_thesis: empty_rel D = {} assume A1: not empty_rel D = {} ; ::_thesis: contradiction set x = the Element of empty_rel D; empty_rel D is Subset of (D *) by Def7; then the Element of empty_rel D in D * by A1, TARSKI:def_3; then reconsider a = the Element of empty_rel D as FinSequence of D by FINSEQ_1:def_11; a in empty_rel D by A1; hence contradiction by Def9; ::_thesis: verum end; definition let D be non empty set ; let p be Element of relations_on D; assume A1: p <> empty_rel D ; func the_arity_of p -> Element of NAT means :: MARGREL1:def 10 for a being FinSequence of D st a in p holds it = len a; existence ex b1 being Element of NAT st for a being FinSequence of D st a in p holds b1 = len a proof consider c being FinSequence of D such that A2: c in p by A1, Def9; for a being FinSequence of D st a in p holds len c = len a by A2, Def7; hence ex b1 being Element of NAT st for a being FinSequence of D st a in p holds b1 = len a ; ::_thesis: verum end; uniqueness for b1, b2 being Element of NAT st ( for a being FinSequence of D st a in p holds b1 = len a ) & ( for a being FinSequence of D st a in p holds b2 = len a ) holds b1 = b2 proof let n1, n2 be Element of NAT ; ::_thesis: ( ( for a being FinSequence of D st a in p holds n1 = len a ) & ( for a being FinSequence of D st a in p holds n2 = len a ) implies n1 = n2 ) assume that A3: for a being FinSequence of D st a in p holds n1 = len a and A4: for a being FinSequence of D st a in p holds n2 = len a ; ::_thesis: n1 = n2 consider a being FinSequence of D such that A5: a in p by A1, Def9; len a = n1 by A3, A5; hence n1 = n2 by A4, A5; ::_thesis: verum end; end; :: deftheorem defines the_arity_of MARGREL1:def_10_:_ for D being non empty set for p being Element of relations_on D st p <> empty_rel D holds for b3 being Element of NAT holds ( b3 = the_arity_of p iff for a being FinSequence of D st a in p holds b3 = len a ); scheme :: MARGREL1:sch 3 relDexist2{ F1() -> non empty set , F2() -> Element of NAT , P1[ FinSequence of F1()] } : ex r being Element of relations_on F1() st for a being FinSequence of F1() st len a = F2() holds ( a in r iff P1[a] ) proof defpred S1[ set ] means ex a being FinSequence of F1() st ( len a = F2() & P1[a] & \$1 = a ); consider X being set such that A1: for x being set holds ( x in X iff ( x in F1() * & S1[x] ) ) from XBOOLE_0:sch_1(); A2: for a, b being FinSequence of F1() st a in X & b in X holds len a = len b proof let a, b be FinSequence of F1(); ::_thesis: ( a in X & b in X implies len a = len b ) assume that A3: a in X and A4: b in X ; ::_thesis: len a = len b A5: ex d being FinSequence of F1() st ( len d = F2() & P1[d] & b = d ) by A1, A4; ex c being FinSequence of F1() st ( len c = F2() & P1[c] & a = c ) by A1, A3; hence len a = len b by A5; ::_thesis: verum end; for x being set st x in X holds x in F1() * by A1; then X c= F1() * by TARSKI:def_3; then reconsider r = X as Element of relations_on F1() by A2, Def7; for a being FinSequence of F1() st len a = F2() holds ( a in r iff P1[a] ) proof let a be FinSequence of F1(); ::_thesis: ( len a = F2() implies ( a in r iff P1[a] ) ) assume A6: len a = F2() ; ::_thesis: ( a in r iff P1[a] ) A7: now__::_thesis:_(_P1[a]_implies_a_in_r_) A8: a in F1() * by FINSEQ_1:def_11; assume P1[a] ; ::_thesis: a in r hence a in r by A1, A6, A8; ::_thesis: verum end; now__::_thesis:_(_a_in_r_implies_P1[a]_) assume a in r ; ::_thesis: P1[a] then ex c being FinSequence of F1() st ( len c = F2() & P1[c] & a = c ) by A1; hence P1[a] ; ::_thesis: verum end; hence ( a in r iff P1[a] ) by A7; ::_thesis: verum end; hence ex r being Element of relations_on F1() st for a being FinSequence of F1() st len a = F2() holds ( a in r iff P1[a] ) ; ::_thesis: verum end; definition func BOOLEAN -> set equals :: MARGREL1:def 11 {0,1}; coherence {0,1} is set ; end; :: deftheorem defines BOOLEAN MARGREL1:def_11_:_ BOOLEAN = {0,1}; registration cluster BOOLEAN -> non empty ; coherence not BOOLEAN is empty ; end; definition :: original: FALSE redefine func FALSE -> Element of BOOLEAN ; coherence FALSE is Element of BOOLEAN by TARSKI:def_2; :: original: TRUE redefine func TRUE -> Element of BOOLEAN ; coherence TRUE is Element of BOOLEAN by TARSKI:def_2; end; definition let x be set ; redefine attr x is boolean means :Def12: :: MARGREL1:def 12 x in BOOLEAN ; compatibility ( x is boolean iff x in BOOLEAN ) proof hereby ::_thesis: ( x in BOOLEAN implies x is boolean ) assume x is boolean ; ::_thesis: x in BOOLEAN then ( x = FALSE or x = TRUE ) by XBOOLEAN:def_3; hence x in BOOLEAN ; ::_thesis: verum end; assume x in BOOLEAN ; ::_thesis: x is boolean hence ( x = FALSE or x = TRUE ) by TARSKI:def_2; :: according to XBOOLEAN:def_3 ::_thesis: verum end; end; :: deftheorem Def12 defines boolean MARGREL1:def_12_:_ for x being set holds ( x is boolean iff x in BOOLEAN ); registration cluster -> boolean for Element of BOOLEAN ; coherence for b1 being Element of BOOLEAN holds b1 is boolean by Def12; end; definition let v be boolean set ; redefine func 'not' v equals :: MARGREL1:def 13 TRUE if v = FALSE otherwise FALSE ; compatibility for b1 being set holds ( ( v = FALSE implies ( b1 = 'not' v iff b1 = TRUE ) ) & ( not v = FALSE implies ( b1 = 'not' v iff b1 = FALSE ) ) ) proof let w be boolean set ; ::_thesis: ( ( v = FALSE implies ( w = 'not' v iff w = TRUE ) ) & ( not v = FALSE implies ( w = 'not' v iff w = FALSE ) ) ) thus ( v = FALSE implies ( w = 'not' v iff w = TRUE ) ) ; ::_thesis: ( not v = FALSE implies ( w = 'not' v iff w = FALSE ) ) assume v <> FALSE ; ::_thesis: ( w = 'not' v iff w = FALSE ) then v = TRUE by XBOOLEAN:def_3; hence ( w = 'not' v iff w = FALSE ) ; ::_thesis: verum end; consistency for b1 being set holds verum ; let w be boolean set ; redefine func v '&' w equals :: MARGREL1:def 14 TRUE if ( v = TRUE & w = TRUE ) otherwise FALSE ; compatibility for b1 being set holds ( ( v = TRUE & w = TRUE implies ( b1 = v '&' w iff b1 = TRUE ) ) & ( ( not v = TRUE or not w = TRUE ) implies ( b1 = v '&' w iff b1 = FALSE ) ) ) proof let u be set ; ::_thesis: ( ( v = TRUE & w = TRUE implies ( u = v '&' w iff u = TRUE ) ) & ( ( not v = TRUE or not w = TRUE ) implies ( u = v '&' w iff u = FALSE ) ) ) thus ( v = TRUE & w = TRUE implies ( u = v '&' w iff u = TRUE ) ) ; ::_thesis: ( ( not v = TRUE or not w = TRUE ) implies ( u = v '&' w iff u = FALSE ) ) assume ( v <> TRUE or w <> TRUE ) ; ::_thesis: ( u = v '&' w iff u = FALSE ) then ( v = FALSE or w = FALSE ) by XBOOLEAN:def_3; hence ( u = v '&' w iff u = FALSE ) ; ::_thesis: verum end; consistency for b1 being set holds verum ; end; :: deftheorem defines 'not' MARGREL1:def_13_:_ for v being boolean set holds ( ( v = FALSE implies 'not' v = TRUE ) & ( not v = FALSE implies 'not' v = FALSE ) ); :: deftheorem defines '&' MARGREL1:def_14_:_ for v, w being boolean set holds ( ( v = TRUE & w = TRUE implies v '&' w = TRUE ) & ( ( not v = TRUE or not w = TRUE ) implies v '&' w = FALSE ) ); definition let v be Element of BOOLEAN ; :: original: 'not' redefine func 'not' v -> Element of BOOLEAN ; correctness coherence 'not' v is Element of BOOLEAN ; by Def12; let w be Element of BOOLEAN ; :: original: '&' redefine funcv '&' w -> Element of BOOLEAN ; correctness coherence v '&' w is Element of BOOLEAN ; by Def12; end; theorem :: MARGREL1:10 canceled; theorem :: MARGREL1:11 for v being boolean set holds ( ( v = FALSE implies 'not' v = TRUE ) & ( 'not' v = TRUE implies v = FALSE ) & ( v = TRUE implies 'not' v = FALSE ) & ( 'not' v = FALSE implies v = TRUE ) ) ; theorem :: MARGREL1:12 for v, w being boolean set holds ( ( v '&' w = TRUE implies ( v = TRUE & w = TRUE ) ) & ( v = TRUE & w = TRUE implies v '&' w = TRUE ) & ( not v '&' w = FALSE or v = FALSE or w = FALSE ) & ( ( v = FALSE or w = FALSE ) implies v '&' w = FALSE ) ) by XBOOLEAN:101, XBOOLEAN:140; theorem :: MARGREL1:13 for v being boolean set holds FALSE '&' v = FALSE ; theorem :: MARGREL1:14 for v being boolean set holds TRUE '&' v = v ; theorem :: MARGREL1:15 for v being boolean set st v '&' v = FALSE holds v = FALSE ; theorem :: MARGREL1:16 for v, w, u being boolean set holds v '&' (w '&' u) = (v '&' w) '&' u ; definition let X be set ; func ALL X -> set equals :Def15: :: MARGREL1:def 15 TRUE if not FALSE in X otherwise FALSE ; correctness coherence ( ( not FALSE in X implies TRUE is set ) & ( FALSE in X implies FALSE is set ) ); consistency for b1 being set holds verum; ; end; :: deftheorem Def15 defines ALL MARGREL1:def_15_:_ for X being set holds ( ( not FALSE in X implies ALL X = TRUE ) & ( FALSE in X implies ALL X = FALSE ) ); registration let X be set ; cluster ALL X -> boolean ; correctness coherence ALL X is boolean ; by Def15; end; definition let X be set ; :: original: ALL redefine func ALL X -> Element of BOOLEAN ; correctness coherence ALL X is Element of BOOLEAN ; by Def12; end; theorem :: MARGREL1:17 for X being set holds ( ( not FALSE in X implies ALL X = TRUE ) & ( ALL X = TRUE implies not FALSE in X ) & ( FALSE in X implies ALL X = FALSE ) & ( ALL X = FALSE implies FALSE in X ) ) by Def15; begin definition let f be Relation; attrf is boolean-valued means :Def16: :: MARGREL1:def 16 rng f c= BOOLEAN ; end; :: deftheorem Def16 defines boolean-valued MARGREL1:def_16_:_ for f being Relation holds ( f is boolean-valued iff rng f c= BOOLEAN ); registration cluster Relation-like Function-like boolean-valued for set ; existence ex b1 being Function st b1 is boolean-valued proof take {} ; ::_thesis: {} is boolean-valued thus rng {} c= BOOLEAN by XBOOLE_1:2; :: according to MARGREL1:def_16 ::_thesis: verum end; end; registration let f be boolean-valued Function; let x be set ; clusterf . x -> boolean ; coherence f . x is boolean proof percases ( not x in dom f or x in dom f ) ; suppose not x in dom f ; ::_thesis: f . x is boolean then f . x = FALSE by FUNCT_1:def_2; hence f . x in BOOLEAN ; :: according to MARGREL1:def_12 ::_thesis: verum end; supposeA1: x in dom f ; ::_thesis: f . x is boolean A2: rng f c= BOOLEAN by Def16; f . x in rng f by A1, FUNCT_1:def_3; hence f . x in BOOLEAN by A2; :: according to MARGREL1:def_12 ::_thesis: verum end; end; end; end; definition let p be boolean-valued Function; func 'not' p -> boolean-valued Function means :Def17: :: MARGREL1:def 17 ( dom it = dom p & ( for x being set st x in dom p holds it . x = 'not' (p . x) ) ); existence ex b1 being boolean-valued Function st ( dom b1 = dom p & ( for x being set st x in dom p holds b1 . x = 'not' (p . x) ) ) proof deffunc H1( set ) -> set = 'not' (p . \$1); consider q being Function such that A1: dom q = dom p and A2: for x being set st x in dom p holds q . x = H1(x) from FUNCT_1:sch_3(); q is boolean-valued proof let x be set ; :: according to TARSKI:def_3,MARGREL1:def_16 ::_thesis: ( not x in rng q or x in BOOLEAN ) assume x in rng q ; ::_thesis: x in BOOLEAN then consider y being set such that A3: y in dom q and A4: x = q . y by FUNCT_1:def_3; x = 'not' (p . y) by A1, A2, A3, A4; then ( x = FALSE or x = TRUE ) by XBOOLEAN:def_3; hence x in BOOLEAN ; ::_thesis: verum end; hence ex b1 being boolean-valued Function st ( dom b1 = dom p & ( for x being set st x in dom p holds b1 . x = 'not' (p . x) ) ) by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being boolean-valued Function st dom b1 = dom p & ( for x being set st x in dom p holds b1 . x = 'not' (p . x) ) & dom b2 = dom p & ( for x being set st x in dom p holds b2 . x = 'not' (p . x) ) holds b1 = b2 proof let q1, q2 be boolean-valued Function; ::_thesis: ( dom q1 = dom p & ( for x being set st x in dom p holds q1 . x = 'not' (p . x) ) & dom q2 = dom p & ( for x being set st x in dom p holds q2 . x = 'not' (p . x) ) implies q1 = q2 ) assume that A5: dom q1 = dom p and A6: for x being set st x in dom p holds q1 . x = 'not' (p . x) and A7: dom q2 = dom p and A8: for x being set st x in dom p holds q2 . x = 'not' (p . x) ; ::_thesis: q1 = q2 for x being set st x in dom p holds q1 . x = q2 . x proof let x be set ; ::_thesis: ( x in dom p implies q1 . x = q2 . x ) assume A9: x in dom p ; ::_thesis: q1 . x = q2 . x then q1 . x = 'not' (p . x) by A6; hence q1 . x = q2 . x by A8, A9; ::_thesis: verum end; hence q1 = q2 by A5, A7, FUNCT_1:2; ::_thesis: verum end; involutiveness for b1, b2 being boolean-valued Function st dom b1 = dom b2 & ( for x being set st x in dom b2 holds b1 . x = 'not' (b2 . x) ) holds ( dom b2 = dom b1 & ( for x being set st x in dom b1 holds b2 . x = 'not' (b1 . x) ) ) proof let q, p be boolean-valued Function; ::_thesis: ( dom q = dom p & ( for x being set st x in dom p holds q . x = 'not' (p . x) ) implies ( dom p = dom q & ( for x being set st x in dom q holds p . x = 'not' (q . x) ) ) ) assume that A10: dom q = dom p and A11: for x being set st x in dom p holds q . x = 'not' (p . x) ; ::_thesis: ( dom p = dom q & ( for x being set st x in dom q holds p . x = 'not' (q . x) ) ) thus dom p = dom q by A10; ::_thesis: for x being set st x in dom q holds p . x = 'not' (q . x) let x be set ; ::_thesis: ( x in dom q implies p . x = 'not' (q . x) ) assume A12: x in dom q ; ::_thesis: p . x = 'not' (q . x) thus p . x = 'not' ('not' (p . x)) .= 'not' (q . x) by A10, A11, A12 ; ::_thesis: verum end; let q be boolean-valued Function; funcp '&' q -> boolean-valued Function means :Def18: :: MARGREL1:def 18 ( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds it . x = (p . x) '&' (q . x) ) ); existence ex b1 being boolean-valued Function st ( dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds b1 . x = (p . x) '&' (q . x) ) ) proof deffunc H1( set ) -> set = (p . \$1) '&' (q . \$1); consider s being Function such that A13: dom s = (dom p) /\ (dom q) and A14: for x being set st x in (dom p) /\ (dom q) holds s . x = H1(x) from FUNCT_1:sch_3(); s is boolean-valued proof let x be set ; :: according to TARSKI:def_3,MARGREL1:def_16 ::_thesis: ( not x in rng s or x in BOOLEAN ) assume x in rng s ; ::_thesis: x in BOOLEAN then consider y being set such that A15: y in dom s and A16: x = s . y by FUNCT_1:def_3; x = (p . y) '&' (q . y) by A13, A14, A15, A16; then ( x = FALSE or x = TRUE ) by XBOOLEAN:def_3; hence x in BOOLEAN ; ::_thesis: verum end; hence ex b1 being boolean-valued Function st ( dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds b1 . x = (p . x) '&' (q . x) ) ) by A13, A14; ::_thesis: verum end; uniqueness for b1, b2 being boolean-valued Function st dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds b1 . x = (p . x) '&' (q . x) ) & dom b2 = (dom p) /\ (dom q) & ( for x being set st x in dom b2 holds b2 . x = (p . x) '&' (q . x) ) holds b1 = b2 proof let s1, s2 be boolean-valued Function; ::_thesis: ( dom s1 = (dom p) /\ (dom q) & ( for x being set st x in dom s1 holds s1 . x = (p . x) '&' (q . x) ) & dom s2 = (dom p) /\ (dom q) & ( for x being set st x in dom s2 holds s2 . x = (p . x) '&' (q . x) ) implies s1 = s2 ) assume that A17: dom s1 = (dom p) /\ (dom q) and A18: for x being set st x in dom s1 holds s1 . x = (p . x) '&' (q . x) and A19: dom s2 = (dom p) /\ (dom q) and A20: for x being set st x in dom s2 holds s2 . x = (p . x) '&' (q . x) ; ::_thesis: s1 = s2 for x being set st x in dom s1 holds s1 . x = s2 . x proof let x be set ; ::_thesis: ( x in dom s1 implies s1 . x = s2 . x ) assume A21: x in dom s1 ; ::_thesis: s1 . x = s2 . x then s1 . x = (p . x) '&' (q . x) by A18; hence s1 . x = s2 . x by A17, A19, A20, A21; ::_thesis: verum end; hence s1 = s2 by A17, A19, FUNCT_1:2; ::_thesis: verum end; commutativity for b1, p, q being boolean-valued Function st dom b1 = (dom p) /\ (dom q) & ( for x being set st x in dom b1 holds b1 . x = (p . x) '&' (q . x) ) holds ( dom b1 = (dom q) /\ (dom p) & ( for x being set st x in dom b1 holds b1 . x = (q . x) '&' (p . x) ) ) ; idempotence for p being boolean-valued Function holds ( dom p = (dom p) /\ (dom p) & ( for x being set st x in dom p holds p . x = (p . x) '&' (p . x) ) ) ; end; :: deftheorem Def17 defines 'not' MARGREL1:def_17_:_ for p, b2 being boolean-valued Function holds ( b2 = 'not' p iff ( dom b2 = dom p & ( for x being set st x in dom p holds b2 . x = 'not' (p . x) ) ) ); :: deftheorem Def18 defines '&' MARGREL1:def_18_:_ for p, q, b3 being boolean-valued Function holds ( b3 = p '&' q iff ( dom b3 = (dom p) /\ (dom q) & ( for x being set st x in dom b3 holds b3 . x = (p . x) '&' (q . x) ) ) ); registration let A be set ; cluster Function-like quasi_total -> boolean-valued for Element of bool [:A,BOOLEAN:]; coherence for b1 being Function of A,BOOLEAN holds b1 is boolean-valued proof let F be Function of A,BOOLEAN; ::_thesis: F is boolean-valued thus rng F c= BOOLEAN by RELAT_1:def_19; :: according to MARGREL1:def_16 ::_thesis: verum end; end; definition let A be non empty set ; let p be Function of A,BOOLEAN; :: original: 'not' redefine func 'not' p -> Function of A,BOOLEAN means :: MARGREL1:def 19 for x being Element of A holds it . x = 'not' (p . x); coherence 'not' p is Function of A,BOOLEAN proof A1: dom ('not' p) = dom p by Def17 .= A by PARTFUN1:def_2 ; rng ('not' p) c= BOOLEAN by Def16; hence 'not' p is Function of A,BOOLEAN by A1, FUNCT_2:2; ::_thesis: verum end; compatibility for b1 being Function of A,BOOLEAN holds ( b1 = 'not' p iff for x being Element of A holds b1 . x = 'not' (p . x) ) proof let IT be Function of A,BOOLEAN; ::_thesis: ( IT = 'not' p iff for x being Element of A holds IT . x = 'not' (p . x) ) A2: dom IT = A by FUNCT_2:def_1; hereby ::_thesis: ( ( for x being Element of A holds IT . x = 'not' (p . x) ) implies IT = 'not' p ) assume A3: IT = 'not' p ; ::_thesis: for x being Element of A holds IT . x = 'not' (p . x) let x be Element of A; ::_thesis: IT . x = 'not' (p . x) x in A ; then x in dom p by FUNCT_2:def_1; hence IT . x = 'not' (p . x) by A3, Def17; ::_thesis: verum end; A4: dom p = A by FUNCT_2:def_1; assume for x being Element of A holds IT . x = 'not' (p . x) ; ::_thesis: IT = 'not' p then for x being set st x in dom p holds IT . x = 'not' (p . x) by A4; hence IT = 'not' p by A2, A4, Def17; ::_thesis: verum end; let q be Function of A,BOOLEAN; :: original: '&' redefine funcp '&' q -> Function of A,BOOLEAN means :: MARGREL1:def 20 for x being Element of A holds it . x = (p . x) '&' (q . x); coherence p '&' q is Function of A,BOOLEAN proof A5: rng (p '&' q) c= BOOLEAN by Def16; ( dom p = A & dom q = A ) by PARTFUN1:def_2; then dom (p '&' q) = A /\ A by Def18 .= A ; hence p '&' q is Function of A,BOOLEAN by A5, FUNCT_2:2; ::_thesis: verum end; compatibility for b1 being Function of A,BOOLEAN holds ( b1 = p '&' q iff for x being Element of A holds b1 . x = (p . x) '&' (q . x) ) proof let IT be Function of A,BOOLEAN; ::_thesis: ( IT = p '&' q iff for x being Element of A holds IT . x = (p . x) '&' (q . x) ) A6: dom IT = A by FUNCT_2:def_1; hereby ::_thesis: ( ( for x being Element of A holds IT . x = (p . x) '&' (q . x) ) implies IT = p '&' q ) assume A7: IT = p '&' q ; ::_thesis: for x being Element of A holds IT . x = (p . x) '&' (q . x) let x be Element of A; ::_thesis: IT . x = (p . x) '&' (q . x) A8: dom q = A by FUNCT_2:def_1; dom p = A by FUNCT_2:def_1; then dom (p '&' q) = A /\ A by A8, Def18 .= A ; hence IT . x = (p . x) '&' (q . x) by A7, Def18; ::_thesis: verum end; A9: dom q = A by FUNCT_2:def_1; A10: dom IT = A /\ A by FUNCT_2:def_1 .= (dom p) /\ (dom q) by A9, FUNCT_2:def_1 ; assume for x being Element of A holds IT . x = (p . x) '&' (q . x) ; ::_thesis: IT = p '&' q then for x being set st x in dom IT holds IT . x = (p . x) '&' (q . x) by A6; hence IT = p '&' q by A10, Def18; ::_thesis: verum end; end; :: deftheorem defines 'not' MARGREL1:def_19_:_ for A being non empty set for p, b3 being Function of A,BOOLEAN holds ( b3 = 'not' p iff for x being Element of A holds b3 . x = 'not' (p . x) ); :: deftheorem defines '&' MARGREL1:def_20_:_ for A being non empty set for p, q, b4 being Function of A,BOOLEAN holds ( b4 = p '&' q iff for x being Element of A holds b4 . x = (p . x) '&' (q . x) ); begin definition let IT be Relation; attrIT is homogeneous means :Def21: :: MARGREL1:def 21 dom IT is with_common_domain ; end; :: deftheorem Def21 defines homogeneous MARGREL1:def_21_:_ for IT being Relation holds ( IT is homogeneous iff dom IT is with_common_domain ); definition let A be set ; let IT be PartFunc of (A *),A; attrIT is quasi_total means :Def22: :: MARGREL1:def 22 for x, y being FinSequence of A st len x = len y & x in dom IT holds y in dom IT; end; :: deftheorem Def22 defines quasi_total MARGREL1:def_22_:_ for A being set for IT being PartFunc of (A *),A holds ( IT is quasi_total iff for x, y being FinSequence of A st len x = len y & x in dom IT holds y in dom IT ); registration let f be Relation; let X be with_common_domain set ; clusterf | X -> homogeneous ; coherence f | X is homogeneous proof dom (f | X) c= X by RELAT_1:58; hence dom (f | X) is with_common_domain ; :: according to MARGREL1:def_21 ::_thesis: verum end; end; registration let A be non empty set ; let f be PartFunc of (A *),A; cluster dom f -> FinSequence-membered ; coherence dom f is FinSequence-membered proof dom f c= A * by RELAT_1:def_18; hence dom f is FinSequence-membered ; ::_thesis: verum end; end; registration let A be non empty set ; cluster Relation-like A * -defined A -valued Function-like non empty homogeneous quasi_total for Element of bool [:(A *),A:]; existence ex b1 being PartFunc of (A *),A st ( b1 is homogeneous & b1 is quasi_total & not b1 is empty ) proof set a = the Element of A; set f = (<*> A) .--> the Element of A; A1: dom ((<*> A) .--> the Element of A) = {(<*> A)} by FUNCOP_1:13; A2: dom ((<*> A) .--> the Element of A) c= A * proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom ((<*> A) .--> the Element of A) or z in A * ) assume z in dom ((<*> A) .--> the Element of A) ; ::_thesis: z in A * then z = <*> A by A1, TARSKI:def_1; hence z in A * by FINSEQ_1:def_11; ::_thesis: verum end; A3: rng ((<*> A) .--> the Element of A) = { the Element of A} by FUNCOP_1:8; rng ((<*> A) .--> the Element of A) c= A proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng ((<*> A) .--> the Element of A) or z in A ) assume z in rng ((<*> A) .--> the Element of A) ; ::_thesis: z in A then z = the Element of A by A3, TARSKI:def_1; hence z in A ; ::_thesis: verum end; then reconsider f = (<*> A) .--> the Element of A as PartFunc of (A *),A by A2, RELSET_1:4; A4: f is quasi_total proof let x, y be FinSequence of A; :: according to MARGREL1:def_22 ::_thesis: ( len x = len y & x in dom f implies y in dom f ) assume that A5: len x = len y and A6: x in dom f ; ::_thesis: y in dom f x = <*> A by A1, A6, TARSKI:def_1; then len x = 0 ; then y = <*> A by A5; hence y in dom f by A1, TARSKI:def_1; ::_thesis: verum end; f is homogeneous proof let x, y be FinSequence; :: according to MARGREL1:def_1,MARGREL1:def_21 ::_thesis: ( x in dom f & y in dom f implies len x = len y ) assume that A7: x in dom f and A8: y in dom f ; ::_thesis: len x = len y x = <*> A by A1, A7, TARSKI:def_1; hence len x = len y by A1, A8, TARSKI:def_1; ::_thesis: verum end; hence ex b1 being PartFunc of (A *),A st ( b1 is homogeneous & b1 is quasi_total & not b1 is empty ) by A4; ::_thesis: verum end; end; registration cluster Relation-like Function-like non empty homogeneous for set ; existence ex b1 being Function st ( b1 is homogeneous & not b1 is empty ) proof set f = the non empty homogeneous PartFunc of ({{}} *),{{}}; take the non empty homogeneous PartFunc of ({{}} *),{{}} ; ::_thesis: ( the non empty homogeneous PartFunc of ({{}} *),{{}} is homogeneous & not the non empty homogeneous PartFunc of ({{}} *),{{}} is empty ) thus ( the non empty homogeneous PartFunc of ({{}} *),{{}} is homogeneous & not the non empty homogeneous PartFunc of ({{}} *),{{}} is empty ) ; ::_thesis: verum end; end; registration let R be homogeneous Relation; cluster dom R -> with_common_domain ; coherence dom R is with_common_domain by Def21; end; theorem Th18: :: MARGREL1:18 for A being non empty set for a being Element of A holds (<*> A) .--> a is non empty homogeneous quasi_total PartFunc of (A *),A proof let A be non empty set ; ::_thesis: for a being Element of A holds (<*> A) .--> a is non empty homogeneous quasi_total PartFunc of (A *),A let a be Element of A; ::_thesis: (<*> A) .--> a is non empty homogeneous quasi_total PartFunc of (A *),A set f = (<*> A) .--> a; A1: dom ((<*> A) .--> a) = {(<*> A)} by FUNCOP_1:13; A2: dom ((<*> A) .--> a) c= A * proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom ((<*> A) .--> a) or z in A * ) assume z in dom ((<*> A) .--> a) ; ::_thesis: z in A * then z = <*> A by A1, TARSKI:def_1; hence z in A * by FINSEQ_1:def_11; ::_thesis: verum end; A3: rng ((<*> A) .--> a) = {a} by FUNCOP_1:8; rng ((<*> A) .--> a) c= A proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng ((<*> A) .--> a) or z in A ) assume z in rng ((<*> A) .--> a) ; ::_thesis: z in A then z = a by A3, TARSKI:def_1; hence z in A ; ::_thesis: verum end; then reconsider f = (<*> A) .--> a as PartFunc of (A *),A by A2, RELSET_1:4; A4: f is quasi_total proof let x, y be FinSequence of A; :: according to MARGREL1:def_22 ::_thesis: ( len x = len y & x in dom f implies y in dom f ) assume that A5: len x = len y and A6: x in dom f ; ::_thesis: y in dom f x = <*> A by A1, A6, TARSKI:def_1; then len x = 0 ; then y = <*> A by A5; hence y in dom f by A1, TARSKI:def_1; ::_thesis: verum end; f is homogeneous proof let x, y be FinSequence; :: according to MARGREL1:def_1,MARGREL1:def_21 ::_thesis: ( x in dom f & y in dom f implies len x = len y ) assume that A7: x in dom f and A8: y in dom f ; ::_thesis: len x = len y x = <*> A by A1, A7, TARSKI:def_1; hence len x = len y by A1, A8, TARSKI:def_1; ::_thesis: verum end; hence (<*> A) .--> a is non empty homogeneous quasi_total PartFunc of (A *),A by A4; ::_thesis: verum end; theorem :: MARGREL1:19 for A being non empty set for a being Element of A holds (<*> A) .--> a is Element of PFuncs ((A *),A) proof let A be non empty set ; ::_thesis: for a being Element of A holds (<*> A) .--> a is Element of PFuncs ((A *),A) let a be Element of A; ::_thesis: (<*> A) .--> a is Element of PFuncs ((A *),A) set f = (<*> A) .--> a; A1: dom ((<*> A) .--> a) = {(<*> A)} by FUNCOP_1:13; A2: dom ((<*> A) .--> a) c= A * proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom ((<*> A) .--> a) or z in A * ) assume z in dom ((<*> A) .--> a) ; ::_thesis: z in A * then z = <*> A by A1, TARSKI:def_1; hence z in A * by FINSEQ_1:def_11; ::_thesis: verum end; A3: rng ((<*> A) .--> a) = {a} by FUNCOP_1:8; rng ((<*> A) .--> a) c= A proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng ((<*> A) .--> a) or z in A ) assume z in rng ((<*> A) .--> a) ; ::_thesis: z in A then z = a by A3, TARSKI:def_1; hence z in A ; ::_thesis: verum end; then reconsider f = (<*> A) .--> a as PartFunc of (A *),A by A2, RELSET_1:4; f in PFuncs ((A *),A) by PARTFUN1:45; hence (<*> A) .--> a is Element of PFuncs ((A *),A) ; ::_thesis: verum end; definition let A be set ; mode PFuncFinSequence of A is FinSequence of PFuncs ((A *),A); end; definition let A be set ; let IT be PFuncFinSequence of A; attrIT is homogeneous means :Def23: :: MARGREL1:def 23 for n being Nat for h being PartFunc of (A *),A st n in dom IT & h = IT . n holds h is homogeneous ; end; :: deftheorem Def23 defines homogeneous MARGREL1:def_23_:_ for A being set for IT being PFuncFinSequence of A holds ( IT is homogeneous iff for n being Nat for h being PartFunc of (A *),A st n in dom IT & h = IT . n holds h is homogeneous ); definition let A be set ; let IT be PFuncFinSequence of A; attrIT is quasi_total means :Def24: :: MARGREL1:def 24 for n being Nat for h being PartFunc of (A *),A st n in dom IT & h = IT . n holds h is quasi_total ; end; :: deftheorem Def24 defines quasi_total MARGREL1:def_24_:_ for A being set for IT being PFuncFinSequence of A holds ( IT is quasi_total iff for n being Nat for h being PartFunc of (A *),A st n in dom IT & h = IT . n holds h is quasi_total ); definition let A be non empty set ; let x be Element of PFuncs ((A *),A); :: original: <* redefine func<*x*> -> PFuncFinSequence of A; coherence <*x*> is PFuncFinSequence of A proof <*x*> is FinSequence of PFuncs ((A *),A) ; hence <*x*> is PFuncFinSequence of A ; ::_thesis: verum end; end; registration let A be non empty set ; cluster Relation-like non-empty NAT -defined PFuncs ((A *),A) -valued Function-like Function-yielding V22() V31() FinSequence-like FinSubsequence-like countable homogeneous quasi_total for FinSequence of PFuncs ((A *),A); existence ex b1 being PFuncFinSequence of A st ( b1 is homogeneous & b1 is quasi_total & b1 is non-empty ) proof set a = the Element of A; reconsider f = (<*> A) .--> the Element of A as PartFunc of (A *),A by Th18; reconsider f = f as Element of PFuncs ((A *),A) by PARTFUN1:45; take <*f*> ; ::_thesis: ( <*f*> is homogeneous & <*f*> is quasi_total & <*f*> is non-empty ) thus <*f*> is homogeneous ::_thesis: ( <*f*> is quasi_total & <*f*> is non-empty ) proof let n be Nat; :: according to MARGREL1:def_23 ::_thesis: for h being PartFunc of (A *),A st n in dom <*f*> & h = <*f*> . n holds h is homogeneous let h be PartFunc of (A *),A; ::_thesis: ( n in dom <*f*> & h = <*f*> . n implies h is homogeneous ) assume that A1: n in dom <*f*> and A2: h = <*f*> . n ; ::_thesis: h is homogeneous n in {1} by A1, FINSEQ_1:2, FINSEQ_1:def_8; then h = <*f*> . 1 by A2, TARSKI:def_1; then h = f by FINSEQ_1:def_8; hence h is homogeneous by Th18; ::_thesis: verum end; thus <*f*> is quasi_total ::_thesis: <*f*> is non-empty proof let n be Nat; :: according to MARGREL1:def_24 ::_thesis: for h being PartFunc of (A *),A st n in dom <*f*> & h = <*f*> . n holds h is quasi_total let h be PartFunc of (A *),A; ::_thesis: ( n in dom <*f*> & h = <*f*> . n implies h is quasi_total ) assume that A3: n in dom <*f*> and A4: h = <*f*> . n ; ::_thesis: h is quasi_total n in {1} by A3, FINSEQ_1:2, FINSEQ_1:def_8; then h = <*f*> . 1 by A4, TARSKI:def_1; then h = f by FINSEQ_1:def_8; hence h is quasi_total by Th18; ::_thesis: verum end; thus <*f*> is non-empty ::_thesis: verum proof let n be set ; :: according to FUNCT_1:def_9 ::_thesis: ( not n in dom <*f*> or not <*f*> . n is empty ) assume A5: n in dom <*f*> ; ::_thesis: not <*f*> . n is empty then reconsider n = n as Element of NAT ; n in {1} by A5, FINSEQ_1:2, FINSEQ_1:def_8; then n = 1 by TARSKI:def_1; hence not <*f*> . n is empty by FINSEQ_1:def_8; ::_thesis: verum end; end; end; registration let A be non empty set ; let f be homogeneous PFuncFinSequence of A; let i be set ; clusterf . i -> homogeneous ; coherence f . i is homogeneous proof percases ( i in dom f or not i in dom f ) ; supposeA1: i in dom f ; ::_thesis: f . i is homogeneous A2: rng f c= PFuncs ((A *),A) by RELAT_1:def_19; f . i in rng f by A1, FUNCT_1:3; then f . i is PartFunc of (A *),A by A2, PARTFUN1:46; hence f . i is homogeneous by A1, Def23; ::_thesis: verum end; supposeA3: not i in dom f ; ::_thesis: f . i is homogeneous let x be Function; :: according to CARD_3:def_10,MARGREL1:def_21 ::_thesis: for b1 being set holds ( not x in dom (f . i) or not b1 in dom (f . i) or dom x = dom b1 ) thus for b1 being set holds ( not x in dom (f . i) or not b1 in dom (f . i) or dom x = dom b1 ) by A3, FUNCT_1:def_2, RELAT_1:38; ::_thesis: verum end; end; end; end; theorem :: MARGREL1:20 for A being non empty set for a being Element of A for x being Element of PFuncs ((A *),A) st x = (<*> A) .--> a holds ( <*x*> is homogeneous & <*x*> is quasi_total & <*x*> is non-empty ) proof let A be non empty set ; ::_thesis: for a being Element of A for x being Element of PFuncs ((A *),A) st x = (<*> A) .--> a holds ( <*x*> is homogeneous & <*x*> is quasi_total & <*x*> is non-empty ) let a be Element of A; ::_thesis: for x being Element of PFuncs ((A *),A) st x = (<*> A) .--> a holds ( <*x*> is homogeneous & <*x*> is quasi_total & <*x*> is non-empty ) let x be Element of PFuncs ((A *),A); ::_thesis: ( x = (<*> A) .--> a implies ( <*x*> is homogeneous & <*x*> is quasi_total & <*x*> is non-empty ) ) assume A1: x = (<*> A) .--> a ; ::_thesis: ( <*x*> is homogeneous & <*x*> is quasi_total & <*x*> is non-empty ) A2: for n being Nat for h being PartFunc of (A *),A st n in dom <*x*> & h = <*x*> . n holds h is homogeneous proof let n be Nat; ::_thesis: for h being PartFunc of (A *),A st n in dom <*x*> & h = <*x*> . n holds h is homogeneous let h be PartFunc of (A *),A; ::_thesis: ( n in dom <*x*> & h = <*x*> . n implies h is homogeneous ) assume that A3: n in dom <*x*> and A4: h = <*x*> . n ; ::_thesis: h is homogeneous n in {1} by A3, FINSEQ_1:2, FINSEQ_1:def_8; then h = <*x*> . 1 by A4, TARSKI:def_1; then h = x by FINSEQ_1:def_8; hence h is homogeneous by A1, Th18; ::_thesis: verum end; A5: for n being Nat for h being PartFunc of (A *),A st n in dom <*x*> & h = <*x*> . n holds h is quasi_total proof let n be Nat; ::_thesis: for h being PartFunc of (A *),A st n in dom <*x*> & h = <*x*> . n holds h is quasi_total let h be PartFunc of (A *),A; ::_thesis: ( n in dom <*x*> & h = <*x*> . n implies h is quasi_total ) assume that A6: n in dom <*x*> and A7: h = <*x*> . n ; ::_thesis: h is quasi_total n in {1} by A6, FINSEQ_1:2, FINSEQ_1:def_8; then h = <*x*> . 1 by A7, TARSKI:def_1; then h = x by FINSEQ_1:def_8; hence h is quasi_total by A1, Th18; ::_thesis: verum end; for n being set st n in dom <*x*> holds not <*x*> . n is empty proof let n be set ; ::_thesis: ( n in dom <*x*> implies not <*x*> . n is empty ) assume n in dom <*x*> ; ::_thesis: not <*x*> . n is empty then n in {1} by FINSEQ_1:2, FINSEQ_1:def_8; then <*x*> . n = <*x*> . 1 by TARSKI:def_1; hence not <*x*> . n is empty by A1, FINSEQ_1:def_8; ::_thesis: verum end; hence ( <*x*> is homogeneous & <*x*> is quasi_total & <*x*> is non-empty ) by A2, A5, Def23, Def24, FUNCT_1:def_9; ::_thesis: verum end; definition let f be homogeneous Relation; func arity f -> Nat means :Def25: :: MARGREL1:def 25 for x being FinSequence st x in dom f holds it = len x if ex x being FinSequence st x in dom f otherwise it = 0 ; consistency for b1 being Nat holds verum ; existence ( ( ex x being FinSequence st x in dom f implies ex b1 being Nat st for x being FinSequence st x in dom f holds b1 = len x ) & ( ( for x being FinSequence holds not x in dom f ) implies ex b1 being Nat st b1 = 0 ) ) proof thus ( ex x being FinSequence st x in dom f implies ex n being Nat st for x being FinSequence st x in dom f holds n = len x ) ::_thesis: ( ( for x being FinSequence holds not x in dom f ) implies ex b1 being Nat st b1 = 0 ) proof given x being FinSequence such that A1: x in dom f ; ::_thesis: ex n being Nat st for x being FinSequence st x in dom f holds n = len x take len x ; ::_thesis: for x being FinSequence st x in dom f holds len x = len x let y be FinSequence; ::_thesis: ( y in dom f implies len x = len y ) assume y in dom f ; ::_thesis: len x = len y then dom x = dom y by A1, CARD_3:def_10; hence len x = len y by FINSEQ_3:29; ::_thesis: verum end; thus ( ( for x being FinSequence holds not x in dom f ) implies ex b1 being Nat st b1 = 0 ) ; ::_thesis: verum end; uniqueness for b1, b2 being Nat holds ( ( ex x being FinSequence st x in dom f & ( for x being FinSequence st x in dom f holds b1 = len x ) & ( for x being FinSequence st x in dom f holds b2 = len x ) implies b1 = b2 ) & ( ( for x being FinSequence holds not x in dom f ) & b1 = 0 & b2 = 0 implies b1 = b2 ) ) proof let n, m be Nat; ::_thesis: ( ( ex x being FinSequence st x in dom f & ( for x being FinSequence st x in dom f holds n = len x ) & ( for x being FinSequence st x in dom f holds m = len x ) implies n = m ) & ( ( for x being FinSequence holds not x in dom f ) & n = 0 & m = 0 implies n = m ) ) hereby ::_thesis: ( ( for x being FinSequence holds not x in dom f ) & n = 0 & m = 0 implies n = m ) given x0 being FinSequence such that A2: x0 in dom f ; ::_thesis: ( ( for x being FinSequence st x in dom f holds n = len x ) & ( for x being FinSequence st x in dom f holds m = len x ) implies n = m ) assume that A3: for x being FinSequence st x in dom f holds n = len x and A4: for x being FinSequence st x in dom f holds m = len x ; ::_thesis: n = m n = len x0 by A2, A3; hence n = m by A2, A4; ::_thesis: verum end; thus ( ( for x being FinSequence holds not x in dom f ) & n = 0 & m = 0 implies n = m ) ; ::_thesis: verum end; end; :: deftheorem Def25 defines arity MARGREL1:def_25_:_ for f being homogeneous Relation for b2 being Nat holds ( ( ex x being FinSequence st x in dom f implies ( b2 = arity f iff for x being FinSequence st x in dom f holds b2 = len x ) ) & ( ( for x being FinSequence holds not x in dom f ) implies ( b2 = arity f iff b2 = 0 ) ) ); definition let f be homogeneous Function; :: original: arity redefine func arity f -> Element of NAT ; coherence arity f is Element of NAT by ORDINAL1:def_12; end; begin theorem :: MARGREL1:21 for n being Nat for D being non empty set for D1 being non empty Subset of D holds (n -tuples_on D) /\ (n -tuples_on D1) = n -tuples_on D1 proof let n be Nat; ::_thesis: for D being non empty set for D1 being non empty Subset of D holds (n -tuples_on D) /\ (n -tuples_on D1) = n -tuples_on D1 let D be non empty set ; ::_thesis: for D1 being non empty Subset of D holds (n -tuples_on D) /\ (n -tuples_on D1) = n -tuples_on D1 let D1 be non empty Subset of D; ::_thesis: (n -tuples_on D) /\ (n -tuples_on D1) = n -tuples_on D1 n -tuples_on D1 c= n -tuples_on D proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in n -tuples_on D1 or z in n -tuples_on D ) assume z in n -tuples_on D1 ; ::_thesis: z in n -tuples_on D then z is Tuple of n,D1 by FINSEQ_2:131; then z is Element of n -tuples_on D by FINSEQ_2:109; hence z in n -tuples_on D ; ::_thesis: verum end; hence (n -tuples_on D) /\ (n -tuples_on D1) = n -tuples_on D1 by XBOOLE_1:28; ::_thesis: verum end; theorem :: MARGREL1:22 for D being non empty set for h being non empty homogeneous quasi_total PartFunc of (D *),D holds dom h = (arity h) -tuples_on D proof let D be non empty set ; ::_thesis: for h being non empty homogeneous quasi_total PartFunc of (D *),D holds dom h = (arity h) -tuples_on D let f be non empty homogeneous quasi_total PartFunc of (D *),D; ::_thesis: dom f = (arity f) -tuples_on D set y = the Element of dom f; A1: dom f c= D * by RELAT_1:def_18; then A2: the Element of dom f in D * by TARSKI:def_3; thus dom f c= (arity f) -tuples_on D :: according to XBOOLE_0:def_10 ::_thesis: (arity f) -tuples_on D c= dom f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in (arity f) -tuples_on D ) assume A3: x in dom f ; ::_thesis: x in (arity f) -tuples_on D then reconsider x9 = x as FinSequence of D by A1, FINSEQ_1:def_11; len x9 = arity f by A3, Def25; then x9 is Element of (arity f) -tuples_on D by FINSEQ_2:92; hence x in (arity f) -tuples_on D ; ::_thesis: verum end; reconsider y = the Element of dom f as FinSequence of D by A2, FINSEQ_1:def_11; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (arity f) -tuples_on D or x in dom f ) assume x in (arity f) -tuples_on D ; ::_thesis: x in dom f then x in { s where s is Element of D * : len s = arity f } by FINSEQ_2:def_4; then A4: ex s being Element of D * st ( x = s & len s = arity f ) ; len y = arity f by Def25; hence x in dom f by A4, Def22; ::_thesis: verum end; definition let D be non empty set ; mode PFuncsDomHQN of D -> non empty set means :Def26: :: MARGREL1:def 26 for x being Element of it holds x is non empty homogeneous quasi_total PartFunc of (D *),D; existence ex b1 being non empty set st for x being Element of b1 holds x is non empty homogeneous quasi_total PartFunc of (D *),D proof set a = the Element of D; reconsider A = {({(<*> D)} --> the Element of D)} as non empty set ; take A ; ::_thesis: for x being Element of A holds x is non empty homogeneous quasi_total PartFunc of (D *),D let x be Element of A; ::_thesis: x is non empty homogeneous quasi_total PartFunc of (D *),D x = (<*> D) .--> the Element of D by TARSKI:def_1; hence x is non empty homogeneous quasi_total PartFunc of (D *),D by Th18; ::_thesis: verum end; end; :: deftheorem Def26 defines PFuncsDomHQN MARGREL1:def_26_:_ for D, b2 being non empty set holds ( b2 is PFuncsDomHQN of D iff for x being Element of b2 holds x is non empty homogeneous quasi_total PartFunc of (D *),D ); definition let D be non empty set ; let P be PFuncsDomHQN of D; :: original: Element redefine mode Element of P -> non empty homogeneous quasi_total PartFunc of (D *),D; coherence for b1 being Element of P holds b1 is non empty homogeneous quasi_total PartFunc of (D *),D by Def26; end;