:: by Edmund Woronowicz

::

:: Received June 1, 1990

:: Copyright (c) 1990-2019 Association of Mizar Users

definition

let IT be FinSequence-membered set ;

( IT is with_common_domain iff for a, b being FinSequence st a in IT & b in IT holds

len a = len b )

end;
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 for a, b being FinSequence st a in IT & b in IT holds

len a = len b;

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

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

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

existence

ex b_{1} being set st

( b_{1} is FinSequence-membered & b_{1} is with_common_domain )

end;
ex b

( b

proof end;

definition

let p, r be relation;

compatibility

( p = r iff for a being FinSequence holds

( a in p iff a in r ) )

end;
compatibility

( p = r iff for a being FinSequence holds

( a in p iff a in r ) )

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

for p, r being relation holds

( p = r iff for a being FinSequence holds

( a in p iff a in r ) );

registration
end;

theorem :: MARGREL1:3

definition

let p be relation;

assume A1: p <> {} ;

ex b_{1} being Element of NAT st

for a being FinSequence st a in p holds

b_{1} = len a

for b_{1}, b_{2} being Element of NAT st ( for a being FinSequence st a in p holds

b_{1} = len a ) & ( for a being FinSequence st a in p holds

b_{2} = len a ) holds

b_{1} = b_{2}

end;
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 for a being FinSequence st a in p holds

it = len a;

ex b

for a being FinSequence st a in p holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines the_arity_of MARGREL1:def 3 :

for p being relation st p <> {} holds

for b_{2} being Element of NAT holds

( b_{2} = the_arity_of p iff for a being FinSequence st a in p holds

b_{2} = len a );

for p being relation st p <> {} holds

for b

( b

b

definition

let k be Element of NAT ;

ex b_{1} being relation st

for a being FinSequence st a in b_{1} holds

len a = k

end;
mode relation_length of k -> relation means :: MARGREL1:def 4

for a being FinSequence st a in it holds

len a = k;

existence for a being FinSequence st a in it holds

len a = k;

ex b

for a being FinSequence st a in b

len a = k

proof end;

:: deftheorem defines relation_length MARGREL1:def 4 :

for k being Element of NAT

for b_{2} being relation holds

( b_{2} is relation_length of k iff for a being FinSequence st a in b_{2} holds

len a = k );

for k being Element of NAT

for b

( b

len a = k );

definition

let X be set ;

ex b_{1} being relation st

for a being FinSequence st a in b_{1} holds

rng a c= X

end;
mode relation of X -> relation means :: MARGREL1:def 5

for a being FinSequence st a in it holds

rng a c= X;

existence for a being FinSequence st a in it holds

rng a c= X;

ex b

for a being FinSequence st a in b

rng a c= X

proof end;

:: deftheorem defines relation MARGREL1:def 5 :

for X being set

for b_{2} being relation holds

( b_{2} is relation of X iff for a being FinSequence st a in b_{2} holds

rng a c= X );

for X being set

for b

( b

rng a c= X );

definition

let X be set ;

let k be Element of NAT ;

ex b_{1} being relation st

( b_{1} is relation of X & b_{1} is relation_length of k )

end;
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 ( it is relation of X & it is relation_length of k );

ex b

( b

proof end;

:: deftheorem defines relation MARGREL1:def 6 :

for X being set

for k being Element of NAT

for b_{3} being relation holds

( b_{3} is relation of X,k iff ( b_{3} is relation of X & b_{3} is relation_length of k ) );

for X being set

for k being Element of NAT

for b

( b

definition

let D be non empty set ;

ex b_{1} being set st

for X being set holds

( X in b_{1} iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds

len a = len b ) ) )

for b_{1}, b_{2} being set st ( for X being set holds

( X in b_{1} 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_{2} 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_{1} = b_{2}

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

ex b

for X being set holds

( X in b

len a = len b ) ) )

proof end;

uniqueness for b

( X in b

len a = len b ) ) ) ) & ( for X being set holds

( X in b

len a = len b ) ) ) ) holds

b

proof end;

:: deftheorem Def7 defines relations_on MARGREL1:def 7 :

for D being non empty set

for b_{2} being set holds

