:: Many-Argument Relations
:: by Edmund Woronowicz
::
:: Received June 1, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


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
proofend;
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 )
proofend;
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 )
proofend;
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
proofend;

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

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 ) )
proofend;
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
proofend;
end;

theorem Th3: :: MARGREL1:3
for p being relation st ( for a being FinSequence holds not a in p ) holds
p = {}
proofend;

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
proofend;
uniqueness
 for b1, b2 being Element of NAT st ( for a being FinSequence st a in p holds
b1 = len a ) &amp; ( for a being FinSequence st a in p holds
b2 = len a ) holds
b1 = b2
proofend;
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
proofend;
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
proofend;
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
proofend;

theorem Th5: :: MARGREL1:5
for k being Element of NAT holds {} is relation_length of k
proofend;

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 &amp; it is relation_length of k );
existence
 ex b1 being relation st
( b1 is relation of X &amp; b1 is relation_length of k )
proofend;
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 &amp; 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 * &amp; ( for a, b being FinSequence of D st a in X &amp; 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 * &amp; ( for a, b being FinSequence of D st a in X &amp; b in X holds
len a = len b ) ) )
proofend;
uniqueness
 for b1, b2 being set st ( for X being set holds
( X in b1 iff ( X c= D * &amp; ( for a, b being FinSequence of D st a in X &amp; b in X holds
len a = len b ) ) ) ) &amp; ( for X being set holds
( X in b2 iff ( X c= D * &amp; ( for a, b being FinSequence of D st a in X &amp; b in X holds
len a = len b ) ) ) ) holds
b1 = b2
proofend;
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 * &amp; ( for a, b being FinSequence of D st a in X &amp; 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
proofend;
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
proofend;

theorem :: MARGREL1:7
for D being non empty set
for a being FinSequence of D holds {a} is Element of relations_on D
proofend;

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

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 ) )
proofend;
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] &amp; P1[b] holds
len a = len b
proofend;

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
proofend;
uniqueness
 for b1, b2 being Element of relations_on D st ( for a being FinSequence of D holds not a in b1 ) &amp; ( for a being FinSequence of D holds not a in b2 ) holds
b1 = b2
proofend;
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 = {}
proofend;

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
proofend;
uniqueness
 for b1, b2 being Element of NAT st ( for a being FinSequence of D st a in p holds
b1 = len a ) &amp; ( for a being FinSequence of D st a in p holds
b2 = len a ) holds
b1 = b2
proofend;
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] )
proofend;

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 )
proofend;
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 ) ) &amp; ( not v = FALSE implies ( b1 = 'not' v iff b1 = FALSE ) ) )
proofend;
consistency
 for b1 being set holds verum ;
let w be boolean set ;
redefine func v '&amp;' w equals :: MARGREL1:def 14
 TRUE  if ( v = TRUE &amp; w = TRUE )
otherwise  FALSE ;
compatibility
 for b1 being set holds
( ( v = TRUE &amp; w = TRUE implies ( b1 = v '&amp;' w iff b1 = TRUE ) ) &amp; ( ( not v = TRUE or not w = TRUE ) implies ( b1 = v '&amp;' w iff b1 = FALSE ) ) )
proofend;
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 ) &amp; ( not v = FALSE implies 'not' v = FALSE ) );

:: deftheorem  defines '&amp;' MARGREL1:def_14_:_
 for v, w being boolean set holds
( ( v = TRUE &amp; w = TRUE implies v '&amp;' w = TRUE ) &amp; ( ( not v = TRUE or not w = TRUE ) implies v '&amp;' 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:'&amp;'
redefine funcv '&amp;' w ->  Element of BOOLEAN ;
correctness
coherence
v '&amp;' 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 ) &amp; ( 'not' v = TRUE implies v = FALSE ) &amp; ( v = TRUE implies 'not' v = FALSE ) &amp; ( 'not' v = FALSE implies v = TRUE ) ) ;

theorem :: MARGREL1:12
for v, w being boolean set holds
( ( v '&amp;' w = TRUE implies ( v = TRUE &amp; w = TRUE ) ) &amp; ( v = TRUE &amp; w = TRUE implies v '&amp;' w = TRUE ) &amp; ( not v '&amp;' w = FALSE or v = FALSE or w = FALSE ) &amp; ( ( v = FALSE or w = FALSE ) implies v '&amp;' w = FALSE ) ) by XBOOLEAN:101, XBOOLEAN:140;

theorem :: MARGREL1:13
for v being boolean set holds FALSE '&amp;' v = FALSE ;

theorem :: MARGREL1:14
for v being boolean set holds TRUE '&amp;' v = v ;

theorem :: MARGREL1:15
for v being boolean set st v '&amp;' v = FALSE holds
v = FALSE ;

theorem :: MARGREL1:16
for v, w, u being boolean set holds v '&amp;' (w '&amp;' u) = (v '&amp;' w) '&amp;' 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 ) &amp; ( 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 ) &amp; ( 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 ) &amp; ( ALL X = TRUE implies not FALSE in X ) &amp; ( FALSE in X implies ALL X = FALSE ) &amp; ( ALL X = FALSE implies FALSE in X ) ) by Def15;

begin

:: from VALUAT_1, 2007.03.15, A.T.
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
proofend;
end;

