:: Preliminaries to Classical First-order Model Theory
:: by Marco B. Caminati
::
:: Copyright (c) 2010-2019 Association of Mizar Users

::################### Preliminary Definitions #########################
::#######################################################################
definition
let X be set ;
let f be Function;
attr f is X -one-to-one means :: FOMODEL0:def 1
f | X is one-to-one ;
end;

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

definition
let D be non empty set ;
let f be BinOp of D;
let X be set ;
attr X is f -unambiguous means :: FOMODEL0:def 2
f is [:X,D:] -one-to-one ;
end;

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

definition
let D be non empty set ;
let X be set ;
attr X is D -prefix means :: FOMODEL0:def 3
X is D -concatenation -unambiguous ;
end;

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

definition
let f be Function-yielding Function;
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
ex b1 being Function st
( dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds
b1 . x = (f . x) . (g . x) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = (dom f) /\ (dom g) & ( for x being set st x in dom b1 holds
b1 . x = (f . x) . (g . x) ) & dom b2 = (dom f) /\ (dom g) & ( for x being set st x in dom b2 holds
b2 . x = (f . x) . (g . x) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines ^^^ FOMODEL0:def 4 :
for f being Function-yielding Function
for g, b3 being Function holds
( b3 = ^^^f,g__ iff ( dom b3 = (dom f) /\ (dom g) & ( for x being set st x in dom b3 holds
b3 . x = (f . x) . (g . x) ) ) );

definition
let D be set ;
func D -pr1 -> BinOp of D equals :: FOMODEL0:def 5
pr1 (D,D);
coherence
pr1 (D,D) is BinOp of D
;
end;

:: deftheorem defines -pr1 FOMODEL0:def 5 :
for D being set holds D -pr1 = pr1 (D,D);

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 () /\ (B *) c= m -tuples_on B

proof end;

theorem Th1: :: FOMODEL0:1
for A, B being set
for m being Nat holds () /\ (B *) = () /\ ()
proof end;

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

theorem Th2: :: FOMODEL0:2
for A, B being set
for m being Nat holds () /\ (B *) = m -tuples_on (A /\ B)
proof end;

theorem Th3: :: FOMODEL0:3
for A, B being set
for m being Nat holds m -tuples_on (A /\ B) = () /\ ()
proof end;

Lm10: for D being non empty set
for x, y being FinSequence of D holds () . (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
() . (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 *) \ )
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 ############################
registration
let D be non empty set ;
cluster D -pr1 -> associative for BinOp of D;
coherence
for b1 being BinOp of D st b1 = D -pr1 holds
b1 is associative
proof end;
end;

registration
let D be set ;
existence
ex b1 being BinOp of D st b1 is associative
proof end;
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;

registration
let D be non empty set ;
cluster D -concatenation -> associative for BinOp of (D *);
coherence
for b1 being BinOp of (D *) st b1 = D -concatenation holds
b1 is associative
by MONOID_0:67;
end;

registration
let D be non empty set ;
cluster (D *) \ -> non empty ;
coherence
not (D *) \ is empty
proof end;
end;

registration
let D be non empty set ;
let m be Nat;
existence
ex b1 being Element of D * st b1 is m -element
proof end;
end;

definition
let X be set ;
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
( 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;

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

registration
let D be non empty set ;
let f be BinOp of D;
existence
ex b1 being set st b1 is f -unambiguous
proof end;
end;

registration
let f be Function;
let x be set ;
cluster f | {x} -> one-to-one for Function;
coherence
for b1 being Function st b1 = f | {x} holds
b1 is one-to-one
proof end;
end;

registration
let e be empty set ;
identify e * with {e};
compatibility
e * = {e}
by FUNCT_7:17;
identify {e} with e * ;
compatibility
{e} = e *
;
end;

registration
coherence
for b1 being set st b1 is empty holds
b1 is empty-membered
;
let e be empty set ;
coherence
proof end;
end;

registration
let U be non empty set ;
let m1 be non zero Nat;
coherence
proof end;
end;

registration
let X be empty-membered set ;
cluster -> empty-membered for Element of bool X;
coherence
for b1 being Subset of X holds b1 is empty-membered
proof end;
end;

registration
let A be set ;
let m0 be zero number ;
cluster m0 -tuples_on A -> empty-membered for set ;
coherence
for b1 being set st b1 = m0 -tuples_on A holds
b1 is empty-membered
by Lm6;
end;

registration
let e be empty set ;
let m1 be non zero Nat;
cluster m1 -tuples_on e -> empty for set ;
coherence
for b1 being set st b1 = m1 -tuples_on e holds
b1 is empty
by FINSEQ_3:119;
end;

registration
let D be non empty set ;
let f be BinOp of D;
let e be empty set ;
cluster e typed/\ f -> f -unambiguous for set ;
coherence
for b1 being set st b1 = e /\ f holds
b1 is f -unambiguous
by Lm12;
end;

registration
let U be non empty set ;
let e be empty set ;
cluster e typed/\ U -> U -prefix for set ;
coherence
for b1 being set st b1 = e /\ U holds
b1 is U -prefix
proof end;
end;

registration
let U be non empty set ;
cluster U -prefix for set ;
existence
ex b1 being set st b1 is U -prefix
proof end;
end;

::############################ Type tuning ############################
::############################## END ##################################
::########################### MultPlace ###############################
definition
let D be non empty set ;
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
ex b1 being Function st
( dom b1 = NAT & b1 . 0 = x . 1 & ( for n being Nat holds b1 . (n + 1) = f . ((b1 . n),(x . (n + 2))) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = NAT & b1 . 0 = x . 1 & ( for n being Nat holds b1 . (n + 1) = f . ((b1 . n),(x . (n + 2))) ) & dom b2 = NAT & b2 . 0 = x . 1 & ( for n being Nat holds b2 . (n + 1) = f . ((b2 . n),(x . (n + 2))) ) holds
b1 = b2
proof end;
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 b4 being Function holds
( b4 = MultPlace (f,x) iff ( dom b4 = NAT & b4 . 0 = x . 1 & ( for n being Nat holds b4 . (n + 1) = f . ((b4 . n),(x . (n + 2))) ) ) );

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 *) \ ;
func MultPlace (f,x) -> Function equals :: FOMODEL0:def 8
MultPlace (f,x);
coherence
MultPlace (f,x) is Function
;
end;

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

definition
let D be non empty set ;
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
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
ex b1 being Function of ((D *) \ ),D st
for x being Element of (D *) \ holds b1 . x = (MultPlace (f,x)) . ((len x) - 1)
proof end;
uniqueness
for b1, b2 being Function of ((D *) \ ),D st ( for x being Element of (D *) \ holds b1 . x = (MultPlace (f,x)) . ((len x) - 1) ) & ( for x being Element of (D *) \ holds b2 . x = (MultPlace (f,x)) . ((len x) - 1) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines MultPlace FOMODEL0:def 9 :
for D being non empty set
for f being BinOp of D
for b3 being Function of ((D *) \ ),D holds
( b3 = MultPlace f iff for x being Element of (D *) \ holds b3 . x = (MultPlace (f,x)) . ((len x) - 1) );

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
( () . <*y*> = y & () . (x ^ <*y*>) = 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 ;
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
( 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;

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

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 () . (<*d*> ^ x) = f . (d,(() . 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
() .: ((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
() .: ((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 ###############################
definition
let D be non empty set ;
::# A function-like extracting the first item of a non empty FinSequence of D
func D -firstChar -> Function of ((D *) \ ),D equals :: FOMODEL0:def 11
MultPlace (D -pr1);
coherence
MultPlace (D -pr1) is Function of ((D *) \ ),D
;
end;

:: deftheorem defines -firstChar FOMODEL0:def 11 :
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 () . 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
() . 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
definition
let D be non empty set ;
func D -multiCat -> Function equals :: FOMODEL0:def 12
() +* ();
coherence
() +* () is Function
;
end;

:: deftheorem defines -multiCat FOMODEL0:def 12 :
for D being non empty set holds D -multiCat = () +* ();

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

Lm23: for D being non empty set holds () | (((D *) *) \ ) = MultPlace ()
proof end;

Lm24: for Y being set
for D being non empty set holds () | () = () | Y

proof end;

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

registration
let D be non empty set ;
let e be empty set ;
cluster () . e -> empty for set ;
coherence
for b1 being set st b1 = () . e holds
b1 is empty
proof end;
end;

registration
let D be non empty set ;
cluster -> D -prefix for Element of bool ();
coherence
for b1 being Subset of () holds b1 is D -prefix
proof end;
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
() .: () 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
proof end;

theorem :: FOMODEL0:9
for Y being set
for m being Nat holds (m + 1) -tuples_on Y c= (Y *) \
proof end;

theorem :: FOMODEL0:10
for Y being set
for m being Nat st m is zero holds
m -tuples_on Y = by Lm6;

theorem :: FOMODEL0:11
for Y being set
for i being Nat holds i -tuples_on Y = Funcs ((Seg i),Y) by Lm7;

::#extending FUNCT_2:111
theorem :: FOMODEL0:12
for A, x being set
for m being Nat st x in m -tuples_on A holds
x is FinSequence of A
proof end;

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

theorem :: FOMODEL0:13
for D being non empty set
for d being Element of D
for f being BinOp of D holds
( () . <*d*> = d & ( for x being non empty FinSequence of D holds () . (x ^ <*d*>) = f . ((() . x),d) ) ) by Lm15;

theorem Th14: :: FOMODEL0:14
for D being non empty set
for d being non empty Element of (D *) * holds () . d = () . d
proof end;

theorem :: FOMODEL0:15
for D being non empty set
for d1, d2 being Element of D * holds () . <*d1,d2*> = d1 ^ d2
proof end;

registration
let f, g be FinSequence;
coherence
<:f,g:> is FinSequence-like
proof end;
end;

registration
let m be Nat;
let f, g be m -element FinSequence;
cluster <:f,g:> -> m -element ;
coherence
<:f,g:> is m -element
proof end;
end;

registration
let X, Y be set ;
let f be X -defined Function;
let g be Y -defined Function;
cluster <:f,g:> -> X /\ Y -defined for Function;
coherence
for b1 being Function st b1 = <:f,g:> holds
b1 is X /\ Y -defined
proof end;
end;

registration
let X be set ;
let f, g be X -defined Function;
cluster <:f,g:> -> X -defined for Function;
coherence
for b1 being Function st b1 = <:f,g:> holds
b1 is X -defined
;
end;

registration
let X, Y be set ;
let f be X -defined total Function;
let g be Y -defined total Function;
cluster <:f,g:> -> X /\ Y -defined total for X /\ Y -defined Function;
coherence
for b1 being X /\ Y -defined Function st b1 = <:f,g:> holds
b1 is total
proof end;
end;

registration
let X be set ;
let f, g be X -defined total Function;
cluster <:f,g:> -> X -defined total for X -defined Function;
coherence
for b1 being X -defined Function st b1 = <:f,g:> holds
b1 is total
;
end;

registration
let X, Y be set ;
let f be X -valued Function;
let g be Y -valued Function;
cluster <:f,g:> -> [:X,Y:] -valued for Function;
coherence
for b1 being Function st b1 = <:f,g:> holds
b1 is [:X,Y:] -valued
proof end;
end;

registration
let D be non empty set ;
existence
ex b1 being FinSequence st b1 is D -valued
proof end;
end;

registration
let D be non empty set ;
let m be Nat;
existence
ex b1 being D -valued FinSequence st b1 is m -element
proof end;
end;

registration
let X, Y be non empty set ;
let f be Function of X,Y;
let p be X -valued FinSequence;
coherence
proof end;
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;
cluster p >*> f -> m -element for set ;
coherence
for b1 being set st b1 = f * p holds
b1 is m -element
proof end;
end;

definition
let D be non empty set ;
let f be BinOp of D;
let p, q be Element of D * ;
func f AppliedPairwiseTo (p,q) -> FinSequence of D equals :: FOMODEL0:def 13
f * <:p,q:>;
coherence
f * <:p,q:> is FinSequence of D
proof end;
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:>;

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 * ;
cluster f AppliedPairwiseTo (p,q) -> m -element for set ;
coherence
for b1 being set st b1 = f AppliedPairwiseTo (p,q) holds
b1 is m -element
;
end;

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;

definition
redefine func INT equals :: FOMODEL0:def 14
NAT \/ ();
compatibility
for b1 being set holds
( b1 = INT iff b1 = NAT \/ () )
proof end;
end;

:: deftheorem defines INT FOMODEL0:def 14 :
INT = NAT \/ ();

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

notation
let A, B be set ;
synonym A typed/\ B for A /\ B;
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;

registration
let A, B be set ;
identify A typed/\ B with B typed/\ A;
compatibility
A typed/\ B = B typed/\ A
;
end;

registration
let A, B be set ;
identify A typed/\ B with A typed/\ B;
compatibility
A typed/\ B = A typed/\ B
;
end;

definition
let B, A be object ;
func A null B -> set equals :: FOMODEL0:def 15
A;
coherence
A is set
by TARSKI:1;
end;

:: deftheorem defines null FOMODEL0:def 15 :
for B, A being object holds A null B = A;

registration
let A, B be set ;
reduce A null B to A;
reducibility
A null B = A
;
end;

registration
let A be set ;
let B be Subset of A;
identify A /\ B with B null A;
compatibility
A /\ B = B null A
by XBOOLE_1:28;
identify B null A with A /\ B;
compatibility
B null A = A /\ B
;
end;

registration
let A, B, C be set ;
cluster (B \ A) typed/\ (A /\ C) -> empty for set ;
coherence
for b1 being set st b1 = (B \ A) /\ (A /\ C) holds
b1 is empty
proof end;
end;

definition
let A, B be set ;
func A typed\ B -> Subset of A equals :: FOMODEL0:def 16
A \ B;
coherence
A \ B is Subset of A
;
end;

:: deftheorem defines typed\ FOMODEL0:def 16 :
for A, B being set holds A typed\ B = A \ B;

registration
let A, B be set ;
identify A \ B with A typed\ B;
compatibility
A \ B = A typed\ B
;
end;

definition
let A, B be set ;
::# 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
func A \typed/ B -> Subset of (A \/ B) equals :: FOMODEL0:def 17
A;
coherence
A is Subset of (A \/ B)
by XBOOLE_1:7;
end;

:: deftheorem defines \typed/ FOMODEL0:def 17 :
for A, B being set holds A \typed/ B = A;

registration
let A, B be set ;
identify A \typed/ B with A null B;
compatibility
A \typed/ B = A null B
;
identify A null B with A \typed/ B;
compatibility
A null B = A \typed/ B
;
end;

registration
let A be set ;
let B be Subset of A;
identify A \/ B with A null B;
compatibility
A \/ B = A null B
by XBOOLE_1:12;
identify A null B with A \/ B;
compatibility
A null B = A \/ B
;
end;

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 ;

registration
let R be Relation;
cluster R [*] -> transitive for Relation;
coherence
for b1 being Relation st b1 = R [*] holds
b1 is transitive
proof end;
cluster R [*] -> reflexive for Relation;
coherence
for b1 being Relation st b1 = R [*] holds
b1 is reflexive
proof end;
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
func plus -> Function of COMPLEX,COMPLEX means :Def18: :: FOMODEL0:def 18
for z being Complex holds it . z = z + 1;
existence
ex b1 being Function of COMPLEX,COMPLEX st
for z being Complex holds b1 . z = z + 1
proof end;
uniqueness
for b1, b2 being Function of COMPLEX,COMPLEX st ( for z being Complex holds b1 . z = z + 1 ) & ( for z being Complex holds b2 . z = z + 1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines plus FOMODEL0:def 18 :
for b1 being Function of COMPLEX,COMPLEX holds
( b1 = plus iff for z being Complex holds b1 . z = z + 1 );

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
for f being Function st rng f c= dom f holds
f [*] = union { (iter (f,mm)) where mm is Element of NAT : verum } by Lm37;

theorem :: FOMODEL0:18
for g being Function
for m being Nat
for f being Function st f c= g holds
iter (f,m) c= iter (g,m) by Lm26;

registration
let X be functional set ;
cluster union X -> Relation-like for set ;
coherence
for b1 being set st b1 = union X holds
b1 is Relation-like
proof end;
end;

theorem :: FOMODEL0:19
for A, B, Y being set st Y c= Funcs (A,B) holds
union Y c= [:A,B:] by Lm2;

registration
let Y be set ;
let R be Y -valued Relation;
identify Y | R with R null Y;
compatibility
Y | R = R null Y
;
end;

registration
let Y be set ;
cluster Y \ Y -> empty for set ;
coherence
for b1 being set st b1 = Y \ Y holds
b1 is empty
by XBOOLE_1:37;
end;

registration
let D be non empty set ;
let d be Element of D;
cluster {((id D) . d)} \ {d} -> empty for set ;
coherence
for b1 being set st b1 = {((id D) . d)} \ {d} holds
b1 is empty
;
end;

registration
let p be FinSequence;
let q be empty FinSequence;
identify p ^ q with p null q;
compatibility
p ^ q = p null q
by FINSEQ_1:34;
identify p null q with p ^ q;
compatibility
p null q = p ^ q
;
identify q ^ p with p null q;
compatibility
q ^ p = p null q
by FINSEQ_1:34;
identify p null q with q ^ p;
compatibility
p null q = q ^ p
;
end;

registration
let Y be set ;
let R be Y -defined Relation;
identify R | Y with R null Y;
compatibility
R | Y = R null Y
;
identify R null Y with R | Y;
compatibility
R null Y = R | Y
;
end;

theorem Th20: :: FOMODEL0:20
for f being Function holds f = { [x,(f . x)] where x is Element of dom f : x in dom f }
proof end;

theorem Th21: :: FOMODEL0:21
for Y being set
for R being b1 -defined total Relation holds id Y c= R * (R ~)
proof end;

theorem :: FOMODEL0:22
for D being non empty set
for m, n being Nat holds (m + n) -tuples_on D = () .: [:(),():]
proof end;

theorem Th23: :: FOMODEL0:23
for Y being set
for P, Q being Relation holds (P \/ Q) " Y = (P " Y) \/ (Q " Y)
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:24
for A, B being set holds
( (chi (A,B)) " = B \ A & (chi (A,B)) " {1} = A /\ B )
proof end;

theorem :: FOMODEL0:25
for x being set
for f being Function
for y being non empty set holds
( y = f . x iff x in f " {y} )
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;

registration
let Y be set ;
let X be Subset of Y;
coherence
for b1 being Relation st b1 is X -valued holds
b1 is Y -valued
by XBOOLE_1:1;
end;

Lm41: for Y being set
for R being b1 -defined total Relation ex f being Function of Y,(rng R) st
( 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 b1 -defined Relation st Q is total & R is Y -defined & ((P * Q) * (Q ~)) * R is Function-like & rng P c= dom R holds
((P * Q) * (Q ~)) * R = P * R

proof end;

registration
let A be set ;
let U be non empty set ;
cluster quasi_total -> total for Element of bool [:A,U:];
coherence
for b1 being Relation of A,U st b1 is quasi_total holds
b1 is total
;
end;

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

theorem :: FOMODEL0:28
for p, q being FinSequence st not p is empty holds
(p ^ q) . 1 = p . 1
proof end;

registration
let U be non empty set ;
let p, q be U -valued FinSequence;
cluster p ^ q -> U -valued for FinSequence;
coherence
for b1 being FinSequence st b1 = p ^ q holds
b1 is U -valued
proof end;
end;

definition
let X be set ;
:: original: FinSequence
redefine mode FinSequence of X -> Element of X * ;
coherence
for b1 being FinSequence of X holds b1 is Element of X *
by FINSEQ_1:def 11;
end;

definition
let U be non empty set ;
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
( 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;
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 b1 -valued FinSequence st p1 in X & p2 in X & p1 ^ q1 = p2 ^ q2 holds
( p1 = p2 & q1 = q2 ) );

registration
let X be set ;
cluster -> X -valued for Element of X * ;
coherence
for b1 being Element of X * holds b1 is X -valued
;
end;

registration
let U be non empty set ;
let m be Nat;
let X be U -prefix set ;
cluster () .: () -> U -prefix for set ;
coherence
for b1 being set st b1 = () .: () holds
b1 is U -prefix
by Th7;
end;

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

registration
let P be Relation;
cluster P \ [:(dom P),(rng P):] -> empty ;
coherence
P \ [:(dom P),(rng P):] is empty
by ;
end;

registration
let X, Y, Z be set ;
cluster ((X \/ Y) \/ Z) \+\ (X \/ (Y \/ Z)) -> empty ;
coherence
((X \/ Y) \/ Z) \+\ (X \/ (Y \/ Z)) is empty
by ;
end;

registration
let x be set ;
cluster (id {x}) \+\ {[x,x]} -> empty for set ;
coherence
for b1 being set st b1 = (id {x}) \+\ {[x,x]} holds
b1 is empty
proof end;
end;

registration
let x, y be set ;
cluster (x .--> y) \+\ {[x,y]} -> empty for set ;
coherence
for b1 being set st b1 = (x .--> y) \+\ {[x,y]} holds
b1 is empty
proof end;
end;

registration
let x be set ;
cluster (id {x}) \+\ (x .--> x) -> empty for set ;
coherence
for b1 being set st b1 = (id {x}) \+\ (x .--> x) holds
b1 is empty
proof end;
end;

theorem :: FOMODEL0:30
for x being set
for D being non empty set holds
( x in (D *) \ iff ( x is b2 -valued FinSequence & not x is empty ) )
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
( () . <*d*> = d & ( for x being b1 -valued FinSequence st not x is empty holds
() . (x ^ <*d*>) = f . ((() . x),d) ) )
proof end;

registration
let p be FinSequence;
let x, y be set ;
cluster p +~ (x,y) -> FinSequence-like ;
coherence
p +~ (x,y) is FinSequence-like
proof end;
end;

definition
let x, y be set ;
let p be FinSequence;
func (x,y) -SymbolSubstIn p -> FinSequence equals :: FOMODEL0:def 20
p +~ (x,y);
coherence
p +~ (x,y) is FinSequence
;
end;

:: deftheorem defines -SymbolSubstIn FOMODEL0:def 20 :
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;
cluster (x,y) -SymbolSubstIn p -> m -element for FinSequence;
coherence
for b1 being FinSequence st b1 = (x,y) -SymbolSubstIn p holds
b1 is m -element
proof end;
end;

registration
let x be set ;
let U be non empty set ;
let u be Element of U;
let p be U -valued FinSequence;
cluster (x,u) -SymbolSubstIn p -> U -valued for FinSequence;
coherence
for b1 being FinSequence st b1 = (x,u) -SymbolSubstIn p holds
b1 is U -valued
;
end;

definition
let X, x, y be set ;
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
for b1 being FinSequence holds
( b1 = (x,y) -SymbolSubstIn p iff b1 = ((id X) +* (x,y)) * p )
proof end;
end;

:: deftheorem defines -SymbolSubstIn FOMODEL0:def 21 :
for X, x, y being set
for p being b1 -valued FinSequence holds (x,y) -SymbolSubstIn p = ((id X) +* (x,y)) * p;

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;

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 b2 -valued FinSequence holds (x,u) -SymbolSubstIn (q1 ^ q2) = ((x,u) -SymbolSubstIn q1) ^ ((x,u) -SymbolSubstIn q2)

proof end;

definition
let U be non empty set ;
let x be set ;
let u be Element of U;
set D = U * ;
deffunc H1( Element of U * ) -> FinSequence of U = (x,u) -SymbolSubstIn \$1;
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
ex b1 being Function of (U *),(U *) st
for q being U -valued FinSequence holds b1 . q = (x,u) -SymbolSubstIn q
proof end;
uniqueness
for b1, b2 being Function of (U *),(U *) st ( for q being U -valued FinSequence holds b1 . q = (x,u) -SymbolSubstIn q ) & ( for q being U -valued FinSequence holds b2 . q = (x,u) -SymbolSubstIn q ) holds
b1 = b2
proof end;
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 b4 being Function of (U *),(U *) holds
( b4 = x SubstWith u iff for q being b1 -valued FinSequence holds b4 . q = (x,u) -SymbolSubstIn q );

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 b1 being Function st b1 = x SubstWith u holds
b1 is FinSequence-yielding
proof end;
end;

registration
let F be FinSequence-yielding Function;
let x be set ;
coherence
proof end;
end;

Lm47: for x being set
for U being non empty set
for u being Element of U
for q1, q2 being b2 -valued FinSequence holds () . (q1 ^ q2) = (() . q1) ^ (() . q2)

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;
cluster () . p -> m -element for FinSequence;
coherence
for b1 being FinSequence st b1 = () . p holds
b1 is m -element
proof end;
end;

registration
let U be non empty set ;
let x be set ;
let u be Element of U;
let e be empty set ;
cluster () . e -> empty for set ;
coherence
for b1 being set st b1 = () . e holds
b1 is empty
proof end;
end;

registration
let U be non empty set ;
coherence
for b1 being Function st b1 = U -multiCat holds
b1 is FinSequence-yielding
proof end;
end;

registration
let U be non empty set ;
existence
not for b1 being U -valued FinSequence holds b1 is empty
proof end;
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;
cluster {(p . m1)} \ U -> empty for set ;
coherence
for b1 being set st b1 = {(p . m1)} \ U holds
b1 is empty
proof end;
end;

registration
let U be non empty set ;
let m, n be Nat;
let p be (m + 1) + n -element Element of U * ;
cluster {(p . (m + 1))} \ U -> empty for set ;
coherence
for b1 being set st b1 = {(p . (m + 1))} \ U holds
b1 is empty
;
end;

registration
let x be set ;
cluster <*x*> \+\ {[1,x]} -> empty for set ;
coherence
for b1 being set st b1 = <*x*> \+\ {[1,x]} holds
b1 is empty
;
end;

registration
let m be Nat;
let p be m + 1 -element FinSequence;
cluster ((p | (Seg m)) ^ <*(p . (m + 1))*>) \+\ p -> empty for set ;
coherence
for b1 being set st b1 = ((p | (Seg m)) ^ <*(p . (m + 1))*>) \+\ p holds
b1 is empty
proof end;
end;

registration
let m, n be Nat;
let p be m + n -element FinSequence;
cluster p | (Seg m) -> m -element for FinSequence;
coherence
for b1 being FinSequence st b1 = p | (Seg m) holds
b1 is m -element
proof end;
end;

registration
coherence
for b1 being Relation st b1 is -valued holds
b1 is empty-yielding
;
coherence
for b1 being Relation st b1 is empty-yielding holds
b1 is -valued
;
end;

theorem Th32: :: FOMODEL0:32
for x being set
for U being non empty set holds () . x = () . x
proof end;

theorem Th33: :: FOMODEL0:33
for U being non empty set
for p being FinSequence
for q being b1 -valued FinSequence st p is U * -valued holds
() . (p ^ <*q*>) = (() . 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
() . (() . p) = () . (() * p)

proof end;

registration
let Y be set ;
let X be Subset of Y;
let R be Y -defined total Relation;
cluster R | X -> X -defined total for X -defined Relation;
coherence
for b1 being X -defined Relation st b1 = R | X holds
b1 is total
proof end;
end;

theorem :: FOMODEL0:34
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*> ) ) by Lm44;

theorem :: FOMODEL0:35
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*> ) ) by Lm46;

theorem :: FOMODEL0:36
for x being set
for U being non empty set
for u being Element of U
for q1, q2 being b2 -valued FinSequence holds () . (q1 ^ q2) = (() . q1) ^ (() . q2) by Lm47;

theorem :: FOMODEL0:37
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
() . (() . p) = () . (() * p) by Lm48;

theorem :: FOMODEL0:38
for U being non empty set holds () .: (id ()) = { <*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;
cluster ((f | U) . u) \+\ (f . u) -> empty for set ;
coherence
for b1 being set st b1 = ((f | U) . u) \+\ (f . u) holds
b1 is empty
proof end;
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;
cluster ((f * g) . u) \+\ (f . (g . u)) -> empty for set ;
coherence
for b1 being set st b1 = ((f * g) . u) \+\ (f . (g . u)) holds
b1 is empty
proof end;
end;

registration
cluster integer non negative -> natural for object ;
coherence
for b1 being Integer st not b1 is negative holds
b1 is natural
proof end;
end;

registration
let x, y be Real;
cluster (max (x,y)) - x -> non negative for ExtReal;
coherence
for b1 being ExtReal st b1 = (max (x,y)) - x holds
not b1 is negative
proof end;
end;

theorem :: FOMODEL0:39
for x being set st x is boolean holds
( x = 1 iff x <> 0 ) by XBOOLEAN:def 3;

registration
let Y be set ;
let X be Subset of Y;
cluster X \ Y -> empty for set ;
coherence
for b1 being set st b1 = X \ Y holds
b1 is empty
by XBOOLE_1:37;
end;

registration
let x, y be object ;
cluster {x} \ {x,y} -> empty for set ;
coherence
for b1 being set st b1 = {x} \ {x,y} holds
b1 is empty
proof end;
end;

registration
let x, y be set ;
cluster ([x,y] 1) \+\ x -> empty for set ;
coherence
for b1 being set st b1 = ([x,y] 1) \+\ x holds
b1 is empty
;
end;

registration
let x, y be set ;
cluster ([x,y] 2) \+\ y -> empty for set ;
coherence
for b1 being set st b1 = ([x,y] 2) \+\ y holds
b1 is empty
;
end;

registration
let n be positive Nat;
let X be non empty set ;
existence
ex b1 being Element of (X *) \ st b1 is n -element
proof end;
end;

registration
let m1 be non zero Nat;
coherence
for b1 being FinSequence st b1 is m1 + 0 -element holds
not b1 is empty
;
end;

registration
let R be Relation;
let x be set ;
cluster R null x -> Relation-like for set ;
coherence
for b1 being set st b1 = R null x holds
b1 is Relation-like
;
end;

registration
let f be Function-like set ;
let x be set ;
cluster f null x -> Function-like for set ;
coherence
for b1 being set st b1 = f null x holds
b1 is Function-like
;
end;

registration
let p be FinSequence-like Relation;
let x be set ;
coherence
for b1 being Relation st b1 = p null x holds
b1 is FinSequence-like
;
end;

registration
let p be FinSequence;
let x be set ;
cluster p null x -> len p -element for FinSequence;
coherence
for b1 being FinSequence st b1 = p null x holds
b1 is len p -element
by CARD_1:def 7;
end;

registration
let p be non empty FinSequence;
cluster len p -> non zero for number ;
coherence
for b1 being number st b1 = len p holds
not b1 is zero
;
end;

registration
let R be Relation;
let X be set ;
cluster R | X -> X -defined for Relation;
coherence
for b1 being Relation st b1 = R | X holds
b1 is X -defined
by RELAT_1:58;
end;

registration
let x be set ;
let e be empty set ;
cluster e null x -> empty for set ;
coherence
for b1 being set st b1 = e null x holds
b1 is empty
;
end;

registration
let X be set ;
let e be empty set ;
cluster e null X -> X -valued for Relation;
coherence
for b1 being Relation st b1 = e null X holds
b1 is X -valued
proof end;
end;

registration
let Y be non empty FinSequence-membered set ;
coherence
for b1 being Function st b1 is Y -valued holds
b1 is FinSequence-yielding
proof end;
end;

registration
let X, Y be set ;
cluster -> FinSequence-yielding for Element of Funcs (X,(Y *));
coherence
for b1 being Element of Funcs (X,(Y *)) holds b1 is FinSequence-yielding
;
end;

theorem Th40: :: FOMODEL0:40
for X, x being set
for f being Function st f is X * -valued holds
f . x in X *
proof end;

registration
let m, n be Nat;
let p be m -element FinSequence;
cluster p null n -> Seg (m + n) -defined for Relation;
coherence
for b1 being Relation st b1 = p null n holds
b1 is Seg (m + n) -defined
proof end;
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;
cluster p ^ q -> m + n -element for FinSequence;
coherence
for b1 being FinSequence st b1 = p ^ q holds
b1 is m + n -element
;
end;

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

theorem :: FOMODEL0:42
for x being set
for U, U1 being non empty set st () . x is U1 -valued & x in (U *) * holds
x is FinSequence of U1 *
proof end;

registration
let U be non empty set ;
existence
ex b1 being reflexive Relation of U st b1 is total
proof end;
end;

registration
let m be Nat;
coherence
for b1 being FinSequence st b1 is m + 1 -element holds
not b1 is empty
;
end;

registration
let U be non empty set ;
let u be Element of U;
cluster ((id U) . u) \+\ u -> empty for set ;
coherence
for b1 being set st b1 = ((id U) . u) \+\ u holds
b1 is empty
;
end;

registration
let U be non empty set ;
let p be U -valued non empty FinSequence;
cluster {(p . 1)} \ U -> empty for set ;
coherence
for b1 being set st b1 = {(p . 1)} \ U holds
b1 is empty
proof end;
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) ) )
proof end;

registration
let X be set ;
let U be non empty set ;
existence
ex b1 being X -defined Function st
( b1 is U -valued & b1 is total )
proof end;
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;
cluster P >*> Q -> X -defined total for X -defined Relation;
coherence
for b1 being X -defined Relation st b1 = P * Q holds
b1 is total
proof end;
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 )
proof end;

registration
let X be set ;
let R be Relation;
cluster R null X -> X \/ (rng R) -valued for Relation;
coherence
for b1 being Relation st b1 = R null X holds
b1 is X \/ (rng R) -valued
proof end;
end;

registration
let X, Y be functional set ;
cluster X \/ Y -> functional ;
coherence
X \/ Y is functional
proof end;
end;

registration
coherence
for b1 being set st b1 is FinSequence-membered holds
b1 is finite-membered
proof end;
end;

definition
let X be functional set ;
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 } is set
;
end;

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

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

proof end;

registration
existence
ex b1 being non empty FinSequence-membered set st b1 is trivial
proof end;
end;

registration
let X be functional finite finite-membered set ;
cluster SymbolsOf X -> finite for set ;
coherence
for b1 being set st b1 = SymbolsOf X holds
b1 is finite
by Lm50;
end;

registration
let X be finite FinSequence-membered set ;
cluster SymbolsOf X -> finite for set ;
coherence
for b1 being set st b1 = SymbolsOf X holds
b1 is finite
;
end;

theorem Th45: :: FOMODEL0:45
for f being Function holds SymbolsOf {f} = rng f
proof end;

registration
let P be Function;
cluster () \+\ (rng P) -> empty ;
coherence
() \+\ (rng P) is empty
by ;
end;

registration
let z be non zero Complex;
cluster |.z.| -> positive for ExtReal;
coherence
for b1 being ExtReal st b1 = |.z.| holds
b1 is positive
by COMPLEX1:47;
end;

scheme :: FOMODEL0:sch 1
Sc1{ F1() -> set , F2() -> set , F3( set ) -> set } :
{ F3(x) where x is Element of F1() : x in F1() } = { F3(x) where x is Element of F2() : x in F1() }
provided
A1: F1() c= F2()
proof end;

definition
let X be functional set ;
redefine func SymbolsOf X equals :: FOMODEL0:def 24
union { (rng x) where x is Element of X : x in X } ;
compatibility
for b1 being set holds
( b1 = SymbolsOf X iff b1 = union { (rng x) where x is Element of X : x in X } )
proof end;
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 } ;

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 ;

theorem Th47: :: FOMODEL0:47
for A, B being functional set holds SymbolsOf (A \/ B) = () \/ ()
proof end;

registration
let X be set ;
let F be Subset of (bool X);
cluster () \ X -> empty for set ;
coherence
for b1 being set st b1 = () \ X holds
b1 is empty
;
end;

theorem Th48: :: FOMODEL0:48
for X, Y being set holds X = (X \ Y) \/ (X /\ Y)
proof end;

theorem :: FOMODEL0:49
for A, B being set
for m, n being Nat st m -tuples_on A meets n -tuples_on B holds
m = n by Lm5;

theorem :: FOMODEL0:50
for D being non empty set
for A, B being set st B is D -prefix & A c= B holds
A is D -prefix ;

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

registration
let X, Y be set ;
cluster ((X \ Y) \/ (X /\ Y)) \+\ X -> empty ;
coherence
((X \ Y) \/ (X /\ Y)) \+\ X is empty
by ;
let Z be set ;
cluster ((X /\ Y) \/ (X /\ Z)) \+\ (X /\ (Y \/ Z)) -> empty ;
coherence
((X /\ Y) \/ (X /\ Z)) \+\ (X /\ (Y \/ Z)) is empty
by ;
cluster ((X \ Y) \ Z) \+\ (X \ (Y \/ Z)) -> empty ;
coherence
((X \ Y) \ Z) \+\ (X \ (Y \/ Z)) is empty
by ;
end;

registration
let X, Y be functional set ;
cluster (() \/ ()) \+\ (SymbolsOf (X \/ Y)) -> empty ;
coherence
(() \/ ()) \+\ (SymbolsOf (X \/ Y)) is empty
by ;
end;

registration
let U be non empty set ;
cluster non empty -> non empty-yielding for Element of ((U *) \ ) * ;
coherence
for b1 being Element of ((U *) \ ) * st not b1 is empty holds
not b1 is empty-yielding
proof end;
end;

registration
let e be empty set ;
cluster -> empty for Element of e * ;
coherence
for b1 being Element of e * holds b1 is empty
;
end;

theorem Th52: :: FOMODEL0:52
for x being set
for U1, U2 being non empty set
for p being FinSequence holds
( ( () . x <> {} & () . x <> {} implies () . x = () . x ) & ( p is {} * -valued implies () . p = {} ) & ( () . p = {} & p is U1 * -valued implies p is {} * -valued ) )
proof end;

registration
let U be non empty set ;
let x be set ;
cluster () . x -> U -valued ;
coherence
() . x is U -valued
proof end;
end;

definition
let x be set ;
func x null -> object equals :: FOMODEL0:def 25
x;
coherence
x is object
;
end;

:: deftheorem defines null FOMODEL0:def 25 :
for x being set holds x null = x;

registration
let x be set ;
reduce x null to x;
reducibility
x null = x
;
end;

registration
let Y be with_non-empty_elements set ;
cluster Relation-like Y -valued non empty -> non empty-yielding Y -valued for set ;
coherence
for b1 being Y -valued Relation st not b1 is empty holds
not b1 is empty-yielding
proof end;
end;

registration
let X be set ;
coherence
proof end;
end;

registration
let X be with_non-empty_elements set ;
coherence
for b1 being Subset of X holds b1 is with_non-empty_elements
proof end;
end;

registration
let U be non empty set ;
cluster U * -> infinite for set ;
coherence
for b1 being set st b1 = U * holds
not b1 is finite
proof end;
end;

registration
let U be non empty set ;
coherence
for b1 being set st b1 = U * holds
not b1 is empty-membered
;
end;

registration
let X be with_non-empty_element set ;
existence
ex b1 being non empty Subset of X st b1 is with_non-empty_elements
proof end;
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
() . 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
() . p = () . 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
() . x is X -valued
proof end;

registration
let X be set ;
let m be Nat;
cluster () \ (X *) -> empty for set ;
coherence
for b1 being set st b1 = () \ (X *) holds
b1 is empty
proof end;
end;

theorem :: FOMODEL0:55
for A, B being set holds (A /\ B) * = (A *) /\ (B *)
proof end;

theorem Th56: :: FOMODEL0:56
for X being set
for P, Q being Relation holds (P \/ Q) | X = (P | X) \/ (Q | X)
proof end;

registration
let X be set ;
cluster (bool X) \ X -> non empty for set ;
coherence
for b1 being set st b1 = (bool X) \ X holds
not b1 is empty
proof end;
end;

registration
let X be set ;
let R be Relation;
cluster R null X -> X \/ (dom R) -defined for Relation;
coherence
for b1 being Relation st b1 = R null X holds
b1 is X \/ (dom R) -defined
proof end;
end;

theorem Th57: :: FOMODEL0:57
for X being set
for f, g being Function holds (f | X) +* g = (f | (X \ (dom g))) \/ g
proof end;

registration
let X be set ;
let f be X -defined Function;
let g be X -defined total Function;
identify f +* g with g null f;
compatibility
f +* g = g null f
proof end;
identify g null f with f +* g;
compatibility
g null f = f +* g
;
end;

theorem Th58: :: FOMODEL0:58
for A, X, y being set st not y in proj2 X holds
[:A,{y}:] misses X
proof end;

definition
let X be set ;
func X -freeCountableSet -> set equals :: FOMODEL0:def 26
[:NAT,{ the Element of (bool ()) \ ()}:];
coherence
[:NAT,{ the Element of (bool ()) \ ()}:] is set
;
end;

:: deftheorem defines -freeCountableSet FOMODEL0:def 26 :
for X being set holds X -freeCountableSet = [:NAT,{ the Element of (bool ()) \ ()}:];

theorem Th59: :: FOMODEL0:59
for X being set holds
( /\ X = {} & X -freeCountableSet is infinite )
proof end;

registration
let X be set ;
coherence
for b1 being set st b1 = X -freeCountableSet holds
not b1 is finite
;
end;

registration
let X be set ;
coherence
/\ X is empty
by Th59;
end;

registration
let X be set ;
coherence
for b1 being set st b1 = X -freeCountableSet holds
b1 is countable
by CARD_4:7;
end;

registration
coherence
proof end;
end;

registration
let x be set ;
let p be FinSequence;
cluster ((<*x*> ^ p) . 1) \+\ x -> empty for set ;
coherence
for b1 being set st b1 = ((<*x*> ^ p) . 1) \+\ x holds
b1 is empty
proof end;
end;

registration
let m be Nat;
let m0 be zero number ;
let p be m -element FinSequence;
cluster p null m0 -> Seg (m + m0) -defined total for Seg (m + m0) -defined Relation;
coherence
for b1 being Seg (m + m0) -defined Relation st b1 = p null m0 holds
b1 is total
proof end;
end;

registration
let U be non empty set ;
let q1, q2 be U -valued FinSequence;
cluster (() . <*q1,q2*>) \+\ (q1 ^ q2) -> empty for set ;
coherence
for b1 being set st b1 = (() . <*q1,q2*>) \+\ (q1 ^ q2) holds
b1 is empty
proof end;
end;

registration
let f be Function;
let e be empty set ;
identify f +* e with f null e;
compatibility
f +* e = f null e
;
identify f null e with f +* e;
compatibility
f null e = f +* e
;
identify e +* f with f null e;
compatibility
e +* f = f null e
;
identify f null e with e +* f;
compatibility
f null e = e +* f
;
end;

registration
let X be infinite set ;
existence
ex b1 being Subset of X st b1 is denumerable
proof end;
end;

registration
let X be finite-membered countable set ;
cluster union X -> countable for set ;
coherence
for b1 being set st b1 = union X holds
b1 is countable
proof end;
end;

registration
let X be functional finite-membered countable set ;
cluster SymbolsOf X -> countable for set ;
coherence
for b1 being set st b1 = SymbolsOf X holds
b1 is countable
proof end;
end;

registration
let A, B be countable set ;
cluster A \/ B -> countable for set ;
coherence
for b1 being set st b1 = A \/ B holds
b1 is countable
by CARD_2:85;
end;

theorem Th60: :: FOMODEL0:60
for X, Y being set st union X c= Y holds
X c= bool Y
proof end;

theorem Th61: :: FOMODEL0:61
for A, B, Y, X being set st A is_finer_than B & X is_finer_than Y holds
A \/ X is_finer_than B \/ Y
proof end;

theorem Th62: :: FOMODEL0:62
for A, B being set st A is_finer_than B holds
A \/ B is_finer_than B
proof end;

theorem Th63: :: FOMODEL0:63
for A, B being set st B is c=directed & A is_finer_than B holds
A \/ B is c=directed
proof end;

theorem Th64: :: FOMODEL0:64
for X, Y being set holds INTERSECTION (X,Y) is_finer_than X
proof end;

theorem :: FOMODEL0:65
for Y being set st Y is c=directed holds
for X being finite Subset of () 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
for A, B, X being set st X is Subset of (Funcs (A,B)) holds
X is Subset-Family of [:A,B:] by Lm53;

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
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 ) by Lm54;

definition
let A be set ;
let R be Relation;
func R typed| A -> Subset of R equals :: FOMODEL0:def 27
R | A;
coherence
R | A is Subset of R
by RELAT_1:59;
end;

:: deftheorem defines typed| FOMODEL0:def 27 :
for A being set
for R being Relation holds R typed| A = R | A;

registration
let A be set ;
let R be Relation;
identify R typed| A with R | A;
compatibility
R typed| A = R | A
;
identify R | A with R typed| A;
compatibility
R | A = R typed| A
;
end;

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
let A, B, C be set ;
cluster (A \ ((A \/ B) \ C)) \+\ (A /\ C) -> empty ;
coherence
(A \ ((A \/ B) \ C)) \+\ (A /\ C) is empty
by ;
end;

definition
let X, P be set ;
func P |1 X -> set equals :: FOMODEL0:def 28
P /\ [:X,():];
coherence
P /\ [:X,():] is set
;
end;

:: deftheorem defines |1 FOMODEL0:def 28 :
for X, P being set holds P |1 X = P /\ [:X,():];

registration
let X be set ;
let P be Relation;
identify P |1 X with P | X;
compatibility
P |1 X = P | X
by RELAT_1:67;
identify P | X with P |1 X;
compatibility
P | X = P |1 X
;
end;

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;
func P +*1 Q -> object equals :: FOMODEL0:def 29
(P \ [:(dom Q),(rng P):]) \/ Q;
coherence
(P \ [:(dom Q),(rng P):]) \/ Q is object
;
func P +*2 Q -> object equals :: FOMODEL0:def 30
(P | ((dom P) \ (dom Q))) \/ Q;
coherence
(P | ((dom P) \ (dom Q))) \/ Q is object
;
func P +*3 Q -> object equals :: FOMODEL0:def 31
((P | (dom P)) \ (P | (dom Q))) \/ Q;
coherence
((P | (dom P)) \ (P | (dom Q))) \/ Q is object
;
end;

:: deftheorem defines +*1 FOMODEL0:def 29 :
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;

:: deftheorem defines +*3 FOMODEL0:def 31 :
for P, Q being Relation holds P +*3 Q = ((P | (dom P)) \ (P | (dom Q))) \/ Q;

registration
let P, Q be Relation;
identify P +*1 Q with P +*2 Q;
compatibility
P +*1 Q = P +*2 Q
by Lm58;
identify P +*2 Q with P +*3 Q;
compatibility
P +*2 Q = P +*3 Q
by RELAT_1:80;
end;

registration
let f, g be Function;
identify f +* g with f +*1 g;
compatibility
f +* g = f +*1 g
by Lm56;
identify f +*1 g with f +* g;
compatibility
f +*1 g = f +* g
;
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;
cluster (() . (<*u*> ^ q)) \+\ u -> empty ;
coherence
(() . (<*u*> ^ q)) \+\ u is empty
proof end;
end;

registration
existence
ex b1 being Real st
( b1 is negative & b1 is integer )
proof end;
coherence
for b1 being Integer st b1 is positive holds
b1 is natural
;
end;

registration
let X, Y be set ;
let x be Subset of X;
let y be Subset of Y;
cluster (x \ Y) \ (X \ y) -> empty for set ;
coherence
for b1 being set st b1 = (x \ Y) \ (X \ y) holds
b1 is empty
proof end;
end;

registration
let X, Y be set ;
let x be Subset of X;
let y be Subset of Y;
cluster (x \ Y) \ (X \ y) -> empty for set ;
coherence
for b1 being set st b1 = (x \ Y) \ (X \ y) holds
b1 is empty
;
end;

registration
let X, Y be set ;
let x be Subset of X;
cluster (x \ Y) \ (X \ Y) -> empty for set ;
coherence
for b1 being set st b1 = (x \ Y) \ (X \ Y) holds
b1 is empty
proof end;
end;

registration
let X, Y be set ;
let x be Subset of X;
let y be Subset of Y;
cluster ((x \/ y) \ Y) \ X -> empty for set ;
coherence
for b1 being set st b1 = ((x \/ y) \ Y) \ X holds
b1 is empty
proof end;
end;

theorem :: FOMODEL0:68
for R being Relation
for f being Function st dom f c= dom R & R c= f holds
R = f by Lm42;

registration
let T be trivial set ;
let x, y be Element of T;
cluster x \+\ y -> empty for set ;
coherence
for b1 being set st b1 = x \+\ y holds
b1 is empty
proof end;
end;

scheme :: FOMODEL0:sch 2
FraenkelTrivial{ F1() -> trivial set , F2( object ) -> object , P1[ set , set ] } :
{ F2(x) where x is Element of F1() : P1[x,F1()] } c= {F2( the Element of F1())}
proof end;

scheme :: FOMODEL0:sch 3
OnSingleTonsGen{ F1() -> set , F2( set ) -> set , P1[ set ] } :
{ [o,F2(o)] where o is Element of F1() : P1[o] } is Function
proof end;

scheme :: FOMODEL0:sch 4
FraenkelInclusion{ F1() -> set , F2( set , set ) -> set , P1[ set , set ] } :
F1() c= { F2(x,F1()) where x is Element of F1() : P1[x,F1()] }
provided
A1: for y being set st y in F1() holds
ex x being set st
( x in F1() & P1[x,F1()] & y = F2(x,F1()) )
proof end;

scheme :: FOMODEL0:sch 5
FraenkelInclusion2{ F1() -> set , P1[ set , set ] } :
F1() c= { x where x is Element of F1() : P1[x,F1()] }
provided
A1: for x being set st x in F1() holds
P1[x,F1()]
proof end;

scheme :: FOMODEL0:sch 6
FraenkelEq{ F1() -> non empty set , P1[ set ] } :
F1() = { x where x is Element of F1() : P1[x] }
provided
A1: for x being set st x in F1() holds
P1[x]
proof end;

registration
let Y be set ;
let X be Subset of Y;
cluster () \ () -> empty ;
coherence
() \ () is empty
by ;
cluster () \ () -> empty ;
coherence
() \ () is empty
by ;
end;

registration
let X, Y be set ;
cluster (proj1 [:X,Y:]) \ X -> empty ;
coherence
(proj1 [:X,Y:]) \ X is empty
by ;
cluster ((proj1 [:X,Y:]) /\ X) \+\ (proj1 [:X,Y:]) -> empty ;
coherence
((proj1 [:X,Y:]) /\ X) \+\ (proj1 [:X,Y:]) is empty
proof end;
cluster (proj2 [:X,Y:]) \ Y -> empty ;
coherence
(proj2 [:X,Y:]) \ Y is empty
by ;
cluster ((proj2 [:X,Y:]) /\ Y) \+\ (proj2 [:X,Y:]) -> empty ;
coherence
((proj2 [:X,Y:]) /\ Y) \+\ (proj2 [:X,Y:]) is empty
proof end;
cluster (() \/ ()) \+\ (proj2 (X \/ Y)) -> empty ;
coherence
(() \/ ()) \+\ (proj2 (X \/ Y)) is empty
by ;
cluster (() \/ ()) \+\ (proj1 (X \/ Y)) -> empty ;
coherence
(() \/ ()) \+\ (proj1 (X \/ Y)) is empty
by ;
let y be Subset of Y;
cluster (X \ Y) typed/\ y -> empty ;
coherence
(X \ Y) /\ y is empty
proof end;
end;

registration
let X be set ;
let U be non empty set ;
cluster (proj1 [:X,U:]) \+\ X -> empty ;
coherence
(proj1 [:X,U:]) \+\ X is empty
proof end;
cluster (proj2 [:U,X:]) \+\ X -> empty ;
coherence
(proj2 [:U,X:]) \+\ X is empty
proof end;
end;

registration
let X be set ;
let Y be non empty set ;
reduce proj1 [:X,Y:] to X;
reducibility
proj1 [:X,Y:] = X
proof end;
reduce proj2 [:Y,X:] to X;
reducibility
proj2 [:Y,X:] = X
proof end;
end;

registration
let R be Relation;
let X be set ;
cluster (R .: X) \ (rng R) -> empty ;
coherence
(R .: X) \ (rng R) is empty
by ;
end;

registration
let A, B, X, Y be set ;
cluster [:A,B:] \ [:(A \/ X),(B \/ Y):] -> empty ;
coherence
[:A,B:] \ [:(A \/ X),(B \/ Y):] is empty
proof end;
end;

registration
let X, Y, Z be set ;
cluster ((X /\ Y) /\ Z) \+\ (X /\ (Y /\ Z)) -> empty ;
coherence
((X /\ Y) /\ Z) \+\ (X /\ (Y /\ Z)) is empty
by ;
end;

registration
let X, Y be set ;
reduce (X \ Y) \/ (X /\ Y) to X;
reducibility
(X \ Y) \/ (X /\ Y) = X
by Th48;
end;

registration
let P be Relation;
let X be Subset of (dom P);
reduce dom (P | X) to X;
reducibility
dom (P | X) = X
by RELAT_1:62;
end;

registration
let X be set ;
let x, y be Subset of X;
cluster (x \/ y) \ X -> empty ;
coherence
(x \/ y) \ X is empty
;
end;

registration
let X be set ;
cluster id X -> onto ;
coherence
id X is onto
;
end;

registration
coherence
for b1 being Function st b1 is symmetric holds
b1 is involutive
proof end;
end;

registration
existence
ex b1 being Function st
( not b1 is empty & b1 is involutive )
proof end;
end;

registration
let f be non empty involutive Function;
let x be Element of dom f;
reduce f . (f . x) to x;
reducibility
f . (f . x) = x
by PARTIT_2:def 2;
end;

registration
let X, Y be set ;
cluster [:X,Y:] -> Y -valued ;
coherence
[:X,Y:] is Y -valued
proof end;
end;

registration
let x, y be set ;
cluster [:{x},{y}:] +* [:{y},{x}:] -> symmetric ;
coherence
[:{x},{y}:] +* [:{y},{x}:] is symmetric
proof end;
end;

registration
let X be set ;
let P be Relation;
let x be Subset of X;
cluster (P " x) \ (P " X) -> empty ;
coherence
(P " x) \ (P " X) is empty
by ;
end;

registration
let X be set ;
let P be Relation;
cluster (P " (X \/ (rng P))) \+\ (dom P) -> empty ;
coherence
(P " (X \/ (rng P))) \+\ (dom P) is empty
proof end;
end;

registration
let X be set ;
let R be X -defined total Relation;
cluster X \+\ (dom R) -> empty ;
coherence
X \+\ (dom R) is empty
by ;
end;

registration
let P be non empty Relation;
cluster -> pair for Element of P;
coherence
for b1 being Element of P holds b1 is pair
proof end;
end;

registration
let X be set ;
let Y be non empty set ;
let f be X -defined Y -valued total Function;
cluster {f} \ (Funcs (X,Y)) -> empty ;
coherence
{f} \ (Funcs (X,Y)) is empty
proof end;
end;

registration
let X be non empty set ;
let f be X -defined X -valued total Function;
cluster (rng f) \ (dom f) -> empty ;
coherence
(rng f) \ (dom f) is empty
proof end;
end;

registration
let X be set ;
let Y be Subset of X;
reduce (id X) .: Y to Y;
reducibility
(id X) .: Y = Y
by FUNCT_1:92;
end;

registration
let A, B be set ;
let a be Subset of A;
cluster (a \ (A \ B)) \+\ (a /\ B) -> empty ;
coherence
(a \ (A \ B)) \+\ (a /\ B) is empty
proof end;
end;

definition
let a, b be set ;
func a doubleton b -> object equals :: FOMODEL0:def 32
{a} \/ {b};
coherence
{a} \/ {b} is object
;
end;

:: deftheorem defines doubleton FOMODEL0:def 32 :
for a, b being set holds a doubleton b = {a} \/ {b};

registration
let a, b be set ;
identify {a,b} with a doubleton b;
compatibility
{a,b} = a doubleton b
by ENUMSET1:1;
identify a doubleton b with {a,b};
compatibility
a doubleton b = {a,b}
;
identify a doubleton b with b doubleton a;
compatibility ;
end;

definition
let X, Y be set ;
func X .:1 Y -> set equals :: FOMODEL0:def 33
proj2 (X |1 Y);
coherence
proj2 (X |1 Y) is set
;
end;

:: deftheorem defines .:1 FOMODEL0:def 33 :
for X, Y being set holds X .:1 Y = proj2 (X |1 Y);

registration
let P be Relation;
let X be set ;
identify P .: X with P .:1 X;
compatibility
P .: X = P .:1 X
by RELAT_1:115;
identify P .:1 X with P .: X;
compatibility
P .:1 X = P .: X
;
end;

notation
let P, Q be Relation;
synonym P >*> Q for P * Q;
end;

notation
let f, g be Function;
synonym g <*< f for g * f;
end;

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)
proof end;
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:];
cluster x 1 -> pair ;
coherence
x 1 is pair
by Lm59;
cluster x 2 -> pair ;
coherence
x 2 is pair
by Lm59;
end;

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 (() /\ ())) = X /\ (id ())
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) \ ()

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
let P be Relation;
attr P is oneone means :Def34: :: FOMODEL0:def 34
P ~ is Function-like ;
end;

:: deftheorem Def34 defines oneone FOMODEL0:def 34 :
for P being Relation holds
( P is oneone iff P ~ is Function-like );

registration
coherence
for b1 being Function st b1 is one-to-one holds
b1 is oneone
;
coherence
for b1 being Function st b1 is oneone holds
b1 is one-to-one
proof end;
end;

registration
existence
ex b1 being one-to-one Function st b1 is oneone
proof end;
end;

registration
let P be oneone Relation;
coherence by Def34;
end;

registration
existence
ex b1 being Function st
( not b1 is empty & b1 is one-to-one )
proof end;
let P be oneone Relation;
cluster -> oneone for Element of bool P;
coherence
for b1 being Subset of P holds b1 is oneone
proof end;
end;

definition
let R be set ;
func fixpoints R -> set equals :: FOMODEL0:def 35
proj1 (R /\ (id ()));
coherence
proj1 (R /\ (id ())) is set
;
func fixpoints1 R -> set equals :: FOMODEL0:def 36
proj1 (R /\ (id (() /\ ())));
coherence
proj1 (R /\ (id (() /\ ()))) is set
;
end;

:: deftheorem defines fixpoints FOMODEL0:def 35 :
for R being set holds fixpoints R = proj1 (R /\ (id ()));

:: deftheorem defines fixpoints1 FOMODEL0:def 36 :
for R being set holds fixpoints1 R = proj1 (R /\ (id (() /\ ())));

registration
let X be set ;
let R be Subset of (id X);
reduce R ~ to R;
reducibility
R ~ = R
proof end;
end;

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

registration
let R be Relation;
cluster (fixpoints1 (R ~)) \+\ () -> empty ;
coherence
(fixpoints1 (R ~)) \+\ () is empty
by ;
end;

registration
let f be one-to-one Function;
cluster (fixpoints1 (f ")) \+\ () -> empty ;
coherence
(fixpoints1 (f ")) \+\ () is empty
proof end;
end;

registration
let R be set ;
identify fixpoints R with fixpoints1 R;
compatibility by Lm66;
identify fixpoints1 R with fixpoints R;
compatibility ;
end;

Lm78: for f being Function
for x being object holds
( x in fixpoints f iff x is_a_fixpoint_of f )

proof end;

registration
let X be set ;
reduce fixpoints (id X) to X;
reducibility
fixpoints (id X) = X
;
end;

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

registration
let X be non empty set ;
coherence
proof end;
end;

registration
let X be non empty set ;
existence
ex b1 being Permutation of X st
( b1 is with_fixpoint & not b1 is empty & b1 is symmetric )
proof end;
end;

registration
existence
ex b1 being Function st
( b1 is with_fixpoint & not b1 is empty & b1 is symmetric )
proof end;
end;

registration
let f be with_fixpoint Function;
cluster dom f -> non empty ;
coherence
not dom f is empty
proof end;
end;

registration
coherence
for b1 being Function st b1 is empty holds
b1 is without_fixpoints
proof end;
end;

registration
existence
ex b1 being Function st
( b1 is without_fixpoints & b1 is empty )
proof end;
end;

registration
let f be with_fixpoint Function;
cluster fixpoints f -> non empty ;
coherence
not fixpoints f is empty
proof end;
end;

registration
let f be without_fixpoints Function;
coherence by ;
end;

definition
let X be set ;
attr X is constanT means :Def37: :: FOMODEL0:def 37
proj2 X is trivial ;
end;

:: deftheorem Def37 defines constanT FOMODEL0:def 37 :
for X being set holds
( X is constanT iff proj2 X is trivial );

registration
cluster empty -> constanT for set ;
coherence
for b1 being set st b1 is empty holds
b1 is constanT
;
end;

registration
existence
ex b1 being Function st
( b1 is empty & b1 is constanT )
proof end;
end;

registration
coherence
for b1 being Function st b1 is constant holds
b1 is constanT
;
coherence
for b1 being Function st b1 is constanT holds
b1 is constant
;
end;

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 b1 being Relation st b1 is x -valued holds
b1 is Function-like
proof end;
end;

registration
let x be trivial set ;
coherence
for b1 being Function st b1 is x -valued holds
b1 is constant
;
end;

registration
let P be Relation;
let Q be constanT Relation;
cluster P >*> Q -> constanT ;
coherence
P * Q is constanT
proof end;
end;

registration
coherence
for b1 being set st b1 is constanT holds
b1 is Function-like
proof end;
end;

registration
let P be Relation;
let c be constanT Relation;
coherence
P >*> c is Function-like
;
end;

registration
let X, Y be set ;
let x be trivial set ;
cluster [:X,Y:] >*> [:Y,x:] -> Function-like ;
coherence
[:X,Y:] >*> [:Y,x:] is Function-like
;
end;

theorem :: FOMODEL0:69
for x being set
for f being Function holds
( x in fixpoints f iff x is_a_fixpoint_of f ) by Lm78;

theorem :: FOMODEL0:70
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)} by Lm69;

theorem :: FOMODEL0:71
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)} by Lm70;

theorem :: FOMODEL0:72
for f being Function st f is involutive holds
f * f c= id (dom f) by Lm65;

theorem :: FOMODEL0:73
for X, Y, Z, y being set st y <> {} & y c= Y holds
[:X,y:] * [:Y,Z:] = [:X,Z:] by Lm62;

theorem :: FOMODEL0:74
for X being set st X <> {} holds
{ x where x is Element of X : verum } = X by Lm72;

theorem :: FOMODEL0:75
for f being Function st rng f = dom f holds
f is onto Function of (dom f),(dom f) by Lm64;

theorem :: FOMODEL0:76
for f, g being Function holds fixpoints [:f,g:] = [:(),():] by Lm79;

theorem :: FOMODEL0:77
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)) by Lm68;

theorem :: FOMODEL0:78
for X being set
for f being Function st X c= f holds
dom (f \ X) = (dom f) \ () by Lm71;