( b_{2} = relations_on D iff for X being set holds

( X in b_{2} iff ( X c= D * & ( for a, b being FinSequence of D st a in X & b in X holds

len a = len b ) ) ) );

for D being non empty set

for b

( b

( X in b

len a = len b ) ) ) );

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

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;

definition

let D be non empty set ;

let p, r be Element of relations_on D;

( p = r iff for a being FinSequence of D holds

( a in p iff a in r ) )

end;
let p, r be Element of relations_on D;

:: original: =

redefine pred p = r means :: MARGREL1:def 8

for a being FinSequence of D holds

( a in p iff a in r );

compatibility redefine pred p = r means :: MARGREL1:def 8

for a being FinSequence of D holds

( a in p iff a in r );

( p = r iff for a being FinSequence of D holds

( a in p iff a in r ) )

proof end;

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

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_{1}() -> non empty set , P_{1}[ FinSequence of F_{1}()] } :

relDexist{ F

ex r being Element of relations_on F_{1}() st

for a being FinSequence of F_{1}() holds

( a in r iff P_{1}[a] )

provided
for a being FinSequence of F

( a in r iff P

proof end;

definition

let D be non empty set ;

ex b_{1} being Element of relations_on D st

for a being FinSequence of D holds not a in b_{1}

for b_{1}, b_{2} being Element of relations_on D st ( for a being FinSequence of D holds not a in b_{1} ) & ( for a being FinSequence of D holds not a in b_{2} ) holds

b_{1} = b_{2}
;

end;
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 for a being FinSequence of D holds not a in it;

ex b

for a being FinSequence of D holds not a in b

proof end;

uniqueness for b

b

:: deftheorem Def9 defines empty_rel MARGREL1:def 9 :

for D being non empty set

for b_{2} being Element of relations_on D holds

( b_{2} = empty_rel D iff for a being FinSequence of D holds not a in b_{2} );

for D being non empty set

for b

( b

definition

let D be non empty set ;

let p be Element of relations_on D;

assume A1: p <> empty_rel D ;

ex b_{1} being Element of NAT st

for a being FinSequence of D st a in p holds

b_{1} = len a

for b_{1}, b_{2} being Element of NAT st ( for a being FinSequence of D st a in p holds

b_{1} = len a ) & ( for a being FinSequence of D st a in p holds

b_{2} = len a ) holds

b_{1} = b_{2}

end;
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 for a being FinSequence of D st a in p holds

it = len a;

ex b

for a being FinSequence of D st a in p holds

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{3} being Element of NAT holds

( b_{3} = the_arity_of p iff for a being FinSequence of D st a in p holds

b_{3} = len a );

for D being non empty set

for p being Element of relations_on D st p <> empty_rel D holds

for b

( b

b

scheme :: MARGREL1:sch 3

relDexist2{ F_{1}() -> non empty set , F_{2}() -> Element of NAT , P_{1}[ FinSequence of F_{1}()] } :

relDexist2{ F

ex r being Element of relations_on F_{1}() st

for a being FinSequence of F_{1}() st len a = F_{2}() holds

( a in r iff P_{1}[a] )

for a being FinSequence of F

( a in r iff P

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

:: deftheorem Def12 defines boolean MARGREL1:def 12 :

for x being object holds

( x is boolean iff x in BOOLEAN );

for x being object holds

( x is boolean iff x in BOOLEAN );

definition

let v be boolean object ;

compatibility

for b_{1} being object holds

( ( v = FALSE implies ( b_{1} = 'not' v iff b_{1} = TRUE ) ) & ( not v = FALSE implies ( b_{1} = 'not' v iff b_{1} = FALSE ) ) )

for b_{1} being object holds verum
;

let w be boolean object ;

compatibility

for b_{1} being object holds

( ( v = TRUE & w = TRUE implies ( b_{1} = v '&' w iff b_{1} = TRUE ) ) & ( ( not v = TRUE or not w = TRUE ) implies ( b_{1} = v '&' w iff b_{1} = FALSE ) ) )

for b_{1} being object holds verum
;

end;
compatibility

for b

( ( v = FALSE implies ( b

proof end;

consistency for b

let w be boolean object ;

compatibility

for b

( ( v = TRUE & w = TRUE implies ( b

proof end;

consistency for b

:: deftheorem defines 'not' MARGREL1:def 13 :

for v being boolean object holds

( ( v = FALSE implies 'not' v = TRUE ) & ( not v = FALSE implies 'not' v = FALSE ) );

for v being boolean object holds

( ( v = FALSE implies 'not' v = TRUE ) & ( not v = FALSE implies 'not' v = FALSE ) );

:: deftheorem defines '&' MARGREL1:def 14 :

for v, w being boolean object holds

( ( v = TRUE & w = TRUE implies v '&' w = TRUE ) & ( ( not v = TRUE or not w = TRUE ) implies v '&' w = FALSE ) );

for v, w being boolean object 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 func v '&' w -> Element of BOOLEAN ;

correctness

coherence

v '&' w is Element of BOOLEAN ;

by Def12;

end;
:: 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 func v '&' w -> Element of BOOLEAN ;

correctness

coherence

v '&' w is Element of BOOLEAN ;

by Def12;

::$CT

theorem :: MARGREL1:11

theorem :: MARGREL1:12

definition

let X be set ;

correctness

coherence

( ( not FALSE in X implies TRUE is set ) & ( FALSE in X implies FALSE is set ) );

consistency

for b_{1} being set holds verum;

;

end;
correctness

coherence

( ( not FALSE in X implies TRUE is set ) & ( FALSE in X implies FALSE is set ) );

consistency

for b

;

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

for X being set holds

( ( not FALSE in X implies ALL X = TRUE ) & ( FALSE in X implies ALL X = FALSE ) );

registration
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;
:: original: ALL

redefine func ALL X -> Element of BOOLEAN ;

correctness

coherence

ALL X is Element of BOOLEAN ;

by Def12;

theorem :: MARGREL1:17

:: from VALUAT_1, 2007.03.15, A.T.

definition
end;

:: deftheorem Def16 defines boolean-valued MARGREL1:def 16 :

for f being Relation holds

( f is boolean-valued iff rng f c= BOOLEAN );

for f being Relation holds

( f is boolean-valued iff rng f c= BOOLEAN );

registration
end;

definition

let p be boolean-valued Function;

ex b_{1} being boolean-valued Function st

( dom b_{1} = dom p & ( for x being object st x in dom p holds

b_{1} . x = 'not' (p . x) ) )

for b_{1}, b_{2} being boolean-valued Function st dom b_{1} = dom p & ( for x being object st x in dom p holds

b_{1} . x = 'not' (p . x) ) & dom b_{2} = dom p & ( for x being object st x in dom p holds

b_{2} . x = 'not' (p . x) ) holds

b_{1} = b_{2}

for b_{1}, b_{2} being boolean-valued Function st dom b_{1} = dom b_{2} & ( for x being object st x in dom b_{2} holds

b_{1} . x = 'not' (b_{2} . x) ) holds

( dom b_{2} = dom b_{1} & ( for x being object st x in dom b_{1} holds

b_{2} . x = 'not' (b_{1} . x) ) )

ex b_{1} being boolean-valued Function st

( dom b_{1} = (dom p) /\ (dom q) & ( for x being object st x in dom b_{1} holds

b_{1} . x = (p . x) '&' (q . x) ) )

for b_{1}, b_{2} being boolean-valued Function st dom b_{1} = (dom p) /\ (dom q) & ( for x being object st x in dom b_{1} holds

b_{1} . x = (p . x) '&' (q . x) ) & dom b_{2} = (dom p) /\ (dom q) & ( for x being object st x in dom b_{2} holds

b_{2} . x = (p . x) '&' (q . x) ) holds

b_{1} = b_{2}

for b_{1}, p, q being boolean-valued Function st dom b_{1} = (dom p) /\ (dom q) & ( for x being object st x in dom b_{1} holds

b_{1} . x = (p . x) '&' (q . x) ) holds

( dom b_{1} = (dom q) /\ (dom p) & ( for x being object st x in dom b_{1} holds

b_{1} . x = (q . x) '&' (p . x) ) )
;

idempotence

for p being boolean-valued Function holds

( dom p = (dom p) /\ (dom p) & ( for x being object st x in dom p holds

p . x = (p . x) '&' (p . x) ) ) ;

end;
func 'not' p -> boolean-valued Function means :Def17: :: MARGREL1:def 17

( dom it = dom p & ( for x being object st x in dom p holds

it . x = 'not' (p . x) ) );

existence ( dom it = dom p & ( for x being object st x in dom p holds

it . x = 'not' (p . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

involutiveness for b

b

( dom b

b

proof end;

let q be boolean-valued Function;
func p '&' q -> boolean-valued Function means :Def18: :: MARGREL1:def 18

( dom it = (dom p) /\ (dom q) & ( for x being object st x in dom it holds

it . x = (p . x) '&' (q . x) ) );

existence ( dom it = (dom p) /\ (dom q) & ( for x being object st x in dom it holds

it . x = (p . x) '&' (q . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

commutativity for b

b

( dom b

b

idempotence

for p being boolean-valued Function holds

( dom p = (dom p) /\ (dom p) & ( for x being object st x in dom p holds

p . x = (p . x) '&' (p . x) ) ) ;

:: deftheorem Def17 defines 'not' MARGREL1:def 17 :

for p, b_{2} being boolean-valued Function holds

( b_{2} = 'not' p iff ( dom b_{2} = dom p & ( for x being object st x in dom p holds

b_{2} . x = 'not' (p . x) ) ) );

for p, b

( b

b

:: deftheorem Def18 defines '&' MARGREL1:def 18 :

for p, q, b_{3} being boolean-valued Function holds

( b_{3} = p '&' q iff ( dom b_{3} = (dom p) /\ (dom q) & ( for x being object st x in dom b_{3} holds

b_{3} . x = (p . x) '&' (q . x) ) ) );

for p, q, b

( b

b

registration

let A be set ;

coherence

for b_{1} being Function of A,BOOLEAN holds b_{1} is boolean-valued
by RELAT_1:def 19;

end;
coherence

for b

definition

let A be non empty set ;

let p be Function of A,BOOLEAN;

'not' p is Function of A,BOOLEAN

for b_{1} being Function of A,BOOLEAN holds

( b_{1} = 'not' p iff for x being Element of A holds b_{1} . x = 'not' (p . x) )

p '&' q is Function of A,BOOLEAN

for b_{1} being Function of A,BOOLEAN holds

( b_{1} = p '&' q iff for x being Element of A holds b_{1} . x = (p . x) '&' (q . x) )

end;
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 redefine func 'not' p -> Function of A,BOOLEAN means :: MARGREL1:def 19

for x being Element of A holds it . x = 'not' (p . x);

'not' p is Function of A,BOOLEAN

proof end;

compatibility for b

( b

proof end;

let q be Function of A,BOOLEAN;
:: original: '&'

redefine func p '&' q -> Function of A,BOOLEAN means :: MARGREL1:def 20

for x being Element of A holds it . x = (p . x) '&' (q . x);

coherence redefine func p '&' q -> Function of A,BOOLEAN means :: MARGREL1:def 20

for x being Element of A holds it . x = (p . x) '&' (q . x);

p '&' q is Function of A,BOOLEAN

proof end;

compatibility for b

( b

proof end;

:: deftheorem defines 'not' MARGREL1:def 19 :

for A being non empty set

for p, b_{3} being Function of A,BOOLEAN holds

( b_{3} = 'not' p iff for x being Element of A holds b_{3} . x = 'not' (p . x) );

for A being non empty set

for p, b

( b

:: deftheorem defines '&' MARGREL1:def 20 :

for A being non empty set

for p, q, b_{4} being Function of A,BOOLEAN holds

( b_{4} = p '&' q iff for x being Element of A holds b_{4} . x = (p . x) '&' (q . x) );

for A being non empty set

for p, q, b

( b

:: deftheorem Def21 defines homogeneous MARGREL1:def 21 :

for IT being Relation holds

( IT is homogeneous iff dom IT is with_common_domain );

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;

end;
let IT be PartFunc of (A *),A;

attr IT 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;

for x, y being FinSequence of A st len x = len y & x in dom IT holds

y in dom IT;

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

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

registration

let A be non empty set ;

let f be PartFunc of (A *),A;

coherence

dom f is FinSequence-membered

end;
let f be PartFunc of (A *),A;

coherence

dom f is FinSequence-membered

proof end;

registration

let A be non empty set ;

ex b_{1} being PartFunc of (A *),A st

( b_{1} is homogeneous & b_{1} is quasi_total & not b_{1} is empty )

end;
cluster Relation-like A * -defined A -valued Function-like non empty homogeneous quasi_total for Element of bool [:(A *),A:];

existence ex b

( b

proof end;

registration
end;

theorem Th17: :: 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

for a being Element of A holds (<*> A) .--> a is non empty homogeneous quasi_total PartFunc of (A *),A

proof 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)

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

proof end;

definition

let A be set ;

let IT be PFuncFinSequence of A;

end;
let IT be PFuncFinSequence of A;

attr IT 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 ;

for n being Nat

for h being PartFunc of (A *),A st n in dom IT & h = IT . n holds

h is homogeneous ;

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

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;

end;
let IT be PFuncFinSequence of A;

attr IT is quasi_total means :: 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 ;

for n being Nat

for h being PartFunc of (A *),A st n in dom IT & h = IT . n holds

h is quasi_total ;

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

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

end;
let x be Element of PFuncs ((A *),A);

:: original: <*

redefine func <*x*> -> PFuncFinSequence of A;

coherence

<*x*> is PFuncFinSequence of A

proof end;

registration

let A be non empty set ;

ex b_{1} being PFuncFinSequence of A st

( b_{1} is homogeneous & b_{1} is quasi_total & b_{1} is non-empty )

end;
cluster Relation-like non-empty NAT -defined PFuncs ((A *),A) -valued Function-like Function-yielding V22() V34() FinSequence-like FinSubsequence-like countable homogeneous quasi_total for FinSequence of PFuncs ((A *),A);

existence ex b

( b

proof end;

registration

let A be non empty set ;

let f be homogeneous PFuncFinSequence of A;

let i be set ;

coherence

f . i is homogeneous

end;
let f be homogeneous PFuncFinSequence of A;

let i be set ;

coherence

f . i is homogeneous

proof 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 )

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;

for b_{1} being Nat holds verum
;

existence

( ( ex x being FinSequence st x in dom f implies ex b_{1} being Nat st

for x being FinSequence st x in dom f holds

b_{1} = len x ) & ( ( for x being FinSequence holds not x in dom f ) implies ex b_{1} being Nat st b_{1} = 0 ) )

for b_{1}, b_{2} being Nat holds

( ( ex x being FinSequence st x in dom f & ( for x being FinSequence st x in dom f holds

b_{1} = len x ) & ( for x being FinSequence st x in dom f holds

b_{2} = len x ) implies b_{1} = b_{2} ) & ( ( for x being FinSequence holds not x in dom f ) & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

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

for b

existence

( ( ex x being FinSequence st x in dom f implies ex b

for x being FinSequence st x in dom f holds

b

proof end;

uniqueness for b

( ( ex x being FinSequence st x in dom f & ( for x being FinSequence st x in dom f holds

b

b

proof end;

:: deftheorem Def25 defines arity MARGREL1:def 25 :

for f being homogeneous Relation

for b_{2} being Nat holds

( ( ex x being FinSequence st x in dom f implies ( b_{2} = arity f iff for x being FinSequence st x in dom f holds

b_{2} = len x ) ) & ( ( for x being FinSequence holds not x in dom f ) implies ( b_{2} = arity f iff b_{2} = 0 ) ) );

for f being homogeneous Relation

for b

( ( ex x being FinSequence st x in dom f implies ( b

b

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

redefine func arity f -> Element of NAT ;

coherence

arity f is Element of NAT by ORDINAL1:def 12;

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

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

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 ;

ex b_{1} being non empty set st

for x being Element of b_{1} holds x is non empty homogeneous quasi_total PartFunc of (D *),D

end;
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 for x being Element of it holds x is non empty homogeneous quasi_total PartFunc of (D *),D;

ex b

for x being Element of b

proof end;

:: deftheorem Def26 defines PFuncsDomHQN MARGREL1:def 26 :

for D, b_{2} being non empty set holds

( b_{2} is PFuncsDomHQN of D iff for x being Element of b_{2} holds x is non empty homogeneous quasi_total PartFunc of (D *),D );

for D, b

( b

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_{1} being Element of P holds b_{1} is non empty homogeneous quasi_total PartFunc of (D *),D
by Def26;

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