registration
let f be boolean-valued Function;
let x be set ;
clusterf . x ->  boolean ;
coherence
 f . x is boolean
proofend;
end;

definition
let p be boolean-valued Function;
func 'not' p ->  boolean-valued Function means :Def17: :: MARGREL1:def 17
( dom it = dom p &amp; ( 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 &amp; ( for x being set st x in dom p holds
b1 . x = 'not' (p . x) ) )
proofend;
uniqueness
 for b1, b2 being boolean-valued Function st dom b1 = dom p &amp; ( for x being set st x in dom p holds
b1 . x = 'not' (p . x) ) &amp; dom b2 = dom p &amp; ( for x being set st x in dom p holds
b2 . x = 'not' (p . x) ) holds
b1 = b2
proofend;
involutiveness
 for b1, b2 being boolean-valued Function st dom b1 = dom b2 &amp; ( for x being set st x in dom b2 holds
b1 . x = 'not' (b2 . x) ) holds
( dom b2 = dom b1 &amp; ( for x being set st x in dom b1 holds
b2 . x = 'not' (b1 . x) ) )
proofend;
let q be boolean-valued Function;
funcp '&amp;' q ->  boolean-valued Function means :Def18: :: MARGREL1:def 18
( dom it = (dom p) /\ (dom q) &amp; ( for x being set st x in dom it holds
it . x = (p . x) '&amp;' (q . x) ) );
existence
 ex b1 being boolean-valued Function st
( dom b1 = (dom p) /\ (dom q) &amp; ( for x being set st x in dom b1 holds
b1 . x = (p . x) '&amp;' (q . x) ) )
proofend;
uniqueness
 for b1, b2 being boolean-valued Function st dom b1 = (dom p) /\ (dom q) &amp; ( for x being set st x in dom b1 holds
b1 . x = (p . x) '&amp;' (q . x) ) &amp; dom b2 = (dom p) /\ (dom q) &amp; ( for x being set st x in dom b2 holds
b2 . x = (p . x) '&amp;' (q . x) ) holds
b1 = b2
proofend;
commutativity
 for b1, p, q being boolean-valued Function st dom b1 = (dom p) /\ (dom q) &amp; ( for x being set st x in dom b1 holds
b1 . x = (p . x) '&amp;' (q . x) ) holds
( dom b1 = (dom q) /\ (dom p) &amp; ( for x being set st x in dom b1 holds
b1 . x = (q . x) '&amp;' (p . x) ) ) ;
idempotence
 for p being boolean-valued Function holds
( dom p = (dom p) /\ (dom p) &amp; ( for x being set st x in dom p holds
p . x = (p . x) '&amp;' (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 &amp; ( for x being set st x in dom p holds
b2 . x = 'not' (p . x) ) ) );

:: deftheorem Def18 defines '&amp;' MARGREL1:def_18_:_
 for p, q, b3 being boolean-valued Function holds
( b3 = p '&amp;' q iff ( dom b3 = (dom p) /\ (dom q) &amp; ( for x being set st x in dom b3 holds
b3 . x = (p . x) '&amp;' (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
proofend;
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
proofend;
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) )
proofend;
let q be Function of A,BOOLEAN;
:: original:'&amp;'
redefine funcp '&amp;' q ->  Function of A,BOOLEAN means :: MARGREL1:def 20
 for x being Element of A holds it . x = (p . x) '&amp;' (q . x);
coherence
 p '&amp;' q is Function of A,BOOLEAN
proofend;
compatibility
 for b1 being Function of A,BOOLEAN holds
( b1 = p '&amp;' q iff for x being Element of A holds b1 . x = (p . x) '&amp;' (q . x) )
proofend;
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 '&amp;' MARGREL1:def_20_:_
 for A being non empty set
for p, q, b4 being Function of A,BOOLEAN holds
( b4 = p '&amp;' q iff for x being Element of A holds b4 . x = (p . x) '&amp;' (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 &amp; 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 &amp; 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
proofend;
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
proofend;
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 &amp; b1 is quasi_total &amp; not b1 is empty )
proofend;
end;

registration
cluster Relation-like Function-like non empty homogeneous for set ;
existence
 ex b1 being Function st
( b1 is homogeneous &amp; not b1 is empty )
proofend;
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
proofend;

theorem :: MARGREL1:19
for A being non empty set
for a being Element of A holds (<*> A) .--> a is Element of PFuncs ((A *),A)
proofend;

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 &amp; 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 &amp; 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 &amp; 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 &amp; 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
proofend;
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 &amp; b1 is quasi_total &amp; b1 is non-empty )
proofend;
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
proofend;
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 &amp; <*x*> is quasi_total &amp; <*x*> is non-empty )
proofend;

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 ) &amp; ( ( for x being FinSequence holds not x in dom f ) implies ex b1 being Nat st b1 = 0 ) )
proofend;
uniqueness
 for b1, b2 being Nat holds
( ( ex x being FinSequence st x in dom f &amp; ( for x being FinSequence st x in dom f holds
b1 = len x ) &amp; ( for x being FinSequence st x in dom f holds
b2 = len x ) implies b1 = b2 ) &amp; ( ( for x being FinSequence holds not x in dom f ) &amp; b1 = 0 &amp; b2 = 0 implies b1 = b2 ) )
proofend;
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 ) ) &amp; ( ( 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
proofend;

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

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