:: 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;