:: by Marco B. Caminati

::

:: Received December 29, 2010

:: Copyright (c) 2010-2021 Association of Mizar Users

:: deftheorem defines -one-to-one FOMODEL0:def 1 :

for X being set

for f being Function holds

( f is X -one-to-one iff f | X is one-to-one );

for X being set

for f being Function holds

( f is X -one-to-one iff f | X is one-to-one );

:: deftheorem defines -unambiguous FOMODEL0:def 2 :

for D being non empty set

for f being BinOp of D

for X being set holds

( X is f -unambiguous iff f is [:X,D:] -one-to-one );

for D being non empty set

for f being BinOp of D

for X being set holds

( X is f -unambiguous iff f is [:X,D:] -one-to-one );

:: deftheorem defines -prefix FOMODEL0:def 3 :

for D being non empty set

for X being set holds

( X is D -prefix iff X is D -concatenation -unambiguous );

for D being non empty set

for X being set holds

( X is D -prefix iff X is D -concatenation -unambiguous );

definition

let f be Function-yielding Function;

let g be Function;

ex b_{1} being Function st

( dom b_{1} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (f . x) . (g . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{1} holds

b_{1} . x = (f . x) . (g . x) ) & dom b_{2} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{2} holds

b_{2} . x = (f . x) . (g . x) ) holds

b_{1} = b_{2}

end;
let g be Function;

func ^^^f,g__ -> Function means :: FOMODEL0:def 4

( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds

it . x = (f . x) . (g . x) ) );

existence ( dom it = (dom f) /\ (dom g) & ( for x being set st x in dom it holds

it . x = (f . x) . (g . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines ^^^ FOMODEL0:def 4 :

for f being Function-yielding Function

for g, b_{3} being Function holds

( b_{3} = ^^^f,g__ iff ( dom b_{3} = (dom f) /\ (dom g) & ( for x being set st x in dom b_{3} holds

b_{3} . x = (f . x) . (g . x) ) ) );

for f being Function-yielding Function

for g, b

( b

b

Lm1: for Y being set

for g being Function st g is Y -valued & g is FinSequence-like holds

g is FinSequence of Y

by FINSEQ_1:def 4;

Lm2: for A, B, Y being set st Y c= Funcs (A,B) holds

union Y c= [:A,B:]

proof end;

Lm3: for X being set

for f being Function holds

( f is X -one-to-one iff for x, y being set st x in (dom f) /\ X & y in (dom f) /\ X & f . x = f . y holds

x = y )

proof end;

Lm4: for A, B being set

for D being non empty set

for f being BinOp of D st A c= B & f is B -one-to-one holds

f is A -one-to-one

proof end;

Lm5: for A, B being set

for m, n being Nat st m -tuples_on A meets n -tuples_on B holds

m = n

proof end;

Lm6: for D being set holds 0 -tuples_on D = {{}}

proof end;

Lm7: for i being Nat

for Y being set holds i -tuples_on Y = Funcs ((Seg i),Y)

proof end;

Lm8: for A, B being set

for m being Nat holds (m -tuples_on A) /\ (B *) c= m -tuples_on B

proof end;

theorem Th1: :: FOMODEL0:1

for A, B being set

for m being Nat holds (m -tuples_on A) /\ (B *) = (m -tuples_on A) /\ (m -tuples_on B)

for m being Nat holds (m -tuples_on A) /\ (B *) = (m -tuples_on A) /\ (m -tuples_on B)

proof end;

Lm9: for A, B, C being set holds (Funcs (A,B)) /\ (Funcs (A,C)) = Funcs (A,(B /\ C))

proof end;

theorem Th3: :: FOMODEL0:3

for A, B being set

for m being Nat holds m -tuples_on (A /\ B) = (m -tuples_on A) /\ (m -tuples_on B)

for m being Nat holds m -tuples_on (A /\ B) = (m -tuples_on A) /\ (m -tuples_on B)

proof end;

Lm10: for D being non empty set

for x, y being FinSequence of D holds (D -concatenation) . (x,y) = x ^ y

proof end;

theorem Th4: :: FOMODEL0:4

for U being non empty set

for x, y being FinSequence st x is U -valued & y is U -valued holds

(U -concatenation) . (x,y) = x ^ y

for x, y being FinSequence st x is U -valued & y is U -valued holds

(U -concatenation) . (x,y) = x ^ y

proof end;

theorem Th5: :: FOMODEL0:5

for D being non empty set

for x being set holds

( x is non empty FinSequence of D iff x in (D *) \ {{}} )

for x being set holds

( x is non empty FinSequence of D iff x in (D *) \ {{}} )

proof end;

Lm11: for A, B being set

for D being non empty set

for f being BinOp of D st B is f -unambiguous & A c= B holds

A is f -unambiguous

proof end;

Lm12: for D being non empty set

for f being BinOp of D holds {} is f -unambiguous

proof end;

Lm13: for f, g being FinSequence holds dom <:f,g:> = Seg (min ((len f),(len g)))

proof end;

::##################### Preliminary lemmas ############################

::############################## END ##################################

::############################ Type tuning ############################

::############################## END ##################################

::############################ Type tuning ############################

registration

let D be non empty set ;

coherence

for b_{1} being BinOp of D st b_{1} = D -pr1 holds

b_{1} is associative

end;
coherence

for b

b

proof end;

registration

let D be set ;

ex b_{1} being BinOp of D st b_{1} is associative

end;
cluster Relation-like [:D,D:] -defined D -valued Function-like total quasi_total associative for Element of bool [:[:D,D:],D:];

existence ex b

proof end;

definition

let X be set ;

let Y be Subset of X;

:: original: *

redefine func Y * -> non empty Subset of (X *);

coherence

Y * is non empty Subset of (X *) by FINSEQ_1:62;

end;
let Y be Subset of X;

:: original: *

redefine func Y * -> non empty Subset of (X *);

coherence

Y * is non empty Subset of (X *) by FINSEQ_1:62;

registration

let D be non empty set ;

coherence

for b_{1} being BinOp of (D *) st b_{1} = D -concatenation holds

b_{1} is associative
by MONOID_0:67;

end;
coherence

for b

b

registration

let D be non empty set ;

let m be Nat;

ex b_{1} being Element of D * st b_{1} is m -element

end;
let m be Nat;

cluster Relation-like omega -defined D -valued Function-like finite m -element FinSequence-like FinSubsequence-like countable finite-support for Element of D * ;

existence ex b

proof end;

definition

let X be set ;

let f be Function;

( f is X -one-to-one iff for x, y being set st x in X /\ (dom f) & y in X /\ (dom f) & f . x = f . y holds

x = y ) by Lm3;

end;
let f be Function;

redefine attr f is X -one-to-one means :Def6: :: FOMODEL0:def 6

for x, y being set st x in X /\ (dom f) & y in X /\ (dom f) & f . x = f . y holds

x = y;

compatibility for x, y being set st x in X /\ (dom f) & y in X /\ (dom f) & f . x = f . y holds

x = y;

( f is X -one-to-one iff for x, y being set st x in X /\ (dom f) & y in X /\ (dom f) & f . x = f . y holds

x = y ) by Lm3;

:: deftheorem Def6 defines -one-to-one FOMODEL0:def 6 :

for X being set

for f being Function holds

( f is X -one-to-one iff for x, y being set st x in X /\ (dom f) & y in X /\ (dom f) & f . x = f . y holds

x = y );

for X being set

for f being Function holds

( f is X -one-to-one iff for x, y being set st x in X /\ (dom f) & y in X /\ (dom f) & f . x = f . y holds

x = y );

registration

let D be non empty set ;

let f be BinOp of D;

existence

ex b_{1} being set st b_{1} is f -unambiguous

end;
let f be BinOp of D;

existence

ex b

proof end;

registration

let f be Function;

let x be set ;

coherence

for b_{1} being Function st b_{1} = f | {x} holds

b_{1} is one-to-one

end;
let x be set ;

coherence

for b

b

proof end;

registration
end;

registration

coherence

for b_{1} being set st b_{1} is empty holds

b_{1} is empty-membered
;

let e be empty set ;

coherence

{e} is empty-membered

end;
for b

b

let e be empty set ;

coherence

{e} is empty-membered

proof end;

registration

let U be non empty set ;

let m1 be non zero Nat;

coherence

m1 -tuples_on U is with_non-empty_elements

end;
let m1 be non zero Nat;

coherence

m1 -tuples_on U is with_non-empty_elements

proof end;

registration

let X be empty-membered set ;

coherence

for b_{1} being Subset of X holds b_{1} is empty-membered

end;
coherence

for b

proof end;

registration

let A be set ;

let m0 be zero number ;

coherence

for b_{1} being set st b_{1} = m0 -tuples_on A holds

b_{1} is empty-membered
by Lm6;

end;
let m0 be zero number ;

coherence

for b

b

registration

let e be empty set ;

let m1 be non zero Nat;

coherence

for b_{1} being set st b_{1} = m1 -tuples_on e holds

b_{1} is empty
by FINSEQ_3:119;

end;
let m1 be non zero Nat;

coherence

for b

b

registration

let D be non empty set ;

let f be BinOp of D;

let e be empty set ;

coherence

for b_{1} being set st b_{1} = e /\ f holds

b_{1} is f -unambiguous
by Lm12;

end;
let f be BinOp of D;

let e be empty set ;

coherence

for b

b

registration

let U be non empty set ;

let e be empty set ;

coherence

for b_{1} being set st b_{1} = e /\ U holds

b_{1} is U -prefix

end;
let e be empty set ;

coherence

for b

b

proof end;

registration
end;

::############################ Type tuning ############################

::############################## END ##################################

::########################### MultPlace ###############################

::############################## END ##################################

::########################### MultPlace ###############################

definition

let D be non empty set ;

let f be BinOp of D;

let x be FinSequence of D;

ex b_{1} being Function st

( dom b_{1} = NAT & b_{1} . 0 = x . 1 & ( for n being Nat holds b_{1} . (n + 1) = f . ((b_{1} . n),(x . (n + 2))) ) )

for b_{1}, b_{2} being Function st dom b_{1} = NAT & b_{1} . 0 = x . 1 & ( for n being Nat holds b_{1} . (n + 1) = f . ((b_{1} . n),(x . (n + 2))) ) & dom b_{2} = NAT & b_{2} . 0 = x . 1 & ( for n being Nat holds b_{2} . (n + 1) = f . ((b_{2} . n),(x . (n + 2))) ) holds

b_{1} = b_{2}

end;
let f be BinOp of D;

let x be FinSequence of D;

func MultPlace (f,x) -> Function means :Def7: :: FOMODEL0:def 7

( dom it = NAT & it . 0 = x . 1 & ( for n being Nat holds it . (n + 1) = f . ((it . n),(x . (n + 2))) ) );

existence ( dom it = NAT & it . 0 = x . 1 & ( for n being Nat holds it . (n + 1) = f . ((it . n),(x . (n + 2))) ) );

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines MultPlace FOMODEL0:def 7 :

for D being non empty set

for f being BinOp of D

for x being FinSequence of D

for b_{4} being Function holds

( b_{4} = MultPlace (f,x) iff ( dom b_{4} = NAT & b_{4} . 0 = x . 1 & ( for n being Nat holds b_{4} . (n + 1) = f . ((b_{4} . n),(x . (n + 2))) ) ) );

for D being non empty set

for f being BinOp of D

for x being FinSequence of D

for b

( b

Lm14: for D being non empty set

for f being BinOp of D

for x being FinSequence of D

for m being Nat holds

( ( m + 1 <= len x implies (MultPlace (f,x)) . m in D ) & ( for n being Nat st n >= m + 1 holds

(MultPlace (f,(x | n))) . m = (MultPlace (f,x)) . m ) )

proof end;

definition

let D be non empty set ;

let f be BinOp of D;

let x be Element of (D *) \ {{}};

coherence

MultPlace (f,x) is Function ;

end;
let f be BinOp of D;

let x be Element of (D *) \ {{}};

coherence

MultPlace (f,x) is Function ;

:: deftheorem defines MultPlace FOMODEL0:def 8 :

for D being non empty set

for f being BinOp of D

for x being Element of (D *) \ {{}} holds MultPlace (f,x) = MultPlace (f,x);

for D being non empty set

for f being BinOp of D

for x being Element of (D *) \ {{}} holds MultPlace (f,x) = MultPlace (f,x);

definition

let D be non empty set ;

let f be BinOp of D;

ex b_{1} being Function of ((D *) \ {{}}),D st

for x being Element of (D *) \ {{}} holds b_{1} . x = (MultPlace (f,x)) . ((len x) - 1)

for b_{1}, b_{2} being Function of ((D *) \ {{}}),D st ( for x being Element of (D *) \ {{}} holds b_{1} . x = (MultPlace (f,x)) . ((len x) - 1) ) & ( for x being Element of (D *) \ {{}} holds b_{2} . x = (MultPlace (f,x)) . ((len x) - 1) ) holds

b_{1} = b_{2}

end;
let f be BinOp of D;

::# MultPlace is an operator which transforms a BinOp f into a function

::# operating # on an arbitrary (positive and natural) number of arguments by

::# recursively # associating f on the left # Too late I realized something

::# similar (yielding a functor rather than # a function, though) was

::# introduced in FINSOP_1

::# operating # on an arbitrary (positive and natural) number of arguments by

::# recursively # associating f on the left # Too late I realized something

::# similar (yielding a functor rather than # a function, though) was

::# introduced in FINSOP_1

func MultPlace f -> Function of ((D *) \ {{}}),D means :Def9: :: FOMODEL0:def 9

for x being Element of (D *) \ {{}} holds it . x = (MultPlace (f,x)) . ((len x) - 1);

existence for x being Element of (D *) \ {{}} holds it . x = (MultPlace (f,x)) . ((len x) - 1);

ex b

for x being Element of (D *) \ {{}} holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def9 defines MultPlace FOMODEL0:def 9 :

for D being non empty set

for f being BinOp of D

for b_{3} being Function of ((D *) \ {{}}),D holds

( b_{3} = MultPlace f iff for x being Element of (D *) \ {{}} holds b_{3} . x = (MultPlace (f,x)) . ((len x) - 1) );

for D being non empty set

for f being BinOp of D

for b

( b

Lm15: for D being non empty set

for f being BinOp of D

for x being non empty FinSequence of D

for y being Element of D holds

( (MultPlace f) . <*y*> = y & (MultPlace f) . (x ^ <*y*>) = f . (((MultPlace f) . x),y) )

proof end;

Lm16: for D being non empty set

for f being BinOp of D

for X being set holds

( f is [:X,D:] -one-to-one iff for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds

( x = y & d1 = d2 ) )

proof end;

definition

let D be non empty set ;

let f be BinOp of D;

let X be set ;

( X is f -unambiguous iff for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds

( x = y & d1 = d2 ) ) by Lm16;

end;
let f be BinOp of D;

let X be set ;

redefine attr X is f -unambiguous means :Def10: :: FOMODEL0:def 10

for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds

( x = y & d1 = d2 );

compatibility for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds

( x = y & d1 = d2 );

( X is f -unambiguous iff for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds

( x = y & d1 = d2 ) ) by Lm16;

:: deftheorem Def10 defines -unambiguous FOMODEL0:def 10 :

for D being non empty set

for f being BinOp of D

for X being set holds

( X is f -unambiguous iff for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds

( x = y & d1 = d2 ) );

for D being non empty set

for f being BinOp of D

for X being set holds

( X is f -unambiguous iff for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds

( x = y & d1 = d2 ) );

Lm17: for D being non empty set

for f being BinOp of D st f is associative holds

for d being Element of D

for m being Nat

for x being Element of (m + 1) -tuples_on D holds (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x))

proof end;

Lm18: for D being non empty set

for X being non empty Subset of D

for f being BinOp of D

for m being Nat st f is associative & X is f -unambiguous holds

(MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous

proof end;

Lm19: for Y being set

for D being non empty set

for f being BinOp of D

for m being Nat st f is associative & Y is f -unambiguous holds

(MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous

proof end;

Lm20: for D being non empty set

for X being non empty Subset of D

for f being BinOp of D

for m being Nat st f is associative & X is f -unambiguous holds

MultPlace f is (m + 1) -tuples_on X -one-to-one

proof end;

Lm21: for Y being set

for D being non empty set

for f being BinOp of D

for m being Nat st f is associative & Y is f -unambiguous holds

MultPlace f is (m + 1) -tuples_on Y -one-to-one

proof end;

::########################### MultPlace ###############################

::############################## END ##################################

::########################### FirstChar ###############################

::############################## END ##################################

::########################### FirstChar ###############################

definition

let D be non empty set ;

MultPlace (D -pr1) is Function of ((D *) \ {{}}),D ;

end;
::# A function-like extracting the first item of a non empty FinSequence of D

coherence MultPlace (D -pr1) is Function of ((D *) \ {{}}),D ;

:: deftheorem defines -firstChar FOMODEL0:def 11 :

for D being non empty set holds D -firstChar = MultPlace (D -pr1);

for D being non empty set holds D -firstChar = MultPlace (D -pr1);

Lm22: for D being non empty set

for w being non empty FinSequence of D holds (D -firstChar) . w = w . 1

proof end;

theorem Th6: :: FOMODEL0:6

for U being non empty set

for p being FinSequence st p is U -valued & not p is empty holds

(U -firstChar) . p = p . 1

for p being FinSequence st p is U -valued & not p is empty holds

(U -firstChar) . p = p . 1

proof end;

::########################### FirstChar ###############################

::############################## END ##################################

::########################### MultiCat #################################

::#When f is concatenation of strings, MultPlace(f) can be extended to the

::#empty finsequence of strings in the immediate way, obtaining the multiCat

::#function, which chains an arbitrary (natural) number of strings

::############################## END ##################################

::########################### MultiCat #################################

::#When f is concatenation of strings, MultPlace(f) can be extended to the

::#empty finsequence of strings in the immediate way, obtaining the multiCat

::#function, which chains an arbitrary (natural) number of strings

definition

let D be non empty set ;

({} .--> {}) +* (MultPlace (D -concatenation)) is Function ;

end;
func D -multiCat -> Function equals :: FOMODEL0:def 12

({} .--> {}) +* (MultPlace (D -concatenation));

coherence ({} .--> {}) +* (MultPlace (D -concatenation));

({} .--> {}) +* (MultPlace (D -concatenation)) is Function ;

:: deftheorem defines -multiCat FOMODEL0:def 12 :

for D being non empty set holds D -multiCat = ({} .--> {}) +* (MultPlace (D -concatenation));

for D being non empty set holds D -multiCat = ({} .--> {}) +* (MultPlace (D -concatenation));

definition

let D be non empty set ;

:: original: -multiCat

redefine func D -multiCat -> Function of ((D *) *),(D *);

coherence

D -multiCat is Function of ((D *) *),(D *)

end;
:: original: -multiCat

redefine func D -multiCat -> Function of ((D *) *),(D *);

coherence

D -multiCat is Function of ((D *) *),(D *)

proof end;

Lm23: for D being non empty set holds (D -multiCat) | (((D *) *) \ {{}}) = MultPlace (D -concatenation)

proof end;

Lm24: for Y being set

for D being non empty set holds (D -multiCat) | (Y \ {{}}) = (MultPlace (D -concatenation)) | Y

proof end;

Lm25: for D being non empty set holds {} .--> {} tolerates MultPlace (D -concatenation)

proof end;

registration

let D be non empty set ;

let e be empty set ;

coherence

for b_{1} being set st b_{1} = (D -multiCat) . e holds

b_{1} is empty

end;
let e be empty set ;

coherence

for b

b

proof end;

registration

let D be non empty set ;

coherence

for b_{1} being Subset of (1 -tuples_on D) holds b_{1} is D -prefix

end;
coherence

for b

proof end;

theorem Th7: :: FOMODEL0:7

for A being set

for D being non empty set

for m being Nat st A is D -prefix holds

(D -multiCat) .: (m -tuples_on A) is D -prefix

for D being non empty set

for m being Nat st A is D -prefix holds

(D -multiCat) .: (m -tuples_on A) is D -prefix

proof end;

theorem :: FOMODEL0:8

for A being set

for D being non empty set

for m being Nat st A is D -prefix holds

D -multiCat is m -tuples_on A -one-to-one

for D being non empty set

for m being Nat st A is D -prefix holds

D -multiCat is m -tuples_on A -one-to-one

proof end;

theorem :: FOMODEL0:10

theorem :: FOMODEL0:11

::#extending FUNCT_2:111

definition

let A, X be set ;

:: original: chi

redefine func chi (A,X) -> Function of X,BOOLEAN;

coherence

chi (A,X) is Function of X,BOOLEAN

end;
:: original: chi

redefine func chi (A,X) -> Function of X,BOOLEAN;

coherence

chi (A,X) is Function of X,BOOLEAN

proof end;

theorem :: FOMODEL0:13

theorem Th14: :: FOMODEL0:14

for D being non empty set

for d being non empty Element of (D *) * holds (D -multiCat) . d = (MultPlace (D -concatenation)) . d

for d being non empty Element of (D *) * holds (D -multiCat) . d = (MultPlace (D -concatenation)) . d

proof end;

registration
end;

registration

let X, Y be set ;

let f be X -defined Function;

let g be Y -defined Function;

coherence

for b_{1} being Function st b_{1} = <:f,g:> holds

b_{1} is X /\ Y -defined

end;
let f be X -defined Function;

let g be Y -defined Function;

coherence

for b

b

proof end;

registration

let X be set ;

let f, g be X -defined Function;

coherence

for b_{1} being Function st b_{1} = <:f,g:> holds

b_{1} is X -defined
;

end;
let f, g be X -defined Function;

coherence

for b

b

registration

let X, Y be set ;

let f be X -defined total Function;

let g be Y -defined total Function;

coherence

for b_{1} being X /\ Y -defined Function st b_{1} = <:f,g:> holds

b_{1} is total

end;
let f be X -defined total Function;

let g be Y -defined total Function;

coherence

for b

b

proof end;

registration

let X be set ;

let f, g be X -defined total Function;

coherence

for b_{1} being X -defined Function st b_{1} = <:f,g:> holds

b_{1} is total
;

end;
let f, g be X -defined total Function;

coherence

for b

b

registration

let X, Y be set ;

let f be X -valued Function;

let g be Y -valued Function;

coherence

for b_{1} being Function st b_{1} = <:f,g:> holds

b_{1} is [:X,Y:] -valued

end;
let f be X -valued Function;

let g be Y -valued Function;

coherence

for b

b

proof end;

registration

let D be non empty set ;

ex b_{1} being FinSequence st b_{1} is D -valued

end;
cluster Relation-like omega -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support for set ;

existence ex b

proof end;

registration

let D be non empty set ;

let m be Nat;

ex b_{1} being FinSequence st

( b_{1} is m -element & b_{1} is D -valued )

end;
let m be Nat;

cluster Relation-like omega -defined D -valued Function-like finite m -element FinSequence-like FinSubsequence-like countable finite-support for set ;

existence ex b

( b

proof end;

registration

let X, Y be non empty set ;

let f be Function of X,Y;

let p be X -valued FinSequence;

coherence

f * p is FinSequence-like

end;
let f be Function of X,Y;

let p be X -valued FinSequence;

coherence

f * p is FinSequence-like

proof end;

registration

let X, Y be non empty set ;

let m be Nat;

let f be Function of X,Y;

let p be X -valued m -element FinSequence;

coherence

for b_{1} being set st b_{1} = f * p holds

b_{1} is m -element

end;
let m be Nat;

let f be Function of X,Y;

let p be X -valued m -element FinSequence;

coherence

for b

b

proof end;

definition

let D be non empty set ;

let f be BinOp of D;

let p, q be Element of D * ;

coherence

f * <:p,q:> is FinSequence of D

end;
let f be BinOp of D;

let p, q be Element of D * ;

coherence

f * <:p,q:> is FinSequence of D

proof end;

:: deftheorem defines AppliedPairwiseTo FOMODEL0:def 13 :

for D being non empty set

for f being BinOp of D

for p, q being Element of D * holds f AppliedPairwiseTo (p,q) = f * <:p,q:>;

for D being non empty set

for f being BinOp of D

for p, q being Element of D * holds f AppliedPairwiseTo (p,q) = f * <:p,q:>;

registration

let D be non empty set ;

let f be BinOp of D;

let m be Nat;

let p, q be m -element Element of D * ;

coherence

for b_{1} being set st b_{1} = f AppliedPairwiseTo (p,q) holds

b_{1} is m -element
;

end;
let f be BinOp of D;

let m be Nat;

let p, q be m -element Element of D * ;

coherence

for b

b

notation

let D be non empty set ;

let f be BinOp of D;

let p, q be Element of D * ;

synonym f _\ (p,q) for f AppliedPairwiseTo (p,q);

end;
let f be BinOp of D;

let p, q be Element of D * ;

synonym f _\ (p,q) for f AppliedPairwiseTo (p,q);

definition

compatibility

for b_{1} being set holds

( b_{1} = INT iff b_{1} = NAT \/ ([:{0},NAT:] \ {[0,0]}) )

end;
for b

( b

proof end;

theorem Th16: :: FOMODEL0:16

for Y being set

for m being Nat

for p being FinSequence st p is Y -valued & p is m -element holds

p in m -tuples_on Y

for m being Nat

for p being FinSequence st p is Y -valued & p is m -element holds

p in m -tuples_on Y

proof end;

definition

let A, B be set ;

:: original: typed/\

redefine func A typed/\ B -> Subset of A;

coherence

A typed/\ B is Subset of A by XBOOLE_1:17;

end;
:: original: typed/\

redefine func A typed/\ B -> Subset of A;

coherence

A typed/\ B is Subset of A by XBOOLE_1:17;

registration
end;

registration
end;

registration

let A be set ;

let B be Subset of A;

compatibility

A /\ B = B null A by XBOOLE_1:28;

compatibility

B null A = A /\ B ;

end;
let B be Subset of A;

compatibility

A /\ B = B null A by XBOOLE_1:28;

compatibility

B null A = A /\ B ;

registration

let A, B, C be set ;

coherence

for b_{1} being set st b_{1} = (B \ A) /\ (A /\ C) holds

b_{1} is empty

end;
coherence

for b

b

proof end;

registration
end;

definition

let A, B be set ;

A is Subset of (A \/ B) by XBOOLE_1:7;

end;
::# to automatize like: A null B c= A\/B; then A c= A\/B; this is mainly

::# not to have to remember each time what XBOOLE_1 theorem is to be invoked,

::# as long as this file is imported via definitions directive

coherence ::# not to have to remember each time what XBOOLE_1 theorem is to be invoked,

::# as long as this file is imported via definitions directive

A is Subset of (A \/ B) by XBOOLE_1:7;

registration
end;

registration

let A be set ;

let B be Subset of A;

compatibility

A \/ B = A null B by XBOOLE_1:12;

compatibility

A null B = A \/ B ;

end;
let B be Subset of A;

compatibility

A \/ B = A null B by XBOOLE_1:12;

compatibility

A null B = A \/ B ;

Lm26: for g being Function

for m being Nat

for f being Function st f c= g holds

iter (f,m) c= iter (g,m)

proof end;

Lm27: for R being Relation holds R [*] is_transitive_in field R

proof end;

Lm28: for R being Relation holds field (R [*]) c= field R

proof end;

Lm29: for R being Relation holds R [*] is_reflexive_in field R

proof end;

Lm30: for R being Relation holds field (R [*]) = field R

by LANG1:18, RELAT_1:16, Lm28;

registration

let R be Relation;

coherence

for b_{1} being Relation st b_{1} = R [*] holds

b_{1} is transitive

for b_{1} being Relation st b_{1} = R [*] holds

b_{1} is reflexive

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

Lm31: for f being Function holds iter (f,0) c= f [*]

proof end;

Lm32: for m being Nat

for f being Function holds iter (f,(m + 1)) c= f [*]

proof end;

Lm33: for m being Nat

for f being Function holds iter (f,m) c= f [*]

proof end;

Lm34: for x being set

for g being Function

for m being Nat

for f being Function st rng f c= dom f & x in dom f & g . 0 = x & ( for i being Nat st i < m holds

g . (i + 1) = f . (g . i) ) holds

g . m = (iter (f,m)) . x

proof end;

definition

ex b_{1} being Function of COMPLEX,COMPLEX st

for z being Complex holds b_{1} . z = z + 1

for b_{1}, b_{2} being Function of COMPLEX,COMPLEX st ( for z being Complex holds b_{1} . z = z + 1 ) & ( for z being Complex holds b_{2} . z = z + 1 ) holds

b_{1} = b_{2}
end;

func plus -> Function of COMPLEX,COMPLEX means :Def18: :: FOMODEL0:def 18

for z being Complex holds it . z = z + 1;

existence for z being Complex holds it . z = z + 1;

ex b

for z being Complex holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def18 defines plus FOMODEL0:def 18 :

for b_{1} being Function of COMPLEX,COMPLEX holds

( b_{1} = plus iff for z being Complex holds b_{1} . z = z + 1 );

for b

( b

Lm35: for x being set

for p being FinSequence

for m being Nat

for f being Function st rng f c= dom f & x in dom f & p . 1 = x & ( for i being Nat st i >= 1 & i < m + 1 holds

p . (i + 1) = f . (p . i) ) holds

p . (m + 1) = (iter (f,m)) . x

proof end;

Lm36: for z being set

for f being Function st z in f [*] & rng f c= dom f holds

ex n being Nat st z in iter (f,n)

proof end;

Lm37: for f being Function st rng f c= dom f holds

f [*] = union { (iter (f,mm)) where mm is Element of NAT : verum }

proof end;

theorem :: FOMODEL0:17

theorem :: FOMODEL0:18

registration

let X be functional set ;

coherence

for b_{1} being set st b_{1} = union X holds

b_{1} is Relation-like

end;
coherence

for b

b

proof end;

registration
end;

registration

let D be non empty set ;

let d be Element of D;

coherence

for b_{1} being set st b_{1} = {((id D) . d)} \ {d} holds

b_{1} is empty
;

end;
let d be Element of D;

coherence

for b

b

registration

let p be FinSequence;

let q be empty FinSequence;

compatibility

p ^ q = p null q by FINSEQ_1:34;

compatibility

p null q = p ^ q ;

compatibility

q ^ p = p null q by FINSEQ_1:34;

compatibility

p null q = q ^ p ;

end;
let q be empty FinSequence;

compatibility

p ^ q = p null q by FINSEQ_1:34;

compatibility

p null q = p ^ q ;

compatibility

q ^ p = p null q by FINSEQ_1:34;

compatibility

p null q = q ^ p ;

registration

let Y be set ;

let R be Y -defined Relation;

compatibility

R | Y = R null Y ;

compatibility

R null Y = R | Y ;

end;
let R be Y -defined Relation;

compatibility

R | Y = R null Y ;

compatibility

R null Y = R | Y ;

theorem :: FOMODEL0:22

for D being non empty set

for m, n being Nat holds (m + n) -tuples_on D = (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):]

for m, n being Nat holds (m + n) -tuples_on D = (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):]

proof end;

Lm38: for A, B being set holds chi (A,B) = (B --> 0) +* ((A /\ B) --> 1)

proof end;

Lm39: for A, B being set holds chi (A,B) = ((B \ A) --> 0) +* ((A /\ B) --> 1)

proof end;

Lm40: for A, B being set holds chi (A,B) = ((B \ A) --> 0) \/ ((A /\ B) --> 1)

proof end;

theorem :: FOMODEL0:26

for Y being set

for f being Function st f is Y -valued & f is FinSequence-like holds

f is FinSequence of Y by Lm1;

for f being Function st f is Y -valued & f is FinSequence-like holds

f is FinSequence of Y by Lm1;

registration

let Y be set ;

let X be Subset of Y;

coherence

for b_{1} being Relation st b_{1} is X -valued holds

b_{1} is Y -valued
by XBOOLE_1:1;

end;
let X be Subset of Y;

coherence

for b

b

Lm41: for Y being set

for R being b

( f c= R & dom f = Y )

proof end;

Lm42: for R being Relation

for f being Function st dom f c= dom R & R c= f holds

R = f

proof end;

Lm43: for Y being set

for P, R being Relation

for Q being b

((P * Q) * (Q ~)) * R = P * R

proof end;

registration

let A be set ;

let U be non empty set ;

coherence

for b_{1} being Relation of A,U st b_{1} is quasi_total holds

b_{1} is total
;

end;
let U be non empty set ;

coherence

for b

b

theorem :: FOMODEL0:27

for A, B being set

for U1, U2 being non empty set

for Q being quasi_total Relation of B,U1

for R being quasi_total Relation of B,U2

for P being Relation of A,B st ((P * Q) * (Q ~)) * R is Function-like holds

((P * Q) * (Q ~)) * R = P * R

for U1, U2 being non empty set

for Q being quasi_total Relation of B,U1

for R being quasi_total Relation of B,U2

for P being Relation of A,B st ((P * Q) * (Q ~)) * R is Function-like holds

((P * Q) * (Q ~)) * R = P * R

proof end;

registration

let U be non empty set ;

let p, q be U -valued FinSequence;

coherence

for b_{1} being FinSequence st b_{1} = p ^ q holds

b_{1} is U -valued

end;
let p, q be U -valued FinSequence;

coherence

for b

b

proof end;

definition

let X be set ;

:: original: FinSequence

redefine mode FinSequence of X -> Element of X * ;

coherence

for b_{1} being FinSequence of X holds b_{1} is Element of X *
by FINSEQ_1:def 11;

end;
:: original: FinSequence

redefine mode FinSequence of X -> Element of X * ;

coherence

for b

definition

let U be non empty set ;

let X be set ;

( X is U -prefix iff for p1, q1, p2, q2 being U -valued FinSequence st p1 in X & p2 in X & p1 ^ q1 = p2 ^ q2 holds

( p1 = p2 & q1 = q2 ) )

end;
let X be set ;

redefine attr X is U -prefix means :: FOMODEL0:def 19

for p1, q1, p2, q2 being U -valued FinSequence st p1 in X & p2 in X & p1 ^ q1 = p2 ^ q2 holds

( p1 = p2 & q1 = q2 );

compatibility for p1, q1, p2, q2 being U -valued FinSequence st p1 in X & p2 in X & p1 ^ q1 = p2 ^ q2 holds

( p1 = p2 & q1 = q2 );

( X is U -prefix iff for p1, q1, p2, q2 being U -valued FinSequence st p1 in X & p2 in X & p1 ^ q1 = p2 ^ q2 holds

( p1 = p2 & q1 = q2 ) )

proof end;

:: deftheorem defines -prefix FOMODEL0:def 19 :

for U being non empty set

for X being set holds

( X is U -prefix iff for p1, q1, p2, q2 being b_{1} -valued FinSequence st p1 in X & p2 in X & p1 ^ q1 = p2 ^ q2 holds

( p1 = p2 & q1 = q2 ) );

for U being non empty set

for X being set holds

( X is U -prefix iff for p1, q1, p2, q2 being b

( p1 = p2 & q1 = q2 ) );

registration
end;

registration

let U be non empty set ;

let m be Nat;

let X be U -prefix set ;

coherence

for b_{1} being set st b_{1} = (U -multiCat) .: (m -tuples_on X) holds

b_{1} is U -prefix
by Th7;

end;
let m be Nat;

let X be U -prefix set ;

coherence

for b

b

theorem Th29: :: FOMODEL0:29

for Y, X being set holds

( ( X \+\ Y = {} implies X = Y ) & ( X = Y implies X \+\ Y = {} ) & ( X \ Y = {} implies X c= Y ) & ( X c= Y implies X \ Y = {} ) & ( for x being object holds

( {x} \ Y = {} iff x in Y ) ) )

( ( X \+\ Y = {} implies X = Y ) & ( X = Y implies X \+\ Y = {} ) & ( X \ Y = {} implies X c= Y ) & ( X c= Y implies X \ Y = {} ) & ( for x being object holds

( {x} \ Y = {} iff x in Y ) ) )

proof end;

registration
end;

registration

let x be set ;

coherence

for b_{1} being set st b_{1} = (id {x}) \+\ {[x,x]} holds

b_{1} is empty

end;
coherence

for b

b

proof end;

registration

let x, y be set ;

coherence

for b_{1} being set st b_{1} = (x .--> y) \+\ {[x,y]} holds

b_{1} is empty

end;
coherence

for b

b

proof end;

registration

let x be set ;

coherence

for b_{1} being set st b_{1} = (id {x}) \+\ (x .--> x) holds

b_{1} is empty

end;
coherence

for b

b

proof end;

theorem :: FOMODEL0:30

for x being set

for D being non empty set holds

( x in (D *) \ {{}} iff ( x is b_{2} -valued FinSequence & not x is empty ) )

for D being non empty set holds

( x in (D *) \ {{}} iff ( x is b

proof end;

theorem Th31: :: FOMODEL0:31

for D being non empty set

for d being Element of D

for f being BinOp of D holds

( (MultPlace f) . <*d*> = d & ( for x being b_{1} -valued FinSequence st not x is empty holds

(MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d) ) )

for d being Element of D

for f being BinOp of D holds

( (MultPlace f) . <*d*> = d & ( for x being b

(MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d) ) )

proof end;

registration
end;

:: deftheorem defines -SymbolSubstIn FOMODEL0:def 20 :

for x, y being set

for p being FinSequence holds (x,y) -SymbolSubstIn p = p +~ (x,y);

for x, y being set

for p being FinSequence holds (x,y) -SymbolSubstIn p = p +~ (x,y);

registration

let x, y be set ;

let m be Nat;

let p be m -element FinSequence;

coherence

for b_{1} being FinSequence st b_{1} = (x,y) -SymbolSubstIn p holds

b_{1} is m -element

end;
let m be Nat;

let p be m -element FinSequence;

coherence

for b

b

proof end;

registration

let x be set ;

let U be non empty set ;

let u be Element of U;

let p be U -valued FinSequence;

coherence

for b_{1} being FinSequence st b_{1} = (x,u) -SymbolSubstIn p holds

b_{1} is U -valued
;

end;
let U be non empty set ;

let u be Element of U;

let p be U -valued FinSequence;

coherence

for b

b

definition

let X, x, y be set ;

let p be X -valued FinSequence;

for b_{1} being FinSequence holds

( b_{1} = (x,y) -SymbolSubstIn p iff b_{1} = ((id X) +* (x,y)) * p )

end;
let p be X -valued FinSequence;

:: original: -SymbolSubstIn

redefine func (x,y) -SymbolSubstIn p -> FinSequence equals :: FOMODEL0:def 21

((id X) +* (x,y)) * p;

compatibility redefine func (x,y) -SymbolSubstIn p -> FinSequence equals :: FOMODEL0:def 21

((id X) +* (x,y)) * p;

for b

( b

proof end;

:: deftheorem defines -SymbolSubstIn FOMODEL0:def 21 :

for X, x, y being set

for p being b_{1} -valued FinSequence holds (x,y) -SymbolSubstIn p = ((id X) +* (x,y)) * p;

for X, x, y being set

for p being b

definition

let U be non empty set ;

let x be set ;

let u be Element of U;

let q be U -valued FinSequence;

:: original: -SymbolSubstIn

redefine func (x,u) -SymbolSubstIn q -> FinSequence of U;

coherence

(x,u) -SymbolSubstIn q is FinSequence of U by Lm1;

end;
let x be set ;

let u be Element of U;

let q be U -valued FinSequence;

:: original: -SymbolSubstIn

redefine func (x,u) -SymbolSubstIn q -> FinSequence of U;

coherence

(x,u) -SymbolSubstIn q is FinSequence of U by Lm1;

Lm44: for x2 being set

for U being non empty set

for u, u1 being Element of U holds

( ( u = u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*x2*> ) & ( u <> u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*u*> ) )

proof end;

Lm45: for x being set

for U being non empty set

for u being Element of U

for q1, q2 being b

proof end;

definition

let U be non empty set ;

let x be set ;

let u be Element of U;

set D = U * ;

deffunc H_{1}( Element of U * ) -> FinSequence of U = (x,u) -SymbolSubstIn $1;

ex b_{1} being Function of (U *),(U *) st

for q being U -valued FinSequence holds b_{1} . q = (x,u) -SymbolSubstIn q

for b_{1}, b_{2} being Function of (U *),(U *) st ( for q being U -valued FinSequence holds b_{1} . q = (x,u) -SymbolSubstIn q ) & ( for q being U -valued FinSequence holds b_{2} . q = (x,u) -SymbolSubstIn q ) holds

b_{1} = b_{2}

end;
let x be set ;

let u be Element of U;

set D = U * ;

deffunc H

func x SubstWith u -> Function of (U *),(U *) means :Def22: :: FOMODEL0:def 22

for q being U -valued FinSequence holds it . q = (x,u) -SymbolSubstIn q;

existence for q being U -valued FinSequence holds it . q = (x,u) -SymbolSubstIn q;

ex b

for q being U -valued FinSequence holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def22 defines SubstWith FOMODEL0:def 22 :

for U being non empty set

for x being set

for u being Element of U

for b_{4} being Function of (U *),(U *) holds

( b_{4} = x SubstWith u iff for q being b_{1} -valued FinSequence holds b_{4} . q = (x,u) -SymbolSubstIn q );

for U being non empty set

for x being set

for u being Element of U

for b

( b

Lm46: for U being non empty set

for u, u1, u2 being Element of U holds

( ( u = u1 implies (u1 SubstWith u2) . <*u*> = <*u2*> ) & ( u <> u1 implies (u1 SubstWith u2) . <*u*> = <*u*> ) )

proof end;

registration

let U be non empty set ;

let x be set ;

let u be Element of U;

coherence

for b_{1} being Function st b_{1} = x SubstWith u holds

b_{1} is FinSequence-yielding

end;
let x be set ;

let u be Element of U;

coherence

for b

b

proof end;

Lm47: for x being set

for U being non empty set

for u being Element of U

for q1, q2 being b

proof end;

registration

let U be non empty set ;

let x be set ;

let u be Element of U;

let m be Nat;

let p be U -valued m -element FinSequence;

coherence

for b_{1} being FinSequence st b_{1} = (x SubstWith u) . p holds

b_{1} is m -element

end;
let x be set ;

let u be Element of U;

let m be Nat;

let p be U -valued m -element FinSequence;

coherence

for b

b

proof end;

registration

let U be non empty set ;

let x be set ;

let u be Element of U;

let e be empty set ;

coherence

for b_{1} being set st b_{1} = (x SubstWith u) . e holds

b_{1} is empty

end;
let x be set ;

let u be Element of U;

let e be empty set ;

coherence

for b

b

proof end;

registration

let U be non empty set ;

coherence

for b_{1} being Function st b_{1} = U -multiCat holds

b_{1} is FinSequence-yielding

end;
coherence

for b

b

proof end;

registration

let U be non empty set ;

let m1 be non zero Nat;

let n be Nat;

let p be U -valued m1 + n -element FinSequence;

coherence

for b_{1} being set st b_{1} = {(p . m1)} \ U holds

b_{1} is empty

end;
let m1 be non zero Nat;

let n be Nat;

let p be U -valued m1 + n -element FinSequence;

coherence

for b

b

proof end;

registration

let U be non empty set ;

let m, n be Nat;

let p be (m + 1) + n -element Element of U * ;

coherence

for b_{1} being set st b_{1} = {(p . (m + 1))} \ U holds

b_{1} is empty
;

end;
let m, n be Nat;

let p be (m + 1) + n -element Element of U * ;

coherence

for b

b

registration
end;

registration

let m be Nat;

let p be m + 1 -element FinSequence;

coherence

for b_{1} being set st b_{1} = ((p | (Seg m)) ^ <*(p . (m + 1))*>) \+\ p holds

b_{1} is empty

end;
let p be m + 1 -element FinSequence;

coherence

for b

b

proof end;

registration

let m, n be Nat;

let p be m + n -element FinSequence;

coherence

for b_{1} being FinSequence st b_{1} = p | (Seg m) holds

b_{1} is m -element

end;
let p be m + n -element FinSequence;

coherence

for b

b

proof end;

registration

coherence

for b_{1} being Relation st b_{1} is {{}} -valued holds

b_{1} is empty-yielding
;

coherence

for b_{1} being Relation st b_{1} is empty-yielding holds

b_{1} is {{}} -valued
;

end;
for b

b

coherence

for b

b

theorem Th32: :: FOMODEL0:32

for x being set

for U being non empty set holds (U -multiCat) . x = (MultPlace (U -concatenation)) . x

for U being non empty set holds (U -multiCat) . x = (MultPlace (U -concatenation)) . x

proof end;

theorem Th33: :: FOMODEL0:33

for U being non empty set

for p being FinSequence

for q being b_{1} -valued FinSequence st p is U * -valued holds

(U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q

for p being FinSequence

for q being b

(U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q

proof end;

Lm48: for x being set

for U being non empty set

for u being Element of U

for p being FinSequence st p is U * -valued holds

(x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p)

proof end;

registration

let Y be set ;

let X be Subset of Y;

let R be Y -defined total Relation;

coherence

for b_{1} being X -defined Relation st b_{1} = R | X holds

b_{1} is total

end;
let X be Subset of Y;

let R be Y -defined total Relation;

coherence

for b

b

proof end;

theorem :: FOMODEL0:34

theorem :: FOMODEL0:35

theorem :: FOMODEL0:36

theorem :: FOMODEL0:37

theorem :: FOMODEL0:38

for U being non empty set holds (U -concatenation) .: (id (1 -tuples_on U)) = { <*u,u*> where u is Element of U : verum }

proof end;

registration

let f be Function;

let U be non empty set ;

let u be Element of U;

coherence

for b_{1} being set st b_{1} = ((f | U) . u) \+\ (f . u) holds

b_{1} is empty

end;
let U be non empty set ;

let u be Element of U;

coherence

for b

b

proof end;

registration

let f be Function;

let U1, U2 be non empty set ;

let u be Element of U1;

let g be Function of U1,U2;

coherence

for b_{1} being set st b_{1} = ((f * g) . u) \+\ (f . (g . u)) holds

b_{1} is empty

end;
let U1, U2 be non empty set ;

let u be Element of U1;

let g be Function of U1,U2;

coherence

for b

b

proof end;

registration
end;

registration

let x, y be Real;

coherence

for b_{1} being ExtReal st b_{1} = (max (x,y)) - x holds

not b_{1} is negative

end;
coherence

for b

not b

proof end;

theorem :: FOMODEL0:39

registration

let Y be set ;

let X be Subset of Y;

coherence

for b_{1} being set st b_{1} = X \ Y holds

b_{1} is empty
by XBOOLE_1:37;

end;
let X be Subset of Y;

coherence

for b

b

registration

let x, y be object ;

coherence

for b_{1} being set st b_{1} = {x} \ {x,y} holds

b_{1} is empty

end;
coherence

for b

b

proof end;

registration
end;

registration
end;

registration

let n be positive Nat;

let X be non empty set ;

ex b_{1} being Element of (X *) \ {{}} st b_{1} is n -element

end;
let X be non empty set ;

cluster Relation-like omega -defined Function-like finite n -element FinSequence-like FinSubsequence-like countable finite-support for Element of (X *) \ {{}};

existence ex b

proof end;

registration

let m1 be non zero Nat;

coherence

for b_{1} being FinSequence st b_{1} is m1 + 0 -element holds

not b_{1} is empty
;

end;
coherence

for b

not b

registration

let R be Relation;

let x be set ;

coherence

for b_{1} being set st b_{1} = R null x holds

b_{1} is Relation-like
;

end;
let x be set ;

coherence

for b

b

registration

let f be Function-like set ;

let x be set ;

coherence

for b_{1} being set st b_{1} = f null x holds

b_{1} is Function-like
;

end;
let x be set ;

coherence

for b

b

registration

let p be FinSequence-like Relation;

let x be set ;

coherence

for b_{1} being Relation st b_{1} = p null x holds

b_{1} is FinSequence-like
;

end;
let x be set ;

coherence

for b

b

registration

let p be FinSequence;

let x be set ;

coherence

for b_{1} being FinSequence st b_{1} = p null x holds

b_{1} is len p -element
by CARD_1:def 7;

end;
let x be set ;

coherence

for b

b

registration

let p be non empty FinSequence;

coherence

for b_{1} being number st b_{1} = len p holds

not b_{1} is zero
;

end;
coherence

for b

not b

registration

let R be Relation;

let X be set ;

coherence

for b_{1} being Relation st b_{1} = R | X holds

b_{1} is X -defined
by RELAT_1:58;

end;
let X be set ;

coherence

for b

b

registration

let x be set ;

let e be empty set ;

coherence

for b_{1} being set st b_{1} = e null x holds

b_{1} is empty
;

end;
let e be empty set ;

coherence

for b

b

registration

let X be set ;

let e be empty set ;

coherence

for b_{1} being Relation st b_{1} = e null X holds

b_{1} is X -valued

end;
let e be empty set ;

coherence

for b

b

proof end;

registration

let Y be non empty FinSequence-membered set ;

coherence

for b_{1} being Function st b_{1} is Y -valued holds

b_{1} is FinSequence-yielding

end;
coherence

for b

b

proof end;

registration

let X, Y be set ;

coherence

for b_{1} being Element of Funcs (X,(Y *)) holds b_{1} is FinSequence-yielding
;

end;
coherence

for b

registration

let m, n be Nat;

let p be m -element FinSequence;

coherence

for b_{1} being Relation st b_{1} = p null n holds

b_{1} is Seg (m + n) -defined

end;
let p be m -element FinSequence;

coherence

for b

b

proof end;

Lm49: for m being Nat

for p1, p2, q1, q2 being FinSequence st p1 is m -element & q1 is m -element & p1 ^ p2 = q1 ^ q2 holds

( p1 = q1 & p2 = q2 )

proof end;

registration

let m, n be Nat;

let p be m -element FinSequence;

let q be n -element FinSequence;

coherence

for b_{1} being FinSequence st b_{1} = p ^ q holds

b_{1} is m + n -element
;

end;
let p be m -element FinSequence;

let q be n -element FinSequence;

coherence

for b

b

theorem :: FOMODEL0:41

for m being Nat

for p1, p2, q1, q2 being FinSequence st p1 is m -element & q1 is m -element & ( p1 ^ p2 = q1 ^ q2 or p2 ^ p1 = q2 ^ q1 ) holds

( p1 = q1 & p2 = q2 )

for p1, p2, q1, q2 being FinSequence st p1 is m -element & q1 is m -element & ( p1 ^ p2 = q1 ^ q2 or p2 ^ p1 = q2 ^ q1 ) holds

( p1 = q1 & p2 = q2 )

proof end;

theorem :: FOMODEL0:42

for x being set

for U, U1 being non empty set st (U -multiCat) . x is U1 -valued & x in (U *) * holds

x is FinSequence of U1 *

for U, U1 being non empty set st (U -multiCat) . x is U1 -valued & x in (U *) * holds

x is FinSequence of U1 *

proof end;

registration

let U be non empty set ;

existence

ex b_{1} being reflexive Relation of U st b_{1} is total

end;
existence

ex b

proof end;

registration

let m be Nat;

coherence

for b_{1} being FinSequence st b_{1} is m + 1 -element holds

not b_{1} is empty
;

end;
coherence

for b

not b

registration

let U be non empty set ;

let u be Element of U;

coherence

for b_{1} being set st b_{1} = ((id U) . u) \+\ u holds

b_{1} is empty
;

end;
let u be Element of U;

coherence

for b

b

registration

let U be non empty set ;

let p be U -valued non empty FinSequence;

coherence

for b_{1} being set st b_{1} = {(p . 1)} \ U holds

b_{1} is empty

end;
let p be U -valued non empty FinSequence;

coherence

for b

b

proof end;

theorem :: FOMODEL0:43

for x1, x2, y1, y2 being set

for f being Function holds

( ( x1 = x2 implies (f +* (x1 .--> y1)) +* (x2 .--> y2) = f +* (x2 .--> y2) ) & ( x1 <> x2 implies (f +* (x1 .--> y1)) +* (x2 .--> y2) = (f +* (x2 .--> y2)) +* (x1 .--> y1) ) )

for f being Function holds

( ( x1 = x2 implies (f +* (x1 .--> y1)) +* (x2 .--> y2) = f +* (x2 .--> y2) ) & ( x1 <> x2 implies (f +* (x1 .--> y1)) +* (x2 .--> y2) = (f +* (x2 .--> y2)) +* (x1 .--> y1) ) )

proof end;

registration

let X be set ;

let U be non empty set ;

existence

ex b_{1} being X -defined Function st

( b_{1} is U -valued & b_{1} is total )

end;
let U be non empty set ;

existence

ex b

( b

proof end;

registration

let X be set ;

let U be non empty set ;

let P be X -defined U -valued total Relation;

let Q be U -defined total Relation;

coherence

for b_{1} being X -defined Relation st b_{1} = P * Q holds

b_{1} is total

end;
let U be non empty set ;

let P be X -defined U -valued total Relation;

let Q be U -defined total Relation;

coherence

for b

b

proof end;

theorem :: FOMODEL0:44

for X being set

for p, p1, p2 being FinSequence st (p ^ p1) ^ p2 is X -valued holds

( p2 is X -valued & p1 is X -valued & p is X -valued )

for p, p1, p2 being FinSequence st (p ^ p1) ^ p2 is X -valued holds

( p2 is X -valued & p1 is X -valued & p is X -valued )

proof end;

registration

let X be set ;

let R be Relation;

coherence

for b_{1} being Relation st b_{1} = R null X holds

b_{1} is X \/ (rng R) -valued

end;
let R be Relation;

coherence

for b

b

proof end;

registration

coherence

for b_{1} being set st b_{1} is FinSequence-membered holds

b_{1} is finite-membered

end;
for b

b

proof end;

definition

let X be functional set ;

union { (rng x) where x is Element of X \/ {{}} : x in X } is set ;

end;
func SymbolsOf X -> set equals :: FOMODEL0:def 23

union { (rng x) where x is Element of X \/ {{}} : x in X } ;

coherence union { (rng x) where x is Element of X \/ {{}} : x in X } ;

union { (rng x) where x is Element of X \/ {{}} : x in X } is set ;

:: deftheorem defines SymbolsOf FOMODEL0:def 23 :

for X being functional set holds SymbolsOf X = union { (rng x) where x is Element of X \/ {{}} : x in X } ;

for X being functional set holds SymbolsOf X = union { (rng x) where x is Element of X \/ {{}} : x in X } ;

Lm50: for X being functional set st X is finite & X is finite-membered holds

SymbolsOf X is finite

proof end;

registration
end;

registration

let X be functional finite finite-membered set ;

coherence

for b_{1} being set st b_{1} = SymbolsOf X holds

b_{1} is finite
by Lm50;

end;
coherence

for b

b

registration

let X be finite FinSequence-membered set ;

coherence

for b_{1} being set st b_{1} = SymbolsOf X holds

b_{1} is finite
;

end;
coherence

for b

b

registration

let z be non zero Complex;

coherence

for b_{1} being ExtReal st b_{1} = |.z.| holds

b_{1} is positive
by COMPLEX1:47;

end;
coherence

for b

b

definition

let X be functional set ;

for b_{1} being set holds

( b_{1} = SymbolsOf X iff b_{1} = union { (rng x) where x is Element of X : x in X } )

end;
redefine func SymbolsOf X equals :: FOMODEL0:def 24

union { (rng x) where x is Element of X : x in X } ;

compatibility union { (rng x) where x is Element of X : x in X } ;

for b

( b

proof end;

:: deftheorem defines SymbolsOf FOMODEL0:def 24 :

for X being functional set holds SymbolsOf X = union { (rng x) where x is Element of X : x in X } ;

for X being functional set holds SymbolsOf X = union { (rng x) where x is Element of X : x in X } ;

Lm51: for B being functional set

for A being Subset of B holds { (rng x) where x is Element of A : x in A } c= { (rng x) where x is Element of B : x in B }

proof end;

theorem :: FOMODEL0:46

for B being functional set

for A being Subset of B holds SymbolsOf A c= SymbolsOf B by Lm51, ZFMISC_1:77;

for A being Subset of B holds SymbolsOf A c= SymbolsOf B by Lm51, ZFMISC_1:77;

registration

let X be set ;

let F be Subset of (bool X);

coherence

for b_{1} being set st b_{1} = (union F) \ X holds

b_{1} is empty
;

end;
let F be Subset of (bool X);

coherence

for b

b

theorem :: FOMODEL0:49

theorem :: FOMODEL0:50

theorem Th51: :: FOMODEL0:51

for f, g being Function holds

( f c= g iff for x being set st x in dom f holds

( x in dom g & f . x = g . x ) )

( f c= g iff for x being set st x in dom f holds

( x in dom g & f . x = g . x ) )

proof end;

registration

let X, Y be set ;

coherence

((X \ Y) \/ (X /\ Y)) \+\ X is empty by Th29, Th48;

let Z be set ;

coherence

((X /\ Y) \/ (X /\ Z)) \+\ (X /\ (Y \/ Z)) is empty by XBOOLE_1:23, Th29;

coherence

((X \ Y) \ Z) \+\ (X \ (Y \/ Z)) is empty by XBOOLE_1:41, Th29;

end;
coherence

((X \ Y) \/ (X /\ Y)) \+\ X is empty by Th29, Th48;

let Z be set ;

coherence

((X /\ Y) \/ (X /\ Z)) \+\ (X /\ (Y \/ Z)) is empty by XBOOLE_1:23, Th29;

coherence

((X \ Y) \ Z) \+\ (X \ (Y \/ Z)) is empty by XBOOLE_1:41, Th29;

registration

let X, Y be functional set ;

coherence

((SymbolsOf X) \/ (SymbolsOf Y)) \+\ (SymbolsOf (X \/ Y)) is empty by Th47, Th29;

end;
coherence

((SymbolsOf X) \/ (SymbolsOf Y)) \+\ (SymbolsOf (X \/ Y)) is empty by Th47, Th29;

registration

let U be non empty set ;

coherence

for b_{1} being Element of ((U *) \ {{}}) * st not b_{1} is empty holds

not b_{1} is empty-yielding

end;
coherence

for b

not b

proof end;

registration
end;

theorem Th52: :: FOMODEL0:52

for x being set

for U1, U2 being non empty set

for p being FinSequence holds

( ( (U1 -multiCat) . x <> {} & (U2 -multiCat) . x <> {} implies (U1 -multiCat) . x = (U2 -multiCat) . x ) & ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {} * -valued ) )

for U1, U2 being non empty set

for p being FinSequence holds

( ( (U1 -multiCat) . x <> {} & (U2 -multiCat) . x <> {} implies (U1 -multiCat) . x = (U2 -multiCat) . x ) & ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {} * -valued ) )

proof end;

registration
end;

definition
end;

registration

let Y be with_non-empty_elements set ;

coherence

for b_{1} being Y -valued Relation st not b_{1} is empty holds

not b_{1} is empty-yielding

end;
coherence

for b

not b

proof end;

registration

let X be with_non-empty_elements set ;

coherence

for b_{1} being Subset of X holds b_{1} is with_non-empty_elements

end;
coherence

for b

proof end;

registration

let U be non empty set ;

coherence

for b_{1} being set st b_{1} = U * holds

not b_{1} is finite

end;
coherence

for b

not b

proof end;

registration

let U be non empty set ;

coherence

for b_{1} being set st b_{1} = U * holds

not b_{1} is empty-membered
;

end;
coherence

for b

not b

registration

let X be with_non-empty_element set ;

existence

ex b_{1} being non empty Subset of X st b_{1} is with_non-empty_elements

end;
existence

ex b

proof end;

Lm52: for Y being set

for U being non empty set

for p being FinSequence st p <> {} & p is Y -valued & Y c= U * & Y is with_non-empty_elements holds

(U -multiCat) . p <> {}

proof end;

theorem :: FOMODEL0:53

for Y being set

for U1, U2 being non empty set

for p being FinSequence st U1 c= U2 & Y c= U1 * & p is Y -valued & p <> {} & Y is with_non-empty_elements holds

(U1 -multiCat) . p = (U2 -multiCat) . p

for U1, U2 being non empty set

for p being FinSequence st U1 c= U2 & Y c= U1 * & p is Y -valued & p <> {} & Y is with_non-empty_elements holds

(U1 -multiCat) . p = (U2 -multiCat) . p

proof end;

theorem :: FOMODEL0:54

for X, x being set

for U being non empty set st ex p being FinSequence st

( x = p & p is X * -valued ) holds

(U -multiCat) . x is X -valued

for U being non empty set st ex p being FinSequence st

( x = p & p is X * -valued ) holds

(U -multiCat) . x is X -valued

proof end;

registration

let X be set ;

let m be Nat;

coherence

for b_{1} being set st b_{1} = (m -tuples_on X) \ (X *) holds

b_{1} is empty

end;
let m be Nat;

coherence

for b

b

proof end;

registration

let X be set ;

coherence

for b_{1} being set st b_{1} = (bool X) \ X holds

not b_{1} is empty

end;
coherence

for b

not b

proof end;

registration

let X be set ;

let R be Relation;

coherence

for b_{1} being Relation st b_{1} = R null X holds

b_{1} is X \/ (dom R) -defined

end;
let R be Relation;

coherence

for b

b

proof end;

registration

let X be set ;

let f be X -defined Function;

let g be X -defined total Function;

compatibility

f +* g = g null f

g null f = f +* g ;

end;
let f be X -defined Function;

let g be X -defined total Function;

compatibility

f +* g = g null f

proof end;

compatibility g null f = f +* g ;

definition

let X be set ;

[:NAT,{ the Element of (bool (proj2 X)) \ (proj2 X)}:] is set ;

end;
func X -freeCountableSet -> set equals :: FOMODEL0:def 26

[:NAT,{ the Element of (bool (proj2 X)) \ (proj2 X)}:];

coherence [:NAT,{ the Element of (bool (proj2 X)) \ (proj2 X)}:];

[:NAT,{ the Element of (bool (proj2 X)) \ (proj2 X)}:] is set ;

:: deftheorem defines -freeCountableSet FOMODEL0:def 26 :

for X being set holds X -freeCountableSet = [:NAT,{ the Element of (bool (proj2 X)) \ (proj2 X)}:];

for X being set holds X -freeCountableSet = [:NAT,{ the Element of (bool (proj2 X)) \ (proj2 X)}:];

registration

let X be set ;

coherence

for b_{1} being set st b_{1} = X -freeCountableSet holds

not b_{1} is finite
;

end;
coherence

for b

not b

registration

let X be set ;

coherence

for b_{1} being set st b_{1} = X -freeCountableSet holds

b_{1} is countable
by CARD_4:7;

end;
coherence

for b

b

registration

let x be set ;

let p be FinSequence;

coherence

for b_{1} being set st b_{1} = ((<*x*> ^ p) . 1) \+\ x holds

b_{1} is empty

end;
let p be FinSequence;

coherence

for b

b

proof end;

registration

let m be Nat;

let m0 be zero number ;

let p be m -element FinSequence;

coherence

for b_{1} being Seg (m + m0) -defined Relation st b_{1} = p null m0 holds

b_{1} is total

end;
let m0 be zero number ;

let p be m -element FinSequence;

coherence

for b

b

proof end;

registration

let U be non empty set ;

let q1, q2 be U -valued FinSequence;

coherence

for b_{1} being set st b_{1} = ((U -multiCat) . <*q1,q2*>) \+\ (q1 ^ q2) holds

b_{1} is empty

end;
let q1, q2 be U -valued FinSequence;

coherence

for b

b

proof end;

registration

let f be Function;

let e be empty set ;

compatibility

f +* e = f null e ;

compatibility

f null e = f +* e ;

compatibility

e +* f = f null e ;

compatibility

f null e = e +* f ;

end;
let e be empty set ;

compatibility

f +* e = f null e ;

compatibility

f null e = f +* e ;

compatibility

e +* f = f null e ;

compatibility

f null e = e +* f ;

registration
end;

registration

let X be finite-membered countable set ;

coherence

for b_{1} being set st b_{1} = union X holds

b_{1} is countable

end;
coherence

for b

b

proof end;

registration

let X be functional finite-membered countable set ;

coherence

for b_{1} being set st b_{1} = SymbolsOf X holds

b_{1} is countable

end;
coherence

for b

b

proof end;

registration

let A, B be countable set ;

coherence

for b_{1} being set st b_{1} = A \/ B holds

b_{1} is countable
by CARD_2:85;

end;
coherence

for b

b

theorem :: FOMODEL0:65

for Y being set st Y is c=directed holds

for X being finite Subset of (union Y) ex y being set st

( y in Y & X c= y )

for X being finite Subset of (union Y) ex y being set st

( y in Y & X c= y )

proof end;

Lm53: for A, B, X being set st X is Subset of (Funcs (A,B)) holds

X is Subset-Family of [:A,B:]

proof end;

theorem :: FOMODEL0:66

Lm54: for Y being set

for U being non empty set

for x, y being Element of U holds

not ( ( x in Y implies y in Y ) & ( y in Y implies x in Y ) & not [((chi (Y,U)) . x),((chi (Y,U)) . y)] in id BOOLEAN )

proof end;

theorem :: FOMODEL0:67

:: deftheorem defines typed| FOMODEL0:def 27 :

for A being set

for R being Relation holds R typed| A = R | A;

for A being set

for R being Relation holds R typed| A = R | A;

registration

let A be set ;

let R be Relation;

compatibility

R typed| A = R | A ;

compatibility

R | A = R typed| A ;

end;
let R be Relation;

compatibility

R typed| A = R | A ;

compatibility

R | A = R typed| A ;

Lm55: for A, B being set

for R being Relation holds R | (A \ B) = (R | A) \ [:B,(rng R):]

proof end;

Lm56: for f, g being Function holds f +* g = (f \ [:(dom g),(rng f):]) \/ g

proof end;

Lm57: for A, B, C being set holds A /\ C = A \ ((A \/ B) \ C)

proof end;

registration
end;

registration

let X be set ;

let P be Relation;

compatibility

P |1 X = P | X by RELAT_1:67;

compatibility

P | X = P |1 X ;

end;
let P be Relation;

compatibility

P |1 X = P | X by RELAT_1:67;

compatibility

P | X = P |1 X ;

Lm58: for X being set

for P being Relation holds P | ((dom P) \ X) = P \ [:X,(rng P):]

proof end;

definition

let P, Q be Relation;

coherence

(P \ [:(dom Q),(rng P):]) \/ Q is object ;

coherence

(P | ((dom P) \ (dom Q))) \/ Q is object ;

coherence

((P | (dom P)) \ (P | (dom Q))) \/ Q is object ;

end;
coherence

(P \ [:(dom Q),(rng P):]) \/ Q is object ;

coherence

(P | ((dom P) \ (dom Q))) \/ Q is object ;

coherence

((P | (dom P)) \ (P | (dom Q))) \/ Q is object ;

:: deftheorem defines +*1 FOMODEL0:def 29 :

for P, Q being Relation holds P +*1 Q = (P \ [:(dom Q),(rng P):]) \/ Q;

for P, Q being Relation holds P +*1 Q = (P \ [:(dom Q),(rng P):]) \/ Q;

:: deftheorem defines +*2 FOMODEL0:def 30 :

for P, Q being Relation holds P +*2 Q = (P | ((dom P) \ (dom Q))) \/ Q;

for P, Q being Relation holds P +*2 Q = (P | ((dom P) \ (dom Q))) \/ Q;

:: deftheorem defines +*3 FOMODEL0:def 31 :

for P, Q being Relation holds P +*3 Q = ((P | (dom P)) \ (P | (dom Q))) \/ Q;

for P, Q being Relation holds P +*3 Q = ((P | (dom P)) \ (P | (dom Q))) \/ Q;

registration

let P, Q be Relation;

compatibility

P +*1 Q = P +*2 Q by Lm58;

compatibility

P +*2 Q = P +*3 Q by RELAT_1:80;

end;
compatibility

P +*1 Q = P +*2 Q by Lm58;

compatibility

P +*2 Q = P +*3 Q by RELAT_1:80;

registration
end;

registration

let U be non empty set ;

let u be Element of U;

let q be U -valued FinSequence;

set f = U -firstChar ;

set p = <*u*>;

set P = <*u*> ^ q;

coherence

((U -firstChar) . (<*u*> ^ q)) \+\ u is empty

end;
let u be Element of U;

let q be U -valued FinSequence;

set f = U -firstChar ;

set p = <*u*>;

set P = <*u*> ^ q;

coherence

((U -firstChar) . (<*u*> ^ q)) \+\ u is empty

proof end;

registration

existence

ex b_{1} being Real st

( b_{1} is negative & b_{1} is integer )

for b_{1} being Integer st b_{1} is positive holds

b_{1} is natural
;

end;
ex b

( b

proof end;

coherence for b

b

registration

let X, Y be set ;

let x be Subset of X;

let y be Subset of Y;

coherence

for b_{1} being set st b_{1} = (x \ Y) \ (X \ y) holds

b_{1} is empty

end;
let x be Subset of X;

let y be Subset of Y;

coherence

for b

b

proof end;

registration

let X, Y be set ;

let x be Subset of X;

let y be Subset of Y;

coherence

for b_{1} being set st b_{1} = (x \ Y) \ (X \ y) holds

b_{1} is empty
;

end;
let x be Subset of X;

let y be Subset of Y;

coherence

for b

b

registration

let X, Y be set ;

let x be Subset of X;

coherence

for b_{1} being set st b_{1} = (x \ Y) \ (X \ Y) holds

b_{1} is empty

end;
let x be Subset of X;

coherence

for b

b

proof end;

registration

let X, Y be set ;

let x be Subset of X;

let y be Subset of Y;

coherence

for b_{1} being set st b_{1} = ((x \/ y) \ Y) \ X holds

b_{1} is empty

end;
let x be Subset of X;

let y be Subset of Y;

coherence

for b

b

proof end;

theorem :: FOMODEL0:68

registration

let T be trivial set ;

let x, y be Element of T;

coherence

for b_{1} being set st b_{1} = x \+\ y holds

b_{1} is empty

end;
let x, y be Element of T;

coherence

for b

b

proof end;

registration

let Y be set ;

let X be Subset of Y;

coherence

(proj1 X) \ (proj1 Y) is empty by XTUPLE_0:8, Th29;

coherence

(proj2 X) \ (proj2 Y) is empty by XTUPLE_0:9, Th29;

end;
let X be Subset of Y;

coherence

(proj1 X) \ (proj1 Y) is empty by XTUPLE_0:8, Th29;

coherence

(proj2 X) \ (proj2 Y) is empty by XTUPLE_0:9, Th29;

registration

let X, Y be set ;

coherence

(proj1 [:X,Y:]) \ X is empty by FUNCT_5:10, Th29;

coherence

((proj1 [:X,Y:]) /\ X) \+\ (proj1 [:X,Y:]) is empty

(proj2 [:X,Y:]) \ Y is empty by FUNCT_5:10, Th29;

coherence

((proj2 [:X,Y:]) /\ Y) \+\ (proj2 [:X,Y:]) is empty

((proj2 X) \/ (proj2 Y)) \+\ (proj2 (X \/ Y)) is empty by XTUPLE_0:27, Th29;

coherence

((proj1 X) \/ (proj1 Y)) \+\ (proj1 (X \/ Y)) is empty by XTUPLE_0:23, Th29;

let y be Subset of Y;

coherence

(X \ Y) /\ y is empty

end;
coherence

(proj1 [:X,Y:]) \ X is empty by FUNCT_5:10, Th29;

coherence

((proj1 [:X,Y:]) /\ X) \+\ (proj1 [:X,Y:]) is empty

proof end;

coherence (proj2 [:X,Y:]) \ Y is empty by FUNCT_5:10, Th29;

coherence

((proj2 [:X,Y:]) /\ Y) \+\ (proj2 [:X,Y:]) is empty

proof end;

coherence ((proj2 X) \/ (proj2 Y)) \+\ (proj2 (X \/ Y)) is empty by XTUPLE_0:27, Th29;

coherence

((proj1 X) \/ (proj1 Y)) \+\ (proj1 (X \/ Y)) is empty by XTUPLE_0:23, Th29;

let y be Subset of Y;

coherence

(X \ Y) /\ y is empty

proof end;

registration

let X be set ;

let U be non empty set ;

coherence

(proj1 [:X,U:]) \+\ X is empty

(proj2 [:U,X:]) \+\ X is empty

end;
let U be non empty set ;

coherence

(proj1 [:X,U:]) \+\ X is empty

proof end;

coherence (proj2 [:U,X:]) \+\ X is empty

proof end;

registration

let X be set ;

let Y be non empty set ;

reducibility

proj1 [:X,Y:] = X

proj2 [:Y,X:] = X

end;
let Y be non empty set ;

reducibility

proj1 [:X,Y:] = X

proof end;

reducibility proj2 [:Y,X:] = X

proof end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let f be non empty involutive Function;

let x be Element of dom f;

reducibility

f . (f . x) = x by PARTIT_2:def 2;

end;
let x be Element of dom f;

reducibility

f . (f . x) = x by PARTIT_2:def 2;

registration
end;

registration

let X be set ;

let P be Relation;

let x be Subset of X;

coherence

(P " x) \ (P " X) is empty by RELAT_1:143, Th29;

end;
let P be Relation;

let x be Subset of X;

coherence

(P " x) \ (P " X) is empty by RELAT_1:143, Th29;

registration
end;

registration

let X be set ;

let R be X -defined total Relation;

coherence

X \+\ (dom R) is empty by PARTFUN1:def 2, Th29;

end;
let R be X -defined total Relation;

coherence

X \+\ (dom R) is empty by PARTFUN1:def 2, Th29;

registration
end;

registration

let X be set ;

let Y be non empty set ;

let f be X -defined Y -valued total Function;

coherence

{f} \ (Funcs (X,Y)) is empty

end;
let Y be non empty set ;

let f be X -defined Y -valued total Function;

coherence

{f} \ (Funcs (X,Y)) is empty

proof end;

registration

let X be non empty set ;

let f be X -defined X -valued total Function;

coherence

(rng f) \ (dom f) is empty

end;
let f be X -defined X -valued total Function;

coherence

(rng f) \ (dom f) is empty

proof end;

registration
end;

:: deftheorem defines doubleton FOMODEL0:def 32 :

for a, b being set holds a doubleton b = {a} \/ {b};

for a, b being set holds a doubleton b = {a} \/ {b};

registration

let a, b be set ;

compatibility

{a,b} = a doubleton b by ENUMSET1:1;

compatibility

a doubleton b = {a,b} ;

compatibility

a doubleton b = b doubleton a ;

end;
compatibility

{a,b} = a doubleton b by ENUMSET1:1;

compatibility

a doubleton b = {a,b} ;

compatibility

a doubleton b = b doubleton a ;

registration

let P be Relation;

let X be set ;

compatibility

P .: X = P .:1 X by RELAT_1:115;

compatibility

P .:1 X = P .: X ;

end;
let X be set ;

compatibility

P .: X = P .:1 X by RELAT_1:115;

compatibility

P .:1 X = P .: X ;

definition

let P, Q be Relation;

:: original: +*1

redefine func P +*1 Q -> Subset of (P \/ Q);

coherence

P +*1 Q is Subset of (P \/ Q)

end;
:: original: +*1

redefine func P +*1 Q -> Subset of (P \/ Q);

coherence

P +*1 Q is Subset of (P \/ Q)

proof end;

Lm59: for f, g being Function

for x being Element of [:f,g:] st f <> {} & g <> {} holds

( x `1 is pair & x `2 is pair )

proof end;

registration

let f, g be non empty Function;

let x be Element of [:f,g:];

coherence

x `1 is pair by Lm59;

coherence

x `2 is pair by Lm59;

end;
let x be Element of [:f,g:];

coherence

x `1 is pair by Lm59;

coherence

x `2 is pair by Lm59;

Lm60: for B, C being set

for P being Relation holds P * [:B,C:] c= [:(P " B),C:]

proof end;

Lm61: for B, C being set

for P being Relation holds P * [:B,C:] = [:(P " B),C:]

proof end;

Lm62: for X, Y, Z, y being set st y <> {} & y c= Y holds

[:X,y:] * [:Y,Z:] = [:X,Z:]

proof end;

Lm63: for X being set

for P being Relation holds P * [:(rng P),X:] = [:(dom P),X:]

proof end;

Lm64: for f being Function st rng f = dom f holds

f is onto Function of (dom f),(dom f)

proof end;

Lm65: for f being Function st f is involutive holds

f * f c= id (dom f)

proof end;

Lm66: for X being set holds X /\ (id ((proj1 X) /\ (proj2 X))) = X /\ (id (proj1 X))

proof end;

Lm67: for X, Y being set holds (id X) | Y = id (X /\ Y)

proof end;

Lm68: for b1, b2 being set

for f1, f2 being Function st (rng f1) /\ (rng f2) = {} & b1 <> b2 & rng f1 c= dom f2 & rng f2 c= dom f1 holds

[:(rng f1),{b2}:] \/ [:(rng f2),{b1}:] c= ((f1 \/ f2) >*> ([:(rng f1),{b2}:] \/ [:(rng f2),{b1}:])) >*> ((b1,b2) --> (b2,b1))

proof end;

Lm69: for a, a1 being set

for f being Function st a in {a1,(f . a1)} & f is involutive & a1 in dom f holds

{a,(f . a)} = {a1,(f . a1)}

proof end;

Lm70: for a, a1 being set

for f being Function st ( a in {a1,(f . a1)} or f . a in {a1,(f . a1)} ) & f is involutive & a in dom f & a1 in dom f holds

{a,(f . a)} = {a1,(f . a1)}

proof end;

Lm71: for X being set

for f being Function st X c= f holds

dom (f \ X) = (dom f) \ (proj1 X)

proof end;

Lm72: for X being set st X <> {} holds

{ x where x is Element of X : verum } = X

proof end;

Lm73: for a1, a2, b1, b2 being set

for f, g being Function holds

( [[a1,a2],[b1,b2]] in [:f,g:] iff ( [a1,b1] in f & [a2,b2] in g ) )

proof end;

Lm74: for X, Y being set holds

( X = Y iff for x being set st x in X \/ Y holds

( x in X iff x in Y ) )

proof end;

Lm75: for x being set

for f, g being Function st x in [:f,g:] holds

x = [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]]

proof end;

Lm76: for f1, f2, g1, g2 being Function holds [:f1,f2:] /\ [:g1,g2:] = [:(f1 /\ g1),(f2 /\ g2):]

proof end;

definition
end;

:: deftheorem Def34 defines oneone FOMODEL0:def 34 :

for P being Relation holds

( P is oneone iff P ~ is Function-like );

for P being Relation holds

( P is oneone iff P ~ is Function-like );

registration

coherence

for b_{1} being Function st b_{1} is one-to-one holds

b_{1} is oneone
;

coherence

for b_{1} being Function st b_{1} is oneone holds

b_{1} is one-to-one

end;
for b

b

coherence

for b

b

proof end;

registration
end;

registration

existence

ex b_{1} being Function st

( not b_{1} is empty & b_{1} is one-to-one )

coherence

for b_{1} being Subset of P holds b_{1} is oneone

end;
ex b

( not b

proof end;

let P be oneone Relation;coherence

for b

proof end;

definition

let R be set ;

coherence

proj1 (R /\ (id (proj1 R))) is set ;

coherence

proj1 (R /\ (id ((proj1 R) /\ (proj2 R)))) is set ;

end;
coherence

proj1 (R /\ (id (proj1 R))) is set ;

coherence

proj1 (R /\ (id ((proj1 R) /\ (proj2 R)))) is set ;

:: deftheorem defines fixpoints FOMODEL0:def 35 :

for R being set holds fixpoints R = proj1 (R /\ (id (proj1 R)));

for R being set holds fixpoints R = proj1 (R /\ (id (proj1 R)));

:: deftheorem defines fixpoints1 FOMODEL0:def 36 :

for R being set holds fixpoints1 R = proj1 (R /\ (id ((proj1 R) /\ (proj2 R))));

for R being set holds fixpoints1 R = proj1 (R /\ (id ((proj1 R) /\ (proj2 R))));

registration
end;

Lm77: for R being Relation holds fixpoints1 R = fixpoints1 (R ~)

proof end;

registration
end;

registration
end;

registration

let R be set ;

compatibility

fixpoints R = fixpoints1 R by Lm66;

compatibility

fixpoints1 R = fixpoints R ;

end;
compatibility

fixpoints R = fixpoints1 R by Lm66;

compatibility

fixpoints1 R = fixpoints R ;

Lm78: for f being Function

for x being object holds

( x in fixpoints f iff x is_a_fixpoint_of f )

proof end;

Lm79: for f, g being Function holds fixpoints [:f,g:] = [:(fixpoints f),(fixpoints g):]

proof end;

registration
end;

registration

let X be non empty set ;

ex b_{1} being Permutation of X st

( b_{1} is with_fixpoint & not b_{1} is empty & b_{1} is symmetric )

end;
cluster Relation-like X -defined X -valued Function-like one-to-one non empty total quasi_total onto bijective symmetric with_fixpoint oneone for Element of bool [:X,X:];

existence ex b

( b

proof end;

registration

existence

ex b_{1} being Function st

( b_{1} is with_fixpoint & not b_{1} is empty & b_{1} is symmetric )

end;
ex b

( b

proof end;

registration
end;

registration
end;

registration
end;

definition
end;

:: deftheorem Def37 defines constanT FOMODEL0:def 37 :

for X being set holds

( X is constanT iff proj2 X is trivial );

for X being set holds

( X is constanT iff proj2 X is trivial );

registration
end;

registration

coherence

for b_{1} being Function st b_{1} is constant holds

b_{1} is constanT
;

coherence

for b_{1} being Function st b_{1} is constanT holds

b_{1} is constant
;

end;
for b

b

coherence

for b

b

Lm80: for X being set

for P being Relation st not X is empty & X is trivial & P is X -valued holds

P is constant Function

proof end;

registration

let x be trivial set ;

coherence

for b_{1} being Relation st b_{1} is x -valued holds

b_{1} is Function-like

end;
coherence

for b

b

proof end;

registration

let x be trivial set ;

coherence

for b_{1} being Function st b_{1} is x -valued holds

b_{1} is constant
;

end;
coherence

for b

b

registration
end;

registration
end;

registration
end;

registration
end;

theorem :: FOMODEL0:69

theorem :: FOMODEL0:70

theorem :: FOMODEL0:71

theorem :: FOMODEL0:73

theorem :: FOMODEL0:74

theorem :: FOMODEL0:75

theorem :: FOMODEL0:76

theorem :: FOMODEL0:77

theorem :: FOMODEL0:78

::#######################################################################