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

begin

definition

let B, A be non empty set ;
let b be Element of B;
:: original: -->
redefine func A --> b -> Element of Funcs (A,B);
coherence
A --> b is Element of Funcs (A,B)

proof 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 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 set ;
existence
ex b₁ being set st
( b₁ is FinSequence-membered & b₁ is with_common_domain )

proof end;

end;

definition

mode relation is FinSequence-membered with_common_domain set ;

end;

theorem :: MARGREL1:1

canceled;

theorem :: MARGREL1:2

canceled;

theorem :: MARGREL1:3

canceled;

theorem :: MARGREL1:4

canceled;

theorem :: MARGREL1:5

canceled;

theorem :: MARGREL1:6

canceled;

theorem :: MARGREL1:7

for X being set
for p being relation st X c= p holds
X is relation ;

theorem :: MARGREL1:8

for a being FinSequence holds {a} is relation

proof end;

scheme :: MARGREL1:sch 1
relexist{ F₁() -> set , P₁[ FinSequence] } :

ex r being relation st
for a being FinSequence holds
( a in r iff ( a in F₁() & P₁[a] ) )

provided

A1: for a, b being FinSequence st P₁[a] & P₁[b] holds
len a = len b

proof 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 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 set ;
coherence
for b₁ being set st b₁ is empty holds
b₁ is with_common_domain

proof end;

end;

theorem Th9: :: MARGREL1:9

for p being relation st ( for a being FinSequence holds not a in p ) holds
p = {}

proof end;

definition

let p be relation;
assume A1: p <> {} ;
canceled;
func the_arity_of p -> Element of NAT means :: MARGREL1:def 4
for a being FinSequence st a in p holds
it = len a;
existence
ex b₁ being Element of NAT st
for a being FinSequence st a in p holds
b₁ = len a

proof end;

uniqueness
for b₁, b₂ being Element of NAT st ( for a being FinSequence st a in p holds
b₁ = len a ) & ( for a being FinSequence st a in p holds
b₂ = len a ) holds
b₁ = b₂

proof end;

end;

:: deftheorem MARGREL1:def 3 :
canceled;

:: deftheorem defines the_arity_of MARGREL1:def 4 :
for p being relation st p <> {} holds
for b₂ being Element of NAT holds
( b₂ = the_arity_of p iff for a being FinSequence st a in p holds
b₂ = len a );

definition

let k be Element of NAT ;
mode relation_length of k -> relation means :: MARGREL1:def 5
for a being FinSequence st a in it holds
len a = k;
existence
ex b₁ being relation st
for a being FinSequence st a in b₁ holds
len a = k

proof end;

end;

:: deftheorem defines relation_length MARGREL1:def 5 :
for k being Element of NAT
for b₂ being relation holds
( b₂ is relation_length of k iff for a being FinSequence st a in b₂ holds
len a = k );

definition

let X be set ;
mode relation of X -> relation means :: MARGREL1:def 6
for a being FinSequence st a in it holds
rng a c= X;
existence
ex b₁ being relation st
for a being FinSequence st a in b₁ holds
rng a c= X

proof end;

end;

:: deftheorem defines relation MARGREL1:def 6 :
for X being set
for b₂ being relation holds
( b₂ is relation of X iff for a being FinSequence st a in b₂ holds
rng a c= X );

theorem :: MARGREL1:10

canceled;

theorem :: MARGREL1:11

canceled;

theorem :: MARGREL1:12

canceled;

theorem :: MARGREL1:13

canceled;

theorem :: MARGREL1:14

canceled;

theorem :: MARGREL1:15

canceled;

theorem :: MARGREL1:16

canceled;

theorem :: MARGREL1:17

canceled;

theorem :: MARGREL1:18

canceled;

theorem :: MARGREL1:19

canceled;

theorem Th20: :: MARGREL1:20

for X being set holds {} is relation of X

proof end;

theorem Th21: :: MARGREL1:21

for k being Element of NAT holds {} is relation_length of k

proof end;

definition

let X be set ;
let k be Element of NAT ;
mode relation of X,k -> relation means :: MARGREL1:def 7
( it is relation of X & it is relation_length of k );
existence
ex b₁ being relation st
( b₁ is relation of X & b₁ is relation_length of k )

proof end;

end;

:: deftheorem defines relation MARGREL1:def 7 :
for X being set
for k being Element of NAT
for b₃ being relation holds
( b₃ is relation of X,k iff ( b₃ is relation of X & b₃ is relation_length of k ) );

definition

let D be non empty set ;
func relations_on D -> set means :Def8: :: MARGREL1:def 8
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 b₁ being set st
for X being set holds
( X in b₁ iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds
len a = len b ) ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for X being set holds
( X in b₁ 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 b₂ iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds
len a = len b ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines relations_on MARGREL1:def 8 :
for D being non empty set
for b₂ being set holds
( b₂ = relations_on D iff for X being set holds
( X in b₂ 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 end;

end;

definition

let D be non empty set ;
mode relation of D is Element of relations_on D;

end;

theorem :: MARGREL1:22

canceled;

theorem :: MARGREL1:23

canceled;

theorem :: MARGREL1:24

canceled;

theorem :: MARGREL1:25

canceled;

theorem :: MARGREL1:26

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

theorem :: MARGREL1:27

for D being non empty set
for a being FinSequence of D holds {a} is Element of relations_on D

proof end;

theorem :: MARGREL1:28

for D being non empty set
for x, y being Element of D holds {<*x,y*>} is Element of relations_on D

proof end;

definition

let D be non empty set ;
let p, r be Element of relations_on D;
:: original: =
redefine pred p = r means :Def9: :: MARGREL1:def 9
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 end;

end;

:: deftheorem Def9 defines = MARGREL1:def 9 :
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{ F₁() -> non empty set , P₁[ FinSequence of F₁()] } :

ex r being Element of relations_on F₁() st
for a being FinSequence of F₁() holds
( a in r iff P₁[a] )

provided

A1: for a, b being FinSequence of F₁() st P₁[a] & P₁[b] holds
len a = len b

proof end;

definition

let D be non empty set ;
func empty_rel D -> Element of relations_on D means :Def10: :: MARGREL1:def 10
for a being FinSequence of D holds not a in it;
existence
ex b₁ being Element of relations_on D st
for a being FinSequence of D holds not a in b₁

proof end;

uniqueness
for b₁, b₂ being Element of relations_on D st ( for a being FinSequence of D holds not a in b₁ ) & ( for a being FinSequence of D holds not a in b₂ ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines empty_rel MARGREL1:def 10 :
for D being non empty set
for b₂ being Element of relations_on D holds
( b₂ = empty_rel D iff for a being FinSequence of D holds not a in b₂ );

theorem :: MARGREL1:29

canceled;

theorem :: MARGREL1:30

canceled;

theorem :: MARGREL1:31

canceled;

theorem :: MARGREL1:32

for D being non empty set holds empty_rel D = {}

proof 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 11
for a being FinSequence of D st a in p holds
it = len a;
existence
ex b₁ being Element of NAT st
for a being FinSequence of D st a in p holds
b₁ = len a

proof end;

uniqueness
for b₁, b₂ being Element of NAT st ( for a being FinSequence of D st a in p holds
b₁ = len a ) & ( for a being FinSequence of D st a in p holds
b₂ = len a ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines the_arity_of MARGREL1:def 11 :
for D being non empty set
for p being Element of relations_on D st p <> empty_rel D holds
for b₃ being Element of NAT holds
( b₃ = the_arity_of p iff for a being FinSequence of D st a in p holds
b₃ = len a );

scheme :: MARGREL1:sch 3
relDexist2{ F₁() -> non empty set , F₂() -> Element of NAT , P₁[ FinSequence of F₁()] } :

ex r being Element of relations_on F₁() st
for a being FinSequence of F₁() st len a = F₂() holds
( a in r iff P₁[a] )

proof end;

definition

func BOOLEAN -> set equals :: MARGREL1:def 12
{0,1};
coherence
{0,1} is set ;

end;

:: deftheorem defines BOOLEAN MARGREL1:def 12 :
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 :Def13: :: MARGREL1:def 13
x in BOOLEAN ;
compatibility
( x is boolean iff x in BOOLEAN )

proof end;

end;

:: deftheorem Def13 defines boolean MARGREL1:def 13 :
for x being set holds
( x is boolean iff x in BOOLEAN );

registration

cluster -> boolean Element of BOOLEAN ;
coherence
for b₁ being Element of BOOLEAN holds b₁ is boolean by Def13;

end;

definition

let v be boolean set ;
redefine func 'not' v equals :: MARGREL1:def 14
TRUE if v = FALSE
otherwise FALSE ;
compatibility
for b₁ being set holds
( ( v = FALSE implies ( b₁ = 'not' v iff b₁ = TRUE ) ) & ( not v = FALSE implies ( b₁ = 'not' v iff b₁ = FALSE ) ) )

proof end;

consistency
for b₁ being set holds verum ;
let w be boolean set ;
redefine func v '&' w equals :: MARGREL1:def 15
TRUE if ( v = TRUE & w = TRUE )
otherwise FALSE ;
compatibility
for b₁ being set holds
( ( v = TRUE & w = TRUE implies ( b₁ = v '&' w iff b₁ = TRUE ) ) & ( ( not v = TRUE or not w = TRUE ) implies ( b₁ = v '&' w iff b₁ = FALSE ) ) )

proof end;

consistency
for b₁ being set holds verum ;

end;

:: deftheorem defines 'not' MARGREL1:def 14 :
for v being boolean set holds
( ( v = FALSE implies 'not' v = TRUE ) & ( not v = FALSE implies 'not' v = FALSE ) );

:: deftheorem defines '&' MARGREL1:def 15 :
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 Def13;
let w be Element of BOOLEAN ;
:: original: '&'
redefine func v '&' w -> Element of BOOLEAN ;
correctness
coherence
v '&' w is Element of BOOLEAN ;
by Def13;

end;

theorem :: MARGREL1:33

canceled;

theorem :: MARGREL1:34

canceled;

theorem :: MARGREL1:35

canceled;

theorem :: MARGREL1:36

canceled;

theorem :: MARGREL1:37

canceled;

theorem :: MARGREL1:38

canceled;

theorem :: MARGREL1:39

canceled;

theorem :: MARGREL1:40

for v being boolean set holds 'not' ('not' v) = v ;

theorem :: MARGREL1:41

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

canceled;

theorem :: MARGREL1:43

canceled;

theorem :: MARGREL1:44

canceled;

theorem :: MARGREL1:45

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

canceled;

theorem :: MARGREL1:47

canceled;

theorem :: MARGREL1:48

canceled;

theorem :: MARGREL1:49

for v being boolean set holds FALSE '&' v = FALSE ;

theorem :: MARGREL1:50

for v being boolean set holds TRUE '&' v = v ;

theorem :: MARGREL1:51

for v being boolean set st v '&' v = FALSE holds
v = FALSE ;

theorem :: MARGREL1:52

for v, w, u being boolean set holds v '&' (w '&' u) = (v '&' w) '&' u ;

definition

let X be set ;
func ALL X -> set equals :Def16: :: MARGREL1:def 16
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 b₁ being set holds verum;
;

end;

:: deftheorem Def16 defines ALL MARGREL1:def 16 :
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 Def16;

end;

definition

let X be set ;
:: original: ALL
redefine func ALL X -> Element of BOOLEAN ;
correctness
coherence
ALL X is Element of BOOLEAN ;
by Def13;

end;

theorem :: MARGREL1:53

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

begin

definition

let f be Function;
attr f is boolean-valued means :Def17: :: MARGREL1:def 17
rng f c= BOOLEAN ;

end;

:: deftheorem Def17 defines boolean-valued MARGREL1:def 17 :
for f being Function holds
( f is boolean-valued iff rng f c= BOOLEAN );

registration

cluster Relation-like Function-like boolean-valued set ;
existence
ex b₁ being Function st b₁ is boolean-valued

proof end;

end;

registration

let f be boolean-valued Function;
let x be set ;
cluster f . x -> boolean ;
coherence
f . x is boolean

proof end;

end;

definition

let p be boolean-valued Function;
func 'not' p -> boolean-valued Function means :Def18: :: MARGREL1:def 18
( dom it = dom p & ( for x being set st x in dom p holds
it . x = 'not' (p . x) ) );
existence
ex b₁ being boolean-valued Function st
( dom b₁ = dom p & ( for x being set st x in dom p holds
b₁ . x = 'not' (p . x) ) )

proof end;

uniqueness
for b₁, b₂ being boolean-valued Function st dom b₁ = dom p & ( for x being set st x in dom p holds
b₁ . x = 'not' (p . x) ) & dom b₂ = dom p & ( for x being set st x in dom p holds
b₂ . x = 'not' (p . x) ) holds
b₁ = b₂

proof end;

involutiveness
for b₁, b₂ being boolean-valued Function st dom b₁ = dom b₂ & ( for x being set st x in dom b₂ holds
b₁ . x = 'not' (b₂ . x) ) holds
( dom b₂ = dom b₁ & ( for x being set st x in dom b₁ holds
b₂ . x = 'not' (b₁ . x) ) )

proof end;

let q be boolean-valued Function;
func p '&' q -> boolean-valued Function means :Def19: :: MARGREL1:def 19
( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds
it . x = (p . x) '&' (q . x) ) );
existence
ex b₁ being boolean-valued Function st
( dom b₁ = (dom p) /\ (dom q) & ( for x being set st x in dom b₁ holds
b₁ . x = (p . x) '&' (q . x) ) )

proof end;

uniqueness
for b₁, b₂ being boolean-valued Function st dom b₁ = (dom p) /\ (dom q) & ( for x being set st x in dom b₁ holds
b₁ . x = (p . x) '&' (q . x) ) & dom b₂ = (dom p) /\ (dom q) & ( for x being set st x in dom b₂ holds
b₂ . x = (p . x) '&' (q . x) ) holds
b₁ = b₂

proof end;

commutativity
for b₁, p, q being boolean-valued Function st dom b₁ = (dom p) /\ (dom q) & ( for x being set st x in dom b₁ holds
b₁ . x = (p . x) '&' (q . x) ) holds
( dom b₁ = (dom q) /\ (dom p) & ( for x being set st x in dom b₁ holds
b₁ . 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 Def18 defines 'not' MARGREL1:def 18 :
for p, b₂ being boolean-valued Function holds
( b₂ = 'not' p iff ( dom b₂ = dom p & ( for x being set st x in dom p holds
b₂ . x = 'not' (p . x) ) ) );

:: deftheorem Def19 defines '&' MARGREL1:def 19 :
for p, q, b₃ being boolean-valued Function holds
( b₃ = p '&' q iff ( dom b₃ = (dom p) /\ (dom q) & ( for x being set st x in dom b₃ holds
b₃ . x = (p . x) '&' (q . x) ) ) );

registration

let A be set ;
cluster -> boolean-valued Element of Funcs (A,BOOLEAN);
coherence
for b₁ being Element of Funcs (A,BOOLEAN) holds b₁ is boolean-valued

proof end;

end;

definition

let A be non empty set ;
let p be Element of Funcs (A,BOOLEAN);
:: original: 'not'
redefine func 'not' p -> Element of Funcs (A,BOOLEAN) means :: MARGREL1:def 20
for x being Element of A holds it . x = 'not' (p . x);
coherence
'not' p is Element of Funcs (A,BOOLEAN)

proof end;

compatibility
for b₁ being Element of Funcs (A,BOOLEAN) holds
( b₁ = 'not' p iff for x being Element of A holds b₁ . x = 'not' (p . x) )

proof end;

let q be Element of Funcs (A,BOOLEAN);
:: original: '&'
redefine func p '&' q -> Element of Funcs (A,BOOLEAN) means :: MARGREL1:def 21
for x being Element of A holds it . x = (p . x) '&' (q . x);
coherence
p '&' q is Element of Funcs (A,BOOLEAN)

proof end;

compatibility
for b₁ being Element of Funcs (A,BOOLEAN) holds
( b₁ = p '&' q iff for x being Element of A holds b₁ . x = (p . x) '&' (q . x) )

proof end;

end;

:: deftheorem defines 'not' MARGREL1:def 20 :
for A being non empty set
for p, b₃ being Element of Funcs (A,BOOLEAN) holds
( b₃ = 'not' p iff for x being Element of A holds b₃ . x = 'not' (p . x) );

:: deftheorem defines '&' MARGREL1:def 21 :
for A being non empty set
for p, q, b₄ being Element of Funcs (A,BOOLEAN) holds
( b₄ = p '&' q iff for x being Element of A holds b₄ . x = (p . x) '&' (q . x) );

begin

definition

let IT be Relation;
attr IT is homogeneous means :Def22: :: MARGREL1:def 22
dom IT is with_common_domain ;

end;

:: deftheorem Def22 defines homogeneous MARGREL1:def 22 :
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;
attr IT is quasi_total means :Def23: :: MARGREL1:def 23
for x, y being FinSequence of A st len x = len y & x in dom IT holds
y in dom IT;

end;

:: deftheorem Def23 defines quasi_total MARGREL1:def 23 :
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 ;
cluster f | X -> homogeneous ;
coherence
f | X is homogeneous

proof end;

end;

registration

let A be non empty set ;
let f be PartFunc of (A *),A;
cluster proj1 f -> FinSequence-membered ;
coherence
dom f is FinSequence-membered

proof end;

end;

registration

let A be non empty set ;
cluster Relation-like A * -defined A -valued Function-like non empty homogeneous quasi_total Element of bool [:(A *),A:];
existence
ex b₁ being PartFunc of (A *),A st
( b₁ is homogeneous & b₁ is quasi_total & not b₁ is empty )

proof end;

end;

registration

cluster Relation-like Function-like non empty homogeneous set ;
existence
ex b₁ being Function st
( b₁ is homogeneous & not b₁ is empty )

proof end;

end;

registration

let R be homogeneous Relation;
cluster proj1 R -> with_common_domain ;
coherence
dom R is with_common_domain by Def22;

end;

theorem Th54: :: MARGREL1:54

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

theorem :: MARGREL1:55

for A being non empty set
for a being Element of A holds (<*> A) .--> a is Element of PFuncs ((A *),A)

proof 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;
attr IT is homogeneous 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 homogeneous ;

end;

:: deftheorem Def24 defines homogeneous MARGREL1:def 24 :
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;
attr IT is quasi_total means :Def25: :: MARGREL1:def 25
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 Def25 defines quasi_total MARGREL1:def 25 :
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 end;

end;

registration

let A be non empty set ;
cluster Relation-like non-empty NAT -defined PFuncs ((A *),A) -valued Function-like Function-yielding V27() FinSequence-like FinSubsequence-like countable homogeneous quasi_total FinSequence of PFuncs ((A *),A);
existence
ex b₁ being PFuncFinSequence of A st
( b₁ is homogeneous & b₁ is quasi_total & b₁ is non-empty )

proof end;

end;

registration

let A be non empty set ;
let f be homogeneous PFuncFinSequence of A;
let i be set ;
cluster f . i -> homogeneous ;
coherence
f . i is homogeneous

proof end;

end;

theorem :: MARGREL1:56

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

definition

let f be homogeneous Relation;
func arity f -> Nat means :Def26: :: MARGREL1:def 26
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 b₁ being Nat holds verum ;
existence
( ( ex x being FinSequence st x in dom f implies ex b₁ being Nat st
for x being FinSequence st x in dom f holds
b₁ = len x ) & ( ( for x being FinSequence holds not x in dom f ) implies ex b₁ being Nat st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being Nat holds
( ( ex x being FinSequence st x in dom f & ( for x being FinSequence st x in dom f holds
b₁ = len x ) & ( for x being FinSequence st x in dom f holds
b₂ = len x ) implies b₁ = b₂ ) & ( ( for x being FinSequence holds not x in dom f ) & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) )

proof end;

end;

:: deftheorem Def26 defines arity MARGREL1:def 26 :
for f being homogeneous Relation
for b₂ being Nat holds
( ( ex x being FinSequence st x in dom f implies ( b₂ = arity f iff for x being FinSequence st x in dom f holds
b₂ = len x ) ) & ( ( for x being FinSequence holds not x in dom f ) implies ( b₂ = arity f iff b₂ = 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 13;

end;

begin

theorem :: MARGREL1:57

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

theorem :: MARGREL1:58

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

definition

let D be non empty set ;
mode PFuncsDomHQN of D -> non empty set means :Def27: :: MARGREL1:def 27
for x being Element of it holds x is non empty homogeneous quasi_total PartFunc of (D *),D;
existence
ex b₁ being non empty set st
for x being Element of b₁ holds x is non empty homogeneous quasi_total PartFunc of (D *),D

proof end;

end;

:: deftheorem Def27 defines PFuncsDomHQN MARGREL1:def 27 :
for D, b₂ being non empty set holds
( b₂ is PFuncsDomHQN of D iff for x being Element of b₂ 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 b₁ being Element of P holds b₁ is non empty homogeneous quasi_total PartFunc of (D *),D by Def27;

end;