:: Preliminaries to Classical First-order Model Theory
:: by Marco B. Caminati
::
:: Received December 29, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

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

:: deftheorem DefInj1 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 ;
attrX is f -unambiguous  means :DefUnambiguous1: :: FOMODEL0:def 2
f is [:X,D:] -one-to-one ;
end;

:: deftheorem DefUnambiguous1 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 ;
attrX is D -prefix  means :DefPrefix: :: FOMODEL0:def 3
X is D -concatenation -unambiguous ;
end;

:: deftheorem DefPrefix 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 D be set ;
funcD -pr1  ->  BinOp of D equals :: FOMODEL0:def 4
 pr1 (D,D);
coherence
 pr1 (D,D) is BinOp of D ;
end;

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

Lm45:  for Y being set
for g being Function st g is Y -valued & g is FinSequence-like holds
g is FinSequence of Y
proofend;

Lm28:  for Y, A, B being set st Y c= Funcs (A,B) holds
union Y c= [:A,B:]
proofend;

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

Lm12:  for D being non empty set
for A, B being set
for f being BinOp of D st A c= B & f is B -one-to-one holds
f is A -one-to-one
proofend;

Lm18:  for A, B being set
for m, n being Nat st m -tuples_on A meets n -tuples_on B holds
m = n
proofend;

Lm21:  for i being Nat
for Y being set holds i -tuples_on Y = Funcs ((Seg i),Y)
proofend;

Lm11:  for A, B being set
for m being Nat holds (m -tuples_on A) /\ (B *) c= m -tuples_on B
proofend;

theorem Lm22: :: 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)
proofend;

Lm20:  for A, B, C being set holds (Funcs (A,B)) /\ (Funcs (A,C)) = Funcs (A,(B /\ C))
proofend;

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

theorem Lm24: :: 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)
proofend;

ThConcatenation:  for D being non empty set
for x, y being FinSequence of D holds (D -concatenation) . (x,y) = x ^ y
proofend;

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

theorem Lm2: :: FOMODEL0:5
for D being non empty set
for x being set holds
( x is non empty FinSequence of D iff x in (D *) \ {{}} )
proofend;

Lm13:  for D being non empty set
for B, A being set
for f being BinOp of D st B is f -unambiguous & A c= B holds
A is f -unambiguous
proofend;

Lm14:  for D being non empty set
for f being BinOp of D holds {} is f -unambiguous
proofend;

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

::##################### Preliminary lemmas ############################
::############################## END ##################################
::############################ Type tuning ############################
::#######################################################################
registration
let D be non empty set ;
clusterD -pr1  ->  associative for BinOp of D;
coherence
 for b1 being BinOp of D st b1 = D -pr1 holds
b1 is associative
proofend;
end;

registration
let D be set ;
cluster Relation-like [:D,D:] -defined D -valued Function-like quasi_total associative for Element of bool [:[:D,D:],D:];
existence
 ex b1 being BinOp of D st b1 is associative
proofend;
end;

definition
let X be set ;
let Y be Subset of X;
:: original:*
redefine funcY *  ->  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 ;
clusterD -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
proofend;
end;

registration
let D be non empty set ;
let m be Nat;
cluster Relation-like NAT -defined D -valued Function-like finite m -element FinSequence-like FinSubsequence-like countable finite-support for Element of D * ;
existence
 ex b1 being Element of D * st b1 is m -element
proofend;
end;

definition
let X be set ;
let f be Function;
redefine attr f is X -one-to-one  means :DefInj2: :: FOMODEL0:def 5
 for x, y being set st x in X /\ (dom f) &amp; y in X /\ (dom f) &amp; 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) &amp; y in X /\ (dom f) &amp; f . x = f . y holds
x = y ) by LmOneOne;
end;

:: deftheorem DefInj2 defines -one-to-one FOMODEL0:def_5_:_
 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) &amp; y in X /\ (dom f) &amp; f . x = f . y holds
x = y );

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

registration
let f be Function;
let x be set ;
clusterf | {x} ->  one-to-one ;
coherence
 f | {x} is one-to-one
proofend;
end;

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

registration
cluster empty  ->  empty-membered for set ;
coherence
 for b1 being set st b1 is empty holds
b1 is empty-membered ;
let e be empty set ;
cluster{e} ->  empty-membered ;
coherence
 {e} is empty-membered
proofend;
end;

registration
let U be non empty set ;
let m1 be non zero Nat;
clusterm1 -tuples_on U ->  with_non-empty_elements ;
coherence
 m1 -tuples_on U is with_non-empty_elements
proofend;
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
proofend;
end;

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

registration
let e be empty set ;
let m1 be non zero Nat;
clusterm1 -tuples_on e ->  empty ;
coherence
 m1 -tuples_on e 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 ;
clustere /\ f -> f -unambiguous ;
coherence
 e /\ f is f -unambiguous by Lm14;
end;

registration
let U be non empty set ;
let e be empty set ;
clustere /\ U -> U -prefix ;
coherence
 e /\ U is U -prefix
proofend;
end;

registration
let U be non empty set ;
clusterU -prefix for set ;
existence
 ex b1 being set st b1 is U -prefix
proofend;
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 :DefMultPlace: :: FOMODEL0:def 6
( dom it = NAT &amp; it . 0 = x . 1 &amp; ( for n being Nat holds it . (n + 1) = f . ((it . n),(x . (n + 2))) ) );
existence
 ex b1 being Function st
( dom b1 = NAT &amp; b1 . 0 = x . 1 &amp; ( for n being Nat holds b1 . (n + 1) = f . ((b1 . n),(x . (n + 2))) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = NAT &amp; b1 . 0 = x . 1 &amp; ( for n being Nat holds b1 . (n + 1) = f . ((b1 . n),(x . (n + 2))) ) &amp; dom b2 = NAT &amp; b2 . 0 = x . 1 &amp; ( for n being Nat holds b2 . (n + 1) = f . ((b2 . n),(x . (n + 2))) ) holds
b1 = b2
proofend;
end;

:: deftheorem DefMultPlace defines MultPlace FOMODEL0:def_6_:_
 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 &amp; b4 . 0 = x . 1 &amp; ( for n being Nat holds b4 . (n + 1) = f . ((b4 . n),(x . (n + 2))) ) ) );

Lm1:  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 ) &amp; ( for n being Nat st n >= m + 1 holds
(MultPlace (f,(x | n))) . m = (MultPlace (f,x)) . m ) )
proofend;

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 7
 MultPlace (f,x);
coherence
 MultPlace (f,x) is Function ;
end;

:: deftheorem  defines MultPlace FOMODEL0:def_7_:_
 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 :DefMultPlace2: :: FOMODEL0:def 8
 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)
proofend;
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) ) &amp; ( for x being Element of (D *) \ {{}} holds b2 . x = (MultPlace (f,x)) . ((len x) - 1) ) holds
b1 = b2
proofend;
end;

:: deftheorem DefMultPlace2 defines MultPlace FOMODEL0:def_8_:_
 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) );

LmMultPlace:  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 &amp; (MultPlace f) . (x ^ <*y*>) = f . (((MultPlace f) . x),y) )
proofend;

Lm3:  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 &amp; y in X /\ D &amp; d1 in D &amp; d2 in D &amp; f . (x,d1) = f . (y,d2) holds
( x = y &amp; d1 = d2 ) )
proofend;

definition
let D be non empty set ;
let f be BinOp of D;
let X be set ;
redefine attr X is f -unambiguous  means :DefUnambiguous2: :: FOMODEL0:def 9
 for x, y, d1, d2 being set st x in X /\ D &amp; y in X /\ D &amp; d1 in D &amp; d2 in D &amp; f . (x,d1) = f . (y,d2) holds
( x = y &amp; d1 = d2 );
compatibility
 ( X is f -unambiguous iff for x, y, d1, d2 being set st x in X /\ D &amp; y in X /\ D &amp; d1 in D &amp; d2 in D &amp; f . (x,d1) = f . (y,d2) holds
( x = y &amp; d1 = d2 ) )
proofend;
end;

:: deftheorem DefUnambiguous2 defines -unambiguous FOMODEL0:def_9_:_
 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 &amp; y in X /\ D &amp; d1 in D &amp; d2 in D &amp; f . (x,d1) = f . (y,d2) holds
( x = y &amp; d1 = d2 ) );

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

Lm5:  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 &amp; X is f -unambiguous holds
(MultPlace f) .: ((m + 1) -tuples_on X) is f -unambiguous
proofend;

Lm15:  for D being non empty set
for Y being set
for f being BinOp of D
for m being Nat st f is associative &amp; Y is f -unambiguous holds
(MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous
proofend;

Lm17:  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 &amp; X is f -unambiguous holds
MultPlace f is (m + 1) -tuples_on X -one-to-one
proofend;

Lm26:  for D being non empty set
for Y being set
for f being BinOp of D
for m being Nat st f is associative &amp; Y is f -unambiguous holds
MultPlace f is (m + 1) -tuples_on Y -one-to-one
proofend;

::########################### MultPlace ###############################
::############################## END ##################################
::########################### FirstChar ###############################
::#######################################################################
definition
let D be non empty set ;
funcD -firstChar  ->  Function of ((D *) \ {{}}),D equals :: FOMODEL0:def 10
 MultPlace (D -pr1);
coherence
 MultPlace (D -pr1) is Function of ((D *) \ {{}}),D ;
end;

:: deftheorem  defines -firstChar FOMODEL0:def_10_:_
 for D being non empty set holds D -firstChar = MultPlace (D -pr1);

Th2:  for D being non empty set
for w being non empty FinSequence of D holds (D -firstChar) . w = w . 1
proofend;

theorem :: FOMODEL0:6
for U being non empty set
for p being FinSequence st p is U -valued &amp; not p is empty holds
(U -firstChar) . p = p . 1
proofend;

::########################### 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 ;
funcD -multiCat  ->  Function equals :: FOMODEL0:def 11
({} .--> {}) +* (MultPlace (D -concatenation));
coherence
 ({} .--> {}) +* (MultPlace (D -concatenation)) is Function ;
end;

:: deftheorem  defines -multiCat FOMODEL0:def_11_:_
 for D being non empty set holds D -multiCat = ({} .--> {}) +* (MultPlace (D -concatenation));

definition
let D be non empty set ;
:: original:-multiCat
redefine funcD -multiCat  ->  Function of ((D *) *),(D *);
coherence
 D -multiCat is Function of ((D *) *),(D *)
proofend;
end;

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

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

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

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

Lm59:  for D being non empty set
for B, A being set st B is D -prefix &amp; A c= B holds
A is D -prefix
proofend;

registration
let D be non empty set ;
cluster  -> D -prefix for Element of bool (1 -tuples_on D);
coherence
 for b1 being Subset of (1 -tuples_on D) holds b1 is D -prefix
proofend;
end;

theorem Lm25: :: FOMODEL0:7
for D being non empty set
for A being set
for m being Nat st A is D -prefix holds
(D -multiCat) .: (m -tuples_on A) is D -prefix
proofend;

theorem :: FOMODEL0:8
for D being non empty set
for A being set
for m being Nat st A is D -prefix holds
D -multiCat is m -tuples_on A -one-to-one
proofend;

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

theorem :: FOMODEL0:10
for Y being set
for m being Nat st m is zero holds
m -tuples_on Y = {{}} by COMPUT_1:5;

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

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

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

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

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

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

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

registration
let m be Nat;
let f, g be m -element FinSequence;
cluster<:f,g:> -> m -element ;
coherence
 <:f,g:> is m -element
proofend;
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
proofend;
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
proofend;
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
proofend;
end;

registration
let D be non empty set ;
cluster Relation-like NAT -defined D -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support for set ;
existence
 ex b1 being FinSequence st b1 is D -valued
proofend;
end;

registration
let D be non empty set ;
let m be Nat;
cluster Relation-like NAT -defined D -valued Function-like finite m -element FinSequence-like FinSubsequence-like countable finite-support for set ;
existence
 ex b1 being D -valued FinSequence st b1 is m -element
proofend;
end;

registration
let X, Y be non empty set ;
let f be Function of X,Y;
let p be X -valued FinSequence;
clusterp * f ->  FinSequence-like ;
coherence
 f * p is FinSequence-like
proofend;
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;
clusterp * f -> m -element ;
coherence
 f * p is m -element
proofend;
end;

definition
let D be non empty set ;
let f be BinOp of D;
let p, q be Element of D * ;
funcf AppliedPairwiseTo (p,q) ->  FinSequence of D equals :: FOMODEL0:def 12
f * <:p,q:>;
coherence
 f * <:p,q:> is FinSequence of D
proofend;
end;

:: deftheorem  defines AppliedPairwiseTo FOMODEL0:def_12_:_
 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 * ;
clusterf AppliedPairwiseTo (p,q) -> m -element ;
coherence
 f AppliedPairwiseTo (p,q) 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 13
NAT \/ ([:{0},NAT:] \ {[0,0]});
compatibility
 for b1 being set holds
( b1 = INT iff b1 = NAT \/ ([:{0},NAT:] \ {[0,0]}) )
proofend;
end;

:: deftheorem  defines INT FOMODEL0:def_13_:_
 INT = NAT \/ ([:{0},NAT:] \ {[0,0]});

theorem Th16: :: FOMODEL0:16
for Y being set
for m being Nat
for p being FinSequence st p is Y -valued &amp; p is m -element holds
p in m -tuples_on Y
proofend;

::##############################Automatizations###############################
::############################################################################
::#To automatize things like A/\B c= A
definition
let A, B be set ;
funcA typed/\ B ->  Subset of A equals :: FOMODEL0:def 14
A /\ B;
coherence
 A /\ B is Subset of A by XBOOLE_1:17;
funcA /\typed B ->  Subset of B equals :: FOMODEL0:def 15
A /\ B;
coherence
 A /\ B is Subset of B by XBOOLE_1:17;
end;

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

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

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

definition
let B, A be set ;
funcA null B ->  set  equals :: FOMODEL0:def 16
A;
coherence
 A is set ;
end;

:: deftheorem  defines null FOMODEL0:def_16_:_
 for B, A being set holds A null B = A;

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

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

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

:: deftheorem  defines typed\ FOMODEL0:def_17_:_
 for A, B being set holds A typed\ B = A \ B;

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

definition
let A, B be set ;
funcA \typed/ B ->  Subset of (A \/ B) equals :: FOMODEL0:def 18
A;
coherence
 A is Subset of (A \/ B) by XBOOLE_1:7;
end;

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

registration
let A, B be set ;
identifyA \typed/ B with A null B;
compatibility
 A \typed/ B = A null B ;
identifyA 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;
identifyA \/ B with A null B;
compatibility
 A \/ B = A null B by XBOOLE_1:12;
identifyA null B with A \/ B;
compatibility
 A null B = A \/ B ;
end;

Lm43:  for m being Nat
for g, f being Function st f c= g holds
iter (f,m) c= iter (g,m)
proofend;

Lm31:  for R being Relation holds R [*] is_transitive_in field R
proofend;

Lm32:  for R being Relation holds field (R [*]) c= field R
proofend;

Lm37:  for R being Relation holds R [*] is_reflexive_in field R
proofend;

Lm34:  for R being Relation holds field (R [*]) = field R
proofend;

registration
let R be Relation;
clusterR [*]  ->  transitive for Relation;
coherence
 for b1 being Relation st b1 = R [*] holds
b1 is transitive
proofend;
clusterR [*]  ->  reflexive for Relation;
coherence
 for b1 being Relation st b1 = R [*] holds
b1 is reflexive
proofend;
end;

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

Lm39:  for m being Nat
for f being Function holds iter (f,(m + 1)) c= f [*]
proofend;

Lm40:  for m being Nat
for f being Function holds iter (f,m) c= f [*]
proofend;

Lm35:  for x being set
for m being Nat
for g, f being Function st rng f c= dom f &amp; x in dom f &amp; g . 0 = x &amp; ( for i being Nat st i < m holds
g . (i + 1) = f . (g . i) ) holds
g . m = (iter (f,m)) . x
proofend;

definition
func plus  ->  Function of COMPLEX,COMPLEX means :DefPlus: :: FOMODEL0:def 19
 for z being complex number holds it . z = z + 1;
existence
 ex b1 being Function of COMPLEX,COMPLEX st
for z being complex number holds b1 . z = z + 1
proofend;
uniqueness
 for b1, b2 being Function of COMPLEX,COMPLEX st ( for z being complex number holds b1 . z = z + 1 ) &amp; ( for z being complex number holds b2 . z = z + 1 ) holds
b1 = b2
proofend;
end;

:: deftheorem DefPlus defines plus FOMODEL0:def_19_:_
 for b1 being Function of COMPLEX,COMPLEX holds
( b1 = plus iff for z being complex number holds b1 . z = z + 1 );

Lm36:  for x being set
for m being Nat
for f being Function
for p being FinSequence st rng f c= dom f &amp; x in dom f &amp; p . 1 = x &amp; ( for i being Nat st i >= 1 &amp; i < m + 1 holds
p . (i + 1) = f . (p . i) ) holds
p . (m + 1) = (iter (f,m)) . x
proofend;

Lm41:  for z being set
for f being Function st z in f [*] &amp; rng f c= dom f holds
ex n being Nat st z in iter (f,n)
proofend;

Lm42:  for f being Function st rng f c= dom f holds
f [*] = union  {  (iter (f,mm)) where mm is Element of NAT : verum  }
proofend;

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

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

registration
let X be functional set ;
cluster union X ->  Relation-like ;
coherence
 union X is Relation-like
proofend;
end;

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

registration
let Y be set ;
clusterY \ 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
proofend;
end;

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

registration
let Y be set ;
let R be Y -defined Relation;
identifyR | Y with R null Y;
compatibility
 R | Y = R null Y
proofend;
identifyR 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  }
proofend;

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

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

theorem Th23: :: FOMODEL0:23
for Y being set
for P, Q being Relation holds (P \/ Q) " Y = (P " Y) \/ (Q " Y)
proofend;

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

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

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

theorem :: FOMODEL0:24
for A, B being set holds
( (chi (A,B)) " {0} = B \ A &amp; (chi (A,B)) " {1} = A /\ B )
proofend;

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

theorem :: FOMODEL0:26
for Y being set
for f being Function st f is Y -valued &amp; f is FinSequence-like holds
f is FinSequence of Y by Lm45;

registration
let Y be set ;
let X be Subset of Y;
cluster Relation-like X -valued  -> Y -valued for set ;
coherence
 for b1 being Relation st b1 is X -valued holds
b1 is Y -valued
proofend;
end;

Lm46:  for Y being set
for R being b1 -defined total Relation ex f being Function of Y,(rng R) st
( f c= R &amp; dom f = Y )
proofend;

Lm47:  for R being Relation
for f being Function st dom f c= dom R &amp; R c= f holds
R = f
proofend;

Lm48:  for Y being set
for R, P being Relation
for Q being b1 -defined Relation st Q is total &amp; R is Y -defined &amp; ((P * Q) * (Q ~)) * R is Function-like &amp; rng P c= dom R holds
((P * Q) * (Q ~)) * R = P * R
proofend;

theorem :: FOMODEL0:27
for B, A 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
proofend;

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

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

definition
let U be non empty set ;
let X be set ;
redefine attr X is U -prefix  means :: FOMODEL0:def 20
 for p1, q1, p2, q2 being U -valued FinSequence st p1 in X &amp; p2 in X &amp; p1 ^ q1 = p2 ^ q2 holds
( p1 = p2 &amp; q1 = q2 );
compatibility
 ( X is U -prefix iff for p1, q1, p2, q2 being U -valued FinSequence st p1 in X &amp; p2 in X &amp; p1 ^ q1 = p2 ^ q2 holds
( p1 = p2 &amp; q1 = q2 ) )
proofend;
end;

:: deftheorem  defines -prefix FOMODEL0:def_20_:_
 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 &amp; p2 in X &amp; p1 ^ q1 = p2 ^ q2 holds
( p1 = p2 &amp; 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 -multiCat) .: (m -tuples_on X) -> U -prefix for set ;
coherence
 for b1 being set st b1 = (U -multiCat) .: (m -tuples_on X) holds
b1 is U -prefix by Lm25;
end;

theorem Th29: :: FOMODEL0:29
for Y, X being set holds
( X \+\ Y = {} iff X = Y )
proofend;

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

theorem :: FOMODEL0:30
for D being non empty set
for x being set holds
( x in (D *) \ {{}} iff ( x is b1 -valued FinSequence &amp; not x is empty ) )
proofend;

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 &amp; ( for x being b1 -valued FinSequence st not x is empty holds
(MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d) ) )
proofend;

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

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

:: deftheorem  defines -SymbolSubstIn FOMODEL0:def_21_:_
 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
proofend;
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 22
((id X) +* (x,y)) * p;
compatibility
 for b1 being FinSequence holds
( b1 = (x,y) -SymbolSubstIn p iff b1 = ((id X) +* (x,y)) * p )
proofend;
end;

:: deftheorem  defines -SymbolSubstIn FOMODEL0:def_22_:_
 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 Lm45;
end;

Lm53:  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*> ) &amp; ( u <> u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*u*> ) )
proofend;

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

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;
funcx SubstWith u ->  Function of (U *),(U *) means :DefSubst: :: FOMODEL0:def 23
 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
proofend;
uniqueness
 for b1, b2 being Function of (U *),(U *) st ( for q being U -valued FinSequence holds b1 . q = (x,u) -SymbolSubstIn q ) &amp; ( for q being U -valued FinSequence holds b2 . q = (x,u) -SymbolSubstIn q ) holds
b1 = b2
proofend;
end;

:: deftheorem DefSubst defines SubstWith FOMODEL0:def_23_:_
 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 );

Lm54:  for U being non empty set
for u, u1, u2 being Element of U holds
( ( u = u1 implies (u1 SubstWith u2) . <*u*> = <*u2*> ) &amp; ( u <> u1 implies (u1 SubstWith u2) . <*u*> = <*u*> ) )
proofend;

registration
let U be non empty set ;
let x be set ;
let u be Element of U;
clusterx SubstWith u ->  FinSequence-yielding for Function;
coherence
 for b1 being Function st b1 = x SubstWith u holds
b1 is FinSequence-yielding
proofend;
end;

registration
let F be FinSequence-yielding Function;
let x be set ;
clusterF . x ->  FinSequence-like ;
coherence
 F . x is FinSequence-like
proofend;
end;

Lm55:  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 SubstWith u) . (q1 ^ q2) = ((x SubstWith u) . q1) ^ ((x SubstWith u) . q2)
proofend;

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

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

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

registration
let U be non empty set ;
cluster Relation-like NAT -defined U -valued Function-like non empty finite FinSequence-like FinSubsequence-like countable finite-support for set ;
existence
 not for b1 being U -valued FinSequence holds b1 is empty
proofend;
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
proofend;
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
proofend;
end;

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

Lm51:  for R being Relation holds
( R is {{}} -valued iff R is empty-yielding )
proofend;

registration
cluster Relation-like {{}} -valued  ->  empty-yielding for set ;
coherence
 for b1 being Relation st b1 is {{}} -valued holds
b1 is empty-yielding by Lm51;
cluster Relation-like empty-yielding  -> {{}} -valued for set ;
coherence
 for b1 being Relation st b1 is empty-yielding holds
b1 is {{}} -valued by Lm51;
end;

theorem Th32: :: FOMODEL0:32
for x being set
for U being non empty set holds (U -multiCat) . x = (MultPlace (U -concatenation)) . x
proofend;

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
(U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q
proofend;

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

registration
let Y be set ;
let X be Subset of Y;
let R be Y -defined total Relation;
clusterR | X -> X -defined total for X -defined Relation;
coherence
 for b1 being X -defined Relation st b1 = R | X holds
b1 is total
proofend;
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*> ) &amp; ( u <> u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*u*> ) ) by Lm53;

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*> ) &amp; ( u <> u1 implies (u1 SubstWith u2) . <*u*> = <*u*> ) ) by Lm54;

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 (x SubstWith u) . (q1 ^ q2) = ((x SubstWith u) . q1) ^ ((x SubstWith u) . q2) by Lm55;

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
(x SubstWith u) . ((U -multiCat) . p) = (U -multiCat) . ((x SubstWith u) * p) by Lm52;

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

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

registration
cluster integer non negative  ->  natural integer for set ;
coherence
 for b1 being integer number st not b1 is negative holds
b1 is natural
proofend;
end;

registration
let x, y be real number ;
cluster(max (x,y)) - x ->  ext-real non negative for ext-real number ;
coherence
 for b1 being ext-real number st b1 = (max (x,y)) - x holds
not b1 is negative
proofend;
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;
clusterX \ 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 set ;
cluster{x} \ {x,y} ->  empty for set ;
coherence
 for b1 being set st b1 = {x} \ {x,y} holds
b1 is empty
proofend;
cluster([x,y] `1) \+\ x ->  empty for set ;
coherence
 for b1 being set st b1 = ([x,y] `1) \+\ x holds
b1 is empty
proofend;
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
proofend;
end;

registration
let n be positive Nat;
let X be non empty set ;
cluster Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like countable finite-support for Element of (X *) \ {{}};
existence
 ex b1 being Element of (X *) \ {{}} st b1 is n -element
proofend;
end;

registration
let m1 be non zero Nat;
cluster Relation-like Function-like m1 + 0 -element FinSequence-like  ->  non empty for set ;
coherence
 for b1 being FinSequence st b1 is m1 + 0 -element holds
not b1 is empty
proofend;
end;

registration
let R be Relation;
let x be set ;
clusterR 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 ;
clusterf 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 ;
clusterp null x ->  FinSequence-like for Relation;
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 ;
clusterp 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 empty ;
end;

registration
let R be Relation;
let X be set ;
clusterR | X -> X -defined for Relation;
coherence
 for b1 being Relation st b1 = R | X holds
b1 is X -defined
proofend;
end;

registration
let x be set ;
let e be empty set ;
clustere 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 ;
clustere null X -> X -valued for Relation;
coherence
 for b1 being Relation st b1 = e null X holds
b1 is X -valued
proofend;
end;

registration
let Y be non empty FinSequence-membered set ;
cluster Relation-like Y -valued Function-like  ->  FinSequence-yielding for set ;
coherence
 for b1 being Function st b1 is Y -valued holds
b1 is FinSequence-yielding
proofend;
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 *
proofend;

registration
let m, n be Nat;
let p be m -element FinSequence;
clusterp 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
proofend;
end;

Lm56:  for m being Nat
for p1, p2, q1, q2 being FinSequence st p1 is m -element &amp; q1 is m -element &amp; p1 ^ p2 = q1 ^ q2 holds
( p1 = q1 &amp; p2 = q2 )
proofend;

registration
let m, n be Nat;
let p be m -element FinSequence;
let q be n -element FinSequence;
clusterp ^ q -> m + n -element for FinSequence;
coherence
 for b1 being FinSequence st b1 = p ^ q holds
b1 is m + n -element
proofend;
end;

theorem :: FOMODEL0:41
for m being Nat
for p1, p2, q1, q2 being FinSequence st p1 is m -element &amp; q1 is m -element &amp; ( p1 ^ p2 = q1 ^ q2 or p2 ^ p1 = q2 ^ q1 ) holds
( p1 = q1 &amp; p2 = q2 )
proofend;

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

registration
let m be Nat;
cluster Relation-like Function-like m + 1 -element FinSequence-like  ->  non empty for set ;
coherence
 for b1 being FinSequence st b1 is m + 1 -element holds
not b1 is empty
proofend;
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
proofend;
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
proofend;
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) ) &amp; ( x1 <> x2 implies (f +* (x1 .--> y1)) +* (x2 .--> y2) = (f +* (x2 .--> y2)) +* (x1 .--> y1) ) )
proofend;

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

registration
let X be set ;
let R be Relation;
clusterR 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
proofend;
end;

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

registration
cluster FinSequence-membered  ->  finite-membered for set ;
coherence
 for b1 being set st b1 is FinSequence-membered holds
b1 is finite-membered
proofend;
end;

definition
let X be functional set ;
func SymbolsOf X ->  set  equals :: FOMODEL0:def 24
 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_24_:_
 for X being functional set holds SymbolsOf X = union  {  (rng x) where x is Element of X \/ {{}} : x in X  }  ;

Lm58:  for X being functional set st X is finite &amp; X is finite-membered holds
SymbolsOf X is finite
proofend;

registration
cluster non empty trivial FinSequence-membered for set ;
existence
 ex b1 being set st
( b1 is trivial &amp; b1 is FinSequence-membered &amp; not b1 is empty )
proofend;
end;

registration
let X be functional finite finite-membered set ;
cluster SymbolsOf X ->  finite ;
coherence
 SymbolsOf X is finite by Lm58;
end;

registration
let X be finite FinSequence-membered set ;
cluster SymbolsOf X ->  finite ;
coherence
 SymbolsOf X is finite ;
end;

theorem :: FOMODEL0:45
for f being Function holds SymbolsOf {f} = rng f
proofend;

registration
let z be non zero complex number ;
cluster|.z.| ->  ext-real positive for ext-real number ;
coherence
 for b1 being ext-real number st b1 = abs 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
B0: F1() c= F2()
proofend;

definition
let X be functional set ;
redefine func SymbolsOf X equals :: FOMODEL0:def 25
 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  }  )
proofend;
end;

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

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

theorem :: FOMODEL0:46
for B being functional set
for A being Subset of B holds SymbolsOf A c= SymbolsOf B by Lm57, ZFMISC_1:77;

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

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

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

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

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

theorem :: 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 &amp; f . x = g . x ) )
proofend;

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
proofend;
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
( ( (U1 -multiCat) . x <> {} &amp; (U2 -multiCat) . x <> {} implies (U1 -multiCat) . x = (U2 -multiCat) . x ) &amp; ( p is {} * -valued implies (U1 -multiCat) . p = {} ) &amp; ( (U1 -multiCat) . p = {} &amp; p is U1 * -valued implies p is {} * -valued ) )
proofend;

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

definition
let x be set ;
funcx null  ->  set  equals :: FOMODEL0:def 26
x;
coherence
 x is set ;
end;

:: deftheorem  defines null FOMODEL0:def_26_:_
 for x being set holds x null = x;

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

registration
let X be set ;
clusterX \ {{}} ->  with_non-empty_elements ;
coherence
 X \ {{}} is with_non-empty_elements
proofend;
end;

registration
let X be with_non-empty_elements set ;
cluster  ->  with_non-empty_elements for Element of bool X;
coherence
 for b1 being Subset of X holds b1 is with_non-empty_elements
proofend;
end;

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

registration
let U be non empty set ;
clusterU *  ->  with_non-empty_element ;
coherence
 not U * is empty-membered ;
end;

registration
let X be with_non-empty_element set ;
cluster non empty with_non-empty_elements for Element of bool X;
existence
 ex b1 being Subset of X st
( b1 is with_non-empty_elements &amp; not b1 is empty )
proofend;
end;

Lm60:  for Y being set
for U being non empty set
for p being FinSequence st p <> {} &amp; p is Y -valued &amp; Y c= U * &amp; Y is with_non-empty_elements holds
(U -multiCat) . p <> {}
proofend;

theorem :: FOMODEL0:53
for Y being set
for U1, U2 being non empty set
for p being FinSequence st U1 c= U2 &amp; Y c= U1 * &amp; p is Y -valued &amp; p <> {} &amp; Y is with_non-empty_elements holds
(U1 -multiCat) . p = (U2 -multiCat) . p
proofend;

theorem :: FOMODEL0:54
for x, X being set
for U being non empty set st ex p being FinSequence st
( x = p &amp; p is X * -valued ) holds
(U -multiCat) . x is X -valued
proofend;

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

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

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

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

registration
let X be set ;
let R be Relation;
clusterR 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
proofend;
end;

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

registration
let X be set ;
let f be X -defined Function;
let g be X -defined total Function;
identifyf +* g with g null f;
compatibility
 f +* g = g null f
proofend;
identifyg null f with f +* g;
compatibility
 g null f = f +* g ;
end;

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

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

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

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

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

registration
let X be set ;
cluster(X -freeCountableSet) /\ X ->  empty ;
coherence
 (X -freeCountableSet) /\ X is empty by Th59;
end;

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

registration
clusterNAT \ INT ->  empty ;
coherence
 NAT \ INT is empty by NUMBERS:17;
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
proofend;
end;

registration
let m be Nat;
let m0 be zero number ;
let p be m -element FinSequence;
clusterp 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
proofend;
end;

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