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

begin

definition

let X be set ;
let f be Function;
attr f 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 ;
attr X 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 ;
attr X 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 ;
func D -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

proof end;

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

proof end;

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 )

proof end;

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

proof end;

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

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

proof end;

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

proof end;

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)

proof end;

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

proof end;

theorem Lm23: :: FOMODEL0:2

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

proof end;

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)

proof end;

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

proof end;

theorem Th4: :: FOMODEL0:4

for U being non empty set
for x, y being FinSequence st x is U -valued & y is U -valued holds
(U -concatenation) . (x,y) = x ^ y

proof end;

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 *) \ {{}} )

proof end;

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

proof end;

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

proof end;

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

proof end;

registration

let D be non empty set ;
cluster D -pr1 -> associative BinOp of D;
coherence
for b₁ being BinOp of D st b₁ = D -pr1 holds
b₁ is associative

proof end;

end;

registration

let D be set ;
cluster Relation-like [:D,D:] -defined D -valued Function-like quasi_total associative Element of bool [:[:D,D:],D:];
existence
ex b₁ being BinOp of D st b₁ 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:83;

end;

registration

let D be non empty set ;
cluster D -concatenation -> associative BinOp of (D *);
coherence
for b₁ being BinOp of (D *) st b₁ = D -concatenation holds
b₁ is associative by MONOID_0:76;

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;
cluster Relation-like NAT -defined D -valued Function-like finite m -element FinSequence-like FinSubsequence-like countable finite-support Element of D * ;
existence
ex b₁ being Element of D * st b₁ is m -element

proof end;

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) & 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 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) & 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;
cluster f -unambiguous set ;
existence
ex b₁ being set st b₁ is f -unambiguous

proof end;

end;

registration

let f be Function;
let x be set ;
cluster f | {x} -> one-to-one ;
coherence
f | {x} is one-to-one

proof end;

end;

registration

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

end;

registration

cluster empty -> empty-membered set ;
coherence
for b₁ being set st b₁ is empty holds
b₁ is empty-membered ;
let e be empty set ;
cluster {e} -> empty-membered ;
coherence
{e} is empty-membered

proof end;

end;

registration

let U be non empty set ;
let m1 be non zero Nat;
cluster m1 -tuples_on U -> with_non-empty_elements ;
coherence
m1 -tuples_on U is with_non-empty_elements

proof end;

end;

registration

let X be empty-membered set ;
cluster -> empty-membered Element of bool X;
coherence
for b₁ being Subset of X holds b₁ is empty-membered

proof end;

end;

registration

let A be set ;
let m0 be zero number ;
cluster m0 -tuples_on A -> empty-membered set ;
coherence
for b₁ being set st b₁ = m0 -tuples_on A holds
b₁ is empty-membered by COMPUT_1:8;

end;

registration

let e be empty set ;
let m1 be non zero Nat;
cluster m1 -tuples_on e -> empty ;
coherence
m1 -tuples_on e is empty by FINSEQ_3:128;

end;

registration

let D be non empty set ;
let f be BinOp of D;
let e be empty set ;
cluster e /\ f -> f -unambiguous ;
coherence
e /\ f is f -unambiguous by Lm14;

end;

registration

let U be non empty set ;
let e be empty set ;
cluster e /\ U -> U -prefix ;
coherence
e /\ U is U -prefix

proof end;

end;

registration

let U be non empty set ;
cluster U -prefix set ;
existence
ex b₁ being set st b₁ is U -prefix

proof end;

end;

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 & it . 0 = x . 1 & ( for n being Nat holds it . (n + 1) = f . ((it . n),(x . (n + 2))) ) );
existence
ex b₁ being Function st
( dom b₁ = NAT & b₁ . 0 = x . 1 & ( for n being Nat holds b₁ . (n + 1) = f . ((b₁ . n),(x . (n + 2))) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = NAT & b₁ . 0 = x . 1 & ( for n being Nat holds b₁ . (n + 1) = f . ((b₁ . n),(x . (n + 2))) ) & dom b₂ = NAT & b₂ . 0 = x . 1 & ( for n being Nat holds b₂ . (n + 1) = f . ((b₂ . n),(x . (n + 2))) ) holds
b₁ = b₂

proof end;

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 b₄ being Function holds
( b₄ = MultPlace (f,x) iff ( dom b₄ = NAT & b₄ . 0 = x . 1 & ( for n being Nat holds b₄ . (n + 1) = f . ((b₄ . 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 ) & ( 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 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;
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 b₁ being Function of ((D *) \ {{}}),D st
for x being Element of (D *) \ {{}} holds b₁ . x = (MultPlace (f,x)) . ((len x) - 1)

proof end;

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

proof end;

end;

:: deftheorem DefMultPlace2 defines MultPlace FOMODEL0:def 8 :
for D being non empty set
for f being BinOp of D
for b₃ being Function of ((D *) \ {{}}),D holds
( b₃ = MultPlace f iff for x being Element of (D *) \ {{}} holds b₃ . 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 & (MultPlace f) . (x ^ <*y*>) = f . (((MultPlace f) . x),y) )

proof end;

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 & 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 :DefUnambiguous2: :: FOMODEL0:def 9
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 ) )

proof end;

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

proof end;

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

proof end;

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 & Y is f -unambiguous holds
(MultPlace f) .: ((m + 1) -tuples_on Y) is f -unambiguous

proof end;

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

proof end;

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 & Y is f -unambiguous holds
MultPlace f is (m + 1) -tuples_on Y -one-to-one

proof end;

definition

let D be non empty set ;
func D -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

proof end;

theorem :: FOMODEL0:6

for U being non empty set
for p being FinSequence st p is U -valued & not p is empty holds
(U -firstChar) . p = p . 1

proof end;

definition

let D be non empty set ;
func D -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 func D -multiCat -> Function of ((D *) *),(D *);
coherence
D -multiCat is Function of ((D *) *),(D *)

proof end;

end;

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

proof end;

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

proof end;

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

proof end;

registration

let D be non empty set ;
let e be empty set ;
cluster (D -multiCat) . e -> empty set ;
coherence
for b₁ being set st b₁ = (D -multiCat) . e holds
b₁ is empty

proof end;

end;

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

proof end;

registration

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

proof end;

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

proof end;

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

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 empty holds
m -tuples_on Y = {{}} by COMPUT_1:8;

theorem :: FOMODEL0:11

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

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

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
( (MultPlace f) . <*d*> = d & ( 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

proof end;

theorem :: FOMODEL0:15

for D being non empty set
for d1, d2 being Element of D * holds (D -multiCat) . <*d1,d2*> = d1 ^ d2

proof end;

registration

let f, g be FinSequence;
cluster <:f,g:> -> FinSequence-like ;
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 Function;
coherence
for b₁ being Function st b₁ = <:f,g:> holds
b₁ is X /\ Y -defined

proof end;

end;

registration

let X be set ;
let f, g be X -defined Function;
cluster <:f,g:> -> X -defined Function;
coherence
for b₁ being Function st b₁ = <:f,g:> holds
b₁ 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 X /\ Y -defined Function;
coherence
for b₁ being X /\ Y -defined Function st b₁ = <:f,g:> holds
b₁ is total

proof end;

end;

registration

let X be set ;
let f, g be X -defined total Function;
cluster <:f,g:> -> X -defined total X -defined Function;
coherence
for b₁ being X -defined Function st b₁ = <:f,g:> holds
b₁ 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 Function;
coherence
for b₁ being Function st b₁ = <:f,g:> holds
b₁ is [:X,Y:] -valued

proof end;

end;

registration

let D be non empty set ;
cluster Relation-like D -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support set ;
existence
ex b₁ being FinSequence st b₁ is D -valued

proof end;

end;

registration

let D be non empty set ;
let m be Nat;
cluster Relation-like D -valued Function-like finite m -element FinSequence-like FinSubsequence-like countable finite-support set ;
existence
ex b₁ being D -valued FinSequence st b₁ 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;
cluster p * f -> FinSequence-like ;
coherence
f * p is FinSequence-like

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 ;
coherence
f * p 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 12
f * <:p,q:>;
coherence
f * <:p,q:> is FinSequence of D

proof end;

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 * ;
cluster f 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 b₁ being set holds
( b₁ = INT iff b₁ = NAT \/ ([:{0},NAT:] \ {[0,0]}) )

proof end;

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 & p is m -element holds
p in m -tuples_on Y

proof end;

definition

let A, B be set ;
func A typed/\ B -> Subset of A equals :: FOMODEL0:def 14
A /\ B;
coherence
A /\ B is Subset of A by XBOOLE_1:17;
func A /\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 ;
identify A /\ B with A typed/\ B;
compatibility
A /\ B = A typed/\ B ;
identify A typed/\ B with A /\ B;
compatibility
A typed/\ B = A /\ B ;
identify A /\ B with A /\typed B;
compatibility
A /\ B = A /\typed B ;
identify A /\typed B with A /\ B;
compatibility
A /\typed B = A /\ B ;

end;

definition

let B, A be set ;
func A 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;
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) /\ (A /\ C) -> empty set ;
coherence
for b₁ being set st b₁ = (B \ A) /\ (A /\ C) holds
b₁ is empty

proof end;

end;

definition

let A, B be set ;
func A 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 ;
identify A \ B with A typed\ B;
compatibility
A \ B = A typed\ B ;
identify A typed\ B with A \ B;
compatibility
A typed\ B = A \ B ;

end;

definition

let A, B be set ;
func A \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 ;
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;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

registration

let R be Relation;
cluster R [*] -> transitive Relation;
coherence
for b₁ being Relation st b₁ = R [*] holds
b₁ is transitive

proof end;

cluster R [*] -> reflexive Relation;
coherence
for b₁ being Relation st b₁ = R [*] holds
b₁ is reflexive

proof end;

end;

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

proof end;

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

proof end;

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

proof end;

Lm35: for x being set
for m being Nat
for g, 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 :DefPlus: :: FOMODEL0:def 19
for z being complex number holds it . z = z + 1;
existence
ex b₁ being Function of COMPLEX,COMPLEX st
for z being complex number holds b₁ . z = z + 1

proof end;

uniqueness
for b₁, b₂ being Function of COMPLEX,COMPLEX st ( for z being complex number holds b₁ . z = z + 1 ) & ( for z being complex number holds b₂ . z = z + 1 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefPlus defines plus FOMODEL0:def 19 :
for b₁ being Function of COMPLEX,COMPLEX holds
( b₁ = plus iff for z being complex number holds b₁ . 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 & 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;

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

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

proof end;

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 ;
let R be Y -valued Relation;
identify Y | R with R null Y;
compatibility
Y | R = R null Y

proof end;

end;

registration

let Y be set ;
cluster Y \ Y -> empty set ;
coherence
for b₁ being set st b₁ = Y \ Y holds
b₁ 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 set ;
coherence
for b₁ being set st b₁ = {((id D) . d)} \ {d} holds
b₁ is empty

proof end;

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

proof end;

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 b₁ -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 = (D -concatenation) .: [:(m -tuples_on D),(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;

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

proof end;

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

proof end;

Lm29: 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)) " {0} = 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 Lm45;

registration

let Y be set ;
let X be Subset of Y;
cluster Relation-like X -valued -> Y -valued set ;
coherence
for b₁ being Relation st b₁ is X -valued holds
b₁ is Y -valued

proof end;

end;

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

proof end;

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

proof end;

Lm48: for Y being set
for R, P being Relation
for Q being b₁ -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 Element of bool [:A,U:];
coherence
for b₁ being Relation of A,U st b₁ is quasi_total holds
b₁ is total

proof end;

end;

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

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 FinSequence;
coherence
for b₁ being FinSequence st b₁ = p ^ q holds
b₁ is U -valued

proof end;

end;

definition

let X be set ;
:: original: FinSequence
redefine mode FinSequence of X -> Element of X * ;
coherence
for b₁ being FinSequence of X holds b₁ 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 20
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 20 :
for U being non empty set
for X being set holds
( X is U -prefix iff for p1, q1, p2, q2 being b₁ -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 Element of X * ;
coherence
for b₁ being Element of X * holds b₁ 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 set ;
coherence
for b₁ being set st b₁ = (U -multiCat) .: (m -tuples_on X) holds
b₁ is U -prefix by Lm25;

end;

theorem Th29: :: FOMODEL0:29

for Y, X being set holds
( X \+\ Y = {} iff X = Y )

proof end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

theorem :: FOMODEL0:30

for D being non empty set
for x being set holds
( x in (D *) \ {{}} iff ( x is b₁ -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
( (MultPlace f) . <*d*> = d & ( for x being b₁ -valued FinSequence st not x is empty holds
(MultPlace f) . (x ^ <*d*>) = f . (((MultPlace 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 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 FinSequence;
coherence
for b₁ being FinSequence st b₁ = (x,y) -SymbolSubstIn p holds
b₁ is m -element

proof end;

end;

registration

let X be set ;
cluster Relation-like X -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support set ;
existence
ex b₁ being FinSequence st b₁ is X -valued

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 FinSequence;
coherence
for b₁ being FinSequence st b₁ = (x,u) -SymbolSubstIn p holds
b₁ 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 b₁ being FinSequence holds
( b₁ = (x,y) -SymbolSubstIn p iff b₁ = ((id X) +* (x,y)) * p )

proof end;

end;

:: deftheorem defines -SymbolSubstIn FOMODEL0:def 22 :
for X, x, y being set
for p being b₁ -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*> ) & ( u <> u1 implies (u1,x2) -SymbolSubstIn <*u*> = <*u*> ) )

proof end;

Lm50: for x being set
for U being non empty set
for u being Element of U
for q1, q2 being b₂ -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 H₁( Element of U * ) -> FinSequence of U = (x,u) -SymbolSubstIn $1;
func x 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 b₁ being Function of (U *),(U *) st
for q being U -valued FinSequence holds b₁ . q = (x,u) -SymbolSubstIn q

proof end;

uniqueness
for b₁, b₂ being Function of (U *),(U *) st ( for q being U -valued FinSequence holds b₁ . q = (x,u) -SymbolSubstIn q ) & ( for q being U -valued FinSequence holds b₂ . q = (x,u) -SymbolSubstIn q ) holds
b₁ = b₂

proof end;

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 b₄ being Function of (U *),(U *) holds
( b₄ = x SubstWith u iff for q being b₁ -valued FinSequence holds b₄ . 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*> ) & ( 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;
cluster x SubstWith u -> FinSequence-yielding Function;
coherence
for b₁ being Function st b₁ = x SubstWith u holds
b₁ is FinSequence-yielding

proof end;

end;

registration

let F be FinSequence-yielding Function;
let x be set ;
cluster F . x -> FinSequence-like ;
coherence
F . x is FinSequence-like

proof end;

end;

Lm55: for x being set
for U being non empty set
for u being Element of U
for q1, q2 being b₂ -valued FinSequence holds (x SubstWith u) . (q1 ^ q2) = ((x SubstWith u) . q1) ^ ((x SubstWith u) . 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 (x SubstWith u) . p -> m -element FinSequence;
coherence
for b₁ being FinSequence st b₁ = (x SubstWith u) . p holds
b₁ 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 (x SubstWith u) . e -> empty set ;
coherence
for b₁ being set st b₁ = (x SubstWith u) . e holds
b₁ is empty

proof end;

end;

registration

let U be non empty set ;
cluster U -multiCat -> FinSequence-yielding Function;
coherence
for b₁ being Function st b₁ = U -multiCat holds
b₁ is FinSequence-yielding

proof end;

end;

registration

let U be non empty set ;
cluster Relation-like U -valued Function-like non empty finite FinSequence-like FinSubsequence-like countable finite-support set ;
existence
not for b₁ being U -valued FinSequence holds b₁ 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 set ;
coherence
for b₁ being set st b₁ = {(p . m1)} \ U holds
b₁ 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 set ;
coherence
for b₁ being set st b₁ = {(p . (m + 1))} \ U holds
b₁ is empty ;

end;

registration

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

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

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

proof end;

registration

cluster Relation-like {{}} -valued -> empty-yielding set ;
coherence
for b₁ being Relation st b₁ is {{}} -valued holds
b₁ is empty-yielding by Lm51;
cluster Relation-like empty-yielding -> {{}} -valued set ;
coherence
for b₁ being Relation st b₁ is empty-yielding holds
b₁ 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

proof end;

theorem Th33: :: FOMODEL0:33

for U being non empty set
for p being FinSequence
for q being b₁ -valued FinSequence st p is U * -valued holds
(U -multiCat) . (p ^ <*q*>) = ((U -multiCat) . p) ^ q

proof end;

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)

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 X -defined Relation;
coherence
for b₁ being X -defined Relation st b₁ = R | X holds
b₁ 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 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*> ) & ( 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 b₂ -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 }

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 set ;
coherence
for b₁ being set st b₁ = ((f | U) . u) \+\ (f . u) holds
b₁ 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 set ;
coherence
for b₁ being set st b₁ = ((f * g) . u) \+\ (f . (g . u)) holds
b₁ is empty

proof end;

end;

registration

cluster integer non negative -> natural integer set ;
coherence
for b₁ being integer number st not b₁ is negative holds
b₁ is natural

proof end;

end;

registration

let x, y be real number ;
cluster (max (x,y)) - x -> ext-real non negative ext-real number ;
coherence
for b₁ being ext-real number st b₁ = (max (x,y)) - x holds
not b₁ 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 set ;
coherence
for b₁ being set st b₁ = X \ Y holds
b₁ is empty by XBOOLE_1:37;

end;

registration

let x, y be set ;
cluster {x} \ {x,y} -> empty set ;
coherence
for b₁ being set st b₁ = {x} \ {x,y} holds
b₁ is empty

proof end;

cluster ([x,y] `1) \+\ x -> empty set ;
coherence
for b<sub>1</sub> being set st b<sub>1</sub> = ([x,y] `1) \+\ x holds
b₁ is empty

proof end;

end;

registration

let x, y be set ;
cluster ([x,y] `2) \+\ y -> empty set ;
coherence
for b<sub>1</sub> being set st b<sub>1</sub> = ([x,y] `2) \+\ y holds
b₁ is empty

proof end;

end;

registration

let n be positive Nat;
let X be non empty set ;
cluster Relation-like Function-like finite n -element FinSequence-like FinSubsequence-like countable finite-support Element of (X *) \ {{}};
existence
ex b₁ being Element of (X *) \ {{}} st b₁ is n -element

proof end;

end;

registration

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

proof end;

end;

registration

let R be Relation;
let x be set ;
cluster R null x -> Relation-like set ;
coherence
for b₁ being set st b₁ = R null x holds
b₁ is Relation-like ;

end;

registration

let f be Function-like set ;
let x be set ;
cluster f null x -> Function-like set ;
coherence
for b₁ being set st b₁ = f null x holds
b₁ is Function-like ;

end;

registration

let p be FinSequence-like Relation;
let x be set ;
cluster p null x -> FinSequence-like Relation;
coherence
for b₁ being Relation st b₁ = p null x holds
b₁ is FinSequence-like ;

end;

registration

let p be FinSequence;
let x be set ;
cluster p null x -> len p -element FinSequence;
coherence
for b₁ being FinSequence st b₁ = p null x holds
b₁ is len p -element by CARD_1:def 13;

end;

registration

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

end;

registration

let R be Relation;
let X be set ;
cluster R | X -> X -defined Relation;
coherence
for b₁ being Relation st b₁ = R | X holds
b₁ is X -defined

proof end;

end;

registration

let x be set ;
let e be empty set ;
cluster e null x -> empty set ;
coherence
for b₁ being set st b₁ = e null x holds
b₁ is empty ;

end;

registration

let X be set ;
let e be empty set ;
cluster e null X -> X -valued Relation;
coherence
for b₁ being Relation st b₁ = e null X holds
b₁ is X -valued

proof end;

end;

registration

let Y be non empty FinSequence-membered set ;
cluster Relation-like Y -valued Function-like -> FinSequence-yielding set ;
coherence
for b₁ being Function st b₁ is Y -valued holds
b₁ is FinSequence-yielding

proof end;

end;

registration

let X, Y be set ;
cluster -> FinSequence-yielding Element of Funcs (X,(Y *));
coherence
for b₁ being Element of Funcs (X,(Y *)) holds b₁ 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 Relation;
coherence
for b₁ being Relation st b₁ = p null n holds
b₁ is Seg (m + n) -defined

proof end;

end;

Lm56: 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 FinSequence;
coherence
for b₁ being FinSequence st b₁ = p ^ q holds
b₁ is m + n -element

proof end;

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 (U -multiCat) . x is U1 -valued & x in (U *) * holds
x is FinSequence of U1 *

proof end;

registration

let U be non empty set ;
cluster Relation-like U -defined U -valued total reflexive Element of bool [:U,U:];
existence
ex b₁ being reflexive Relation of U st b₁ is total

proof end;

end;

registration

let m be Nat;
cluster Relation-like Function-like m + 1 -element FinSequence-like -> non empty set ;
coherence
for b₁ being FinSequence st b₁ is m + 1 -element holds
not b₁ is empty

proof end;

end;

registration

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

proof end;

end;

registration

let U be non empty set ;
let p be U -valued non empty FinSequence;
cluster {(p . 1)} \ U -> empty set ;
coherence
for b₁ being set st b₁ = {(p . 1)} \ U holds
b₁ 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 ;
cluster Relation-like X -defined U -valued Function-like total set ;
existence
ex b₁ being X -defined Function st
( b₁ is U -valued & b₁ 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 X -defined Relation;
coherence
for b₁ being X -defined Relation st b₁ = P * Q holds
b₁ 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 Relation;
coherence
for b₁ being Relation st b₁ = R null X holds
b₁ 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

cluster FinSequence-membered -> finite-membered set ;
coherence
for b₁ being set st b₁ is FinSequence-membered holds
b₁ is finite-membered

proof end;

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 & X is finite-membered holds
SymbolsOf X is finite

proof end;

registration

cluster non empty trivial FinSequence-membered set ;
existence
ex b₁ being set st
( b₁ is trivial & b₁ is FinSequence-membered & not b₁ is empty )

proof end;

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

proof end;

registration

let z be non zero complex number ;
cluster |.z.| -> ext-real positive ext-real number ;
coherence
for b₁ being ext-real number st b₁ = abs z holds
b₁ is positive by COMPLEX1:133;

end;

scheme :: FOMODEL0:sch 1
Sc1{ F₁() -> set , F₂() -> set , F₃( set ) -> set } :

{ F₃(x) where x is Element of F₁() : x in F₁() } = { F₃(x) where x is Element of F₂() : x in F₁() }

provided

B0: F₁() c= F₂()

proof end;

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 b₁ being set holds
( b₁ = SymbolsOf X iff b₁ = union { (rng x) where x is Element of X : x in X } )

proof end;

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 }

proof end;

theorem :: FOMODEL0:46

for B being functional set
for A being Subset of B holds SymbolsOf A c= SymbolsOf B by Lm57, ZFMISC_1:95;

theorem :: FOMODEL0:47

for A, B being functional set holds SymbolsOf (A \/ B) = (SymbolsOf A) \/ (SymbolsOf B)

proof end;

registration

let X be set ;
let F be Subset of (bool X);
cluster (union F) \ X -> empty set ;
coherence
for b₁ being set st b₁ = (union F) \ X holds
b₁ 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 Lm18;

theorem :: FOMODEL0:50

for D being non empty set
for B, A being set st B is D -prefix & 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 & f . x = g . x ) )

proof end;

registration

let U be non empty set ;
cluster non empty -> non empty-yielding Element of ((U *) \ {{}}) * ;
coherence
for b₁ being Element of ((U *) \ {{}}) * st not b₁ is empty holds
not b₁ is empty-yielding

proof end;

end;

registration

let e be empty set ;
cluster -> empty Element of e * ;
coherence
for b₁ being Element of e * holds b₁ 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 <> {} & (U2 -multiCat) . x <> {} implies (U1 -multiCat) . x = (U2 -multiCat) . x ) & ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {} * -valued ) )

proof end;

registration

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

proof end;

end;

definition

let x be set ;
func x 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 set ;
coherence
for b₁ being Y -valued Relation st not b₁ is empty holds
not b₁ is empty-yielding

proof end;

end;

registration

let X be set ;
cluster X \ {{}} -> with_non-empty_elements ;
coherence
X \ {{}} is with_non-empty_elements

proof end;

end;

registration

let X be with_non-empty_elements set ;
cluster -> with_non-empty_elements Element of bool X;
coherence
for b₁ being Subset of X holds b₁ is with_non-empty_elements

proof end;

end;

registration

let U be non empty set ;
cluster U * -> infinite set ;
coherence
for b₁ being set st b₁ = U * holds
not b₁ is finite

proof end;

end;

registration

let U be non empty set ;
cluster U * -> 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 Element of bool X;
existence
ex b₁ being Subset of X st
( b₁ is with_non-empty_elements & not b₁ is empty )

proof end;

end;

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

proof end;

theorem :: FOMODEL0:53

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

proof end;

theorem :: FOMODEL0:54

for x, X being set
for U being non empty set st ex p being FinSequence st
( x = p & p is X * -valued ) holds
(U -multiCat) . x is X -valued

proof end;

registration

let X be set ;
let m be Nat;
cluster (m -tuples_on X) \ (X *) -> empty set ;
coherence
for b₁ being set st b₁ = (m -tuples_on X) \ (X *) holds
b₁ is empty

proof end;

end;

theorem :: FOMODEL0:55

for A, B being set holds (A /\ B) * = (A *) /\ (B *)

proof end;

theorem :: 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 set ;
coherence
for b₁ being set st b₁ = (bool X) \ X holds
not b₁ is empty

proof end;

end;

registration

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

proof end;

end;

theorem :: 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 y, X, A 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 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 = {} & not X -freeCountableSet is finite )

proof end;

registration

let X be set ;
cluster X -freeCountableSet -> infinite set ;
coherence
for b₁ being set st b₁ = X -freeCountableSet holds
not b₁ 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 ;
cluster X -freeCountableSet -> countable set ;
coherence
for b₁ being set st b₁ = X -freeCountableSet holds
b₁ is countable by CARD_4:55;

end;

registration

cluster NAT \ INT -> empty ;
coherence
NAT \ INT is empty

proof end;

end;

registration

let x be set ;
let p be FinSequence;
cluster ((<*x*> ^ p) . 1) \+\ x -> empty set ;
coherence
for b₁ being set st b₁ = ((<*x*> ^ p) . 1) \+\ x holds
b₁ 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 Seg (m + m0) -defined FinSequence;
coherence
for b₁ being Seg (m + m0) -defined FinSequence st b₁ = p null m0 holds
b₁ is total

proof end;

end;

registration

let U be non empty set ;
let q1, q2 be U -valued FinSequence;
cluster ((U -multiCat) . <*q1,q2*>) \+\ (q1 ^ q2) -> empty set ;
coherence
for b₁ being set st b₁ = ((U -multiCat) . <*q1,q2*>) \+\ (q1 ^ q2) holds
b₁ 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 by FUNCT_4:22;
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 by FUNCT_4:21;
identify f null e with e +* f;
compatibility
f null e = e +* f ;

end;