:: Preliminaries to Classical First-order Model Theory
:: by Marco B. Caminati
::
:: Received December 29, 2010
:: Copyright (c) 2010-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies TARSKI, ABIAN, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, NAT_1,
INT_1, RELAT_1, FINSEQ_1, FUNCT_1, ARYTM_3, XCMPLX_0, CARD_1, MONOID_0,
ORDINAL1, ARYTM_1, FUNCT_2, XXREAL_0, ALGSTR_0, ORDINAL4, BINOP_1,
FUNCT_7, FUNCT_4, FUNCOP_1, FINSEQ_2, MCART_1, PARTFUN1, FUNCT_3,
MARGREL1, RELAT_2, PRE_POLY, XBOOLEAN, MATROID0, FINSET_1, COMPLEX1,
SETFAM_1, CARD_3, COHSP_1, OPOSET_1, FACIRC_1, FOMODEL0, REAL_1;
notations COHSP_1, ABIAN, TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1,
NUMBERS, INT_1, XCMPLX_0, FUNCOP_1, RELAT_1, FUNCT_1, PARTFUN1, RELSET_1,
FUNCT_2, FUNCT_4, PRE_POLY, FINSEQ_1, MONOID_0, STRUCT_0, XXREAL_0,
XREAL_0, BINOP_1, FUNCT_7, FINSEQ_2, MCART_1, FINSEQOP, ALGSTR_0,
FUNCT_3, MARGREL1, RELAT_2, SETFAM_1, FINSET_1, COMPLEX1, CARD_1, CARD_3,
XTUPLE_0, XFAMILY, DOMAIN_1, PARTIT_2;
constructors MONOID_0, ABIAN, BINOP_1, FUNCT_4, RELSET_1, FINSEQOP, DOMAIN_1,
SETWISEO, REAL_1, LEXBFS, MATROID0, COMPLEX1, COHSP_1, PARTIT_2, XFAMILY;
registrations CARD_1, CARD_3, COHSP_1, FINSEQ_1, FINSEQ_2, FINSEQ_6, FINSET_1,
FUNCOP_1, FUNCT_1, FUNCT_2, FUNCT_4, FUNCT_7, FUNCTOR0, GRFUNC_1,
HEYTING3, INT_1, MONOID_0, NAT_1, NUMBERS, ORDINAL1, PARTFUN1, PRALG_1,
PRE_POLY, RELAT_1, RELSET_1, SETFAM_1, SUBSET_1, XBOOLE_0, XCMPLX_0,
XREAL_0, XTUPLE_0, XXREAL_0, ZFMISC_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
equalities TARSKI, FINSEQ_1, BINOP_1, RELAT_1, MARGREL1, FUNCT_4, FUNCOP_1,
XBOOLE_0, XBOOLEAN;
expansions TARSKI, FINSEQ_1, BINOP_1, RELAT_1, XBOOLE_0;
theorems TARSKI, ABIAN, XBOOLE_0, INT_1, ZFMISC_1, NUMBERS, FUNCT_1, FINSEQ_1,
RELAT_1, XBOOLE_1, FUNCT_2, FUNCT_4, FUNCOP_1, MONOID_0, XXREAL_0, NAT_1,
ORDINAL1, MCART_1, FINSEQ_5, FINSEQ_2, FINSEQ_3, PARTFUN1, XREAL_1,
RELSET_1, ALGSTR_0, FUNCT_5, FUNCT_7, ARYTM_3, RELAT_2, LANG1, XCMPLX_0,
FRAENKEL, SYSREL, PRE_POLY, FUNCT_3, GRFUNC_1, FINSEQOP, XBOOLEAN,
FINSEQ_6, COMPLEX1, SETFAM_1, CARD_4, CARD_1, CARD_3, WAYBEL12, COHSP_1,
CARD_2, RFUNCT_1, XTUPLE_0, FINSET_1, SUBSET_1, PARTIT_2, ENUMSET1;
schemes NAT_1, FUNCT_1, FUNCT_2, CLASSES1, FRAENKEL, ALTCAT_2, TREES_2;
begin
::#Preliminary/more general results in this article
reserve A,B,C,Y,x,y,z for set, U, D for non empty set,
X for non empty Subset of D, d,d1,d2 for Element of D;
reserve P,Q,R for Relation, g for Function, p,q for FinSequence;
reserve f for BinOp of D, i,m,n for Nat;
::################### Preliminary Definitions #########################
::#######################################################################
definition
let X be set;
let f be Function;
attr f is X-one-to-one means
f|X is one-to-one;
end;
definition
let D,f;
let X be set;
attr X is f-unambiguous means
f is [:X,D:]-one-to-one;
end;
definition ::#def3 1
let D;
let X be set;
attr X is D-prefix means X is (D-concatenation)-unambiguous;
end;
definition
let f be Function-yielding Function, g be Function;
func ^^^ f,g __ -> Function means dom it = dom f /\ dom g & for x being set st
x in dom it holds it.x=(f.x).(g.x);
existence
proof
set A=dom f /\ dom g;
deffunc F(object)=(f.$1).(g.$1);
consider h being Function such that A1:
dom h=A & for x being object st x in A holds h.x=F(x) from FUNCT_1:sch 3;
take h; thus thesis by A1;
end;
uniqueness
proof
set A=dom f /\ dom g;
let IT1,IT2 be Function; assume
A2:dom IT1=A & for x being set st x in dom IT1 holds IT1.x=(f.x).(g.x);assume
A3: dom IT2=A & for x being set st x in dom IT2 holds IT2.x=(f.x).(g.x);
now
let x be object; assume A4: x in dom IT1;
thus IT1.x=(f.x).(g.x) by A2,A4 .= IT2.x by A2,A3,A4;
end;
hence thesis by FUNCT_1:2, A2, A3;
end;
end;
definition
let D be set;
func D-pr1 -> BinOp of D equals pr1(D,D);
::# where pr1(,) is defined in FUNCT_3
coherence;
end;
::################### Preliminary Definitions #########################
::############################## END ##################################
::##################### Preliminary lemmas #############################
Lm1: g is Y-valued & g is FinSequence-like implies g is FinSequence of Y
by FINSEQ_1:def 4;
Lm2: Y c= Funcs(A,B) implies union Y c= [:A,B:]
proof
set AB=[:A,B:], F=Funcs(A,B), X=Y; assume X c= F; then X c= F &
F c= bool AB by FRAENKEL:2; then reconsider
XX=X as Subset of bool AB by XBOOLE_1:1; union XX is Subset of AB;
hence thesis;
end;
Lm3: for X being set, 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
let X be set, f be Function;
set g=f|X;
thus f is X-one-to-one implies
(for x,y being set st x in dom f/\X & y in dom f/\X & f.x=f.y holds x=y)
proof
assume f is X-one-to-one; then
A1: g is one-to-one; let x,y be set;
assume x in dom f/\X; then
A2: x in dom g by RELAT_1:61;
assume y in dom f/\X; then
A3: y in dom g by RELAT_1:61;
assume f.x=f.y; then g.x=f.x & g.y=f.y & f.x=f.y by A2, A3, FUNCT_1:47;
hence x=y by A1, FUNCT_1:def 4,A2,A3;
end;
assume
A4: for x,y being set st
x in dom f/\X & y in dom f/\X & f.x=f.y holds x=y;
now
let x,y be object;
assume A5: x in dom g & y in dom g & g.x=g.y;
then g.x=f.x & g.y=f.y & g.x=g.y by FUNCT_1:47;
then x in dom f/\X & y in dom f /\ X & f.x=f.y by A5, RELAT_1:61;
hence x=y by A4;
end;
then g is one-to-one by FUNCT_1:def 4; hence thesis;
end;
Lm4: A c= B & f is B-one-to-one implies f is A-one-to-one
proof
assume A c= B & f is B-one-to-one; then
f|B is one-to-one & f|A = (f|B)|A by FUNCT_1:51;
hence thesis by FUNCT_1:52;
end;
Lm5: m-tuples_on A meets n-tuples_on B implies m=n
proof
assume m-tuples_on A meets (n-tuples_on B);
then m-tuples_on A /\ (n-tuples_on B) is non empty; then
consider p being object such that
A1: p in m-tuples_on A/\ (n-tuples_on B);
A2: p in m-tuples_on A & p in n-tuples_on B by XBOOLE_0:def 4, A1;
reconsider pA=p as m-element FinSequence by FINSEQ_2:141,A2;
reconsider pB=p as n-element FinSequence by FINSEQ_2:141,A2;
m = len pA by CARD_1:def 7 .= len pB .= n by CARD_1:def 7; hence thesis;
end;
Lm6: for D being set holds 0-tuples_on D={{}} proof let D be set;thus
0-tuples_on D = {<*>D} by FINSEQ_2:94 .= {{}}; end;
Lm7: for i being Nat, Y being set holds i-tuples_on Y = Funcs(Seg i,Y)
proof
let i be Nat,Y be set;
per cases;
suppose A1: Y is empty;
per cases;
suppose i is zero; then i is zero & Seg i={}; then
Funcs(Seg i,Y)={{}} & i-tuples_on Y={{}} by FUNCT_5:57,Lm6;hence thesis;end;
suppose i is non zero; then
Funcs(Seg i,Y)={} & i-tuples_on Y={} by FINSEQ_3:119,A1;hence thesis;end;
end;
suppose Y is non empty; then reconsider YY=Y as non empty set;
thus thesis by FINSEQ_2:93;
end;
end;
Lm8: m-tuples_on A /\ (B*) c= m-tuples_on B
proof
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
set L=m-tuples_on A /\ (B*), R=m-tuples_on B;
let x be object; assume x in L; then
A1: x in m-tuples_on A & x in B* by XBOOLE_0:def 4; then A2: x is m-element
FinSequence & x is FinSequence of B by FINSEQ_2:141, FINSEQ_1:def 11;
reconsider xx=x as FinSequence of B by A1, FINSEQ_1:def 11;
len xx=m by A2, CARD_1:def 7;
then xx=xx & dom xx=Seg m & rng xx c= B by FINSEQ_1:def 3; then
xx in Funcs (Seg m, B) by FUNCT_2:def 2; hence x in R by Lm7;
end;
theorem Th1: m-tuples_on A /\ (B*) = m-tuples_on A /\ (m-tuples_on B)
proof
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
set L=m-tuples_on A /\ (B*), R=m-tuples_on A /\ m-tuples_on B;
m-tuples_on A /\ L c= R by XBOOLE_1:26, Lm8; then
A1: (m-tuples_on A /\ m-tuples_on A) /\ (B*) c= R by XBOOLE_1:16;
now
let x be object; assume A2: x in m-tuples_on B; then
reconsider xx=x as m-element FinSequence by FINSEQ_2:141;
xx in mm-tuples_on B by A2;then len xx=mm & rng xx c= B by FINSEQ_2:132;then
x is FinSequence of B by FINSEQ_1:def 4;hence x in B* by FINSEQ_1:def 11;
end;
then R c= L by XBOOLE_1:26, TARSKI:def 3;
hence thesis by A1;
end;
Lm9: Funcs(A,B) /\ Funcs(A,C) = Funcs(A,B/\C)
proof
set L=Funcs(A,B) /\ Funcs(A,C), R= Funcs(A,B/\C);
now
let f be object;
assume f in L; then A1: f in Funcs(A,B) & f in Funcs(A,C) by
XBOOLE_0:def 4;
consider f1 being Function such that
A2: f1=f & dom f1=A & rng f1 c= B by FUNCT_2:def 2,A1;
consider f2 being Function such that
A3: f2=f & dom f2=A & rng f2 c= C by FUNCT_2:def 2,A1;
f1=f & dom f1=A & rng f1 c= B/\C by XBOOLE_1:19, A2, A3;
hence f in Funcs(A,B/\C) by FUNCT_2:def 2;
end;
then A4: L c= R;
R c= Funcs(A,B) & R c= Funcs(A,C) by XBOOLE_1:17, FUNCT_5:56; then
R c= L by XBOOLE_1:19; hence thesis by A4;
end;
theorem Th2: m-tuples_on A /\ (B*) = m-tuples_on (A/\B)
proof
m-tuples_on (A/\B)= Funcs(Seg m, A/\B) by Lm7 .=
Funcs(Seg m,A) /\ Funcs(Seg m,B) by Lm9 .=
m-tuples_on A /\ Funcs(Seg m,B) by Lm7 .= m-tuples_on A /\ m-tuples_on B
by Lm7 .= m-tuples_on A/\(B*) by Th1; hence thesis;
end;
theorem Th3: m-tuples_on (A/\B)=m-tuples_on A /\ (m-tuples_on B)
proof
m-tuples_on (A/\B) = m-tuples_on A /\ (B*) by Th2 .=
m-tuples_on A /\ (m-tuples_on B) by Th1; hence thesis;
end;
Lm10:
for x,y being FinSequence of D holds (D-concatenation).(x,y) = x^y
proof
let x,y be FinSequence of D;
reconsider x2=x, y2=y as Element of D* by FINSEQ_1:def 11;
reconsider x1=x2, y1=y2 as Element of D*+^ by MONOID_0:def 34;
A1: D-concatenation = the multF of D*+^ by MONOID_0:def 36;
x1^y1 = x1 * y1 by MONOID_0:def 34
.= (D-concatenation).(x1,y1) by A1, ALGSTR_0:def 18;
hence thesis;
end;
theorem Th4: for x,y being FinSequence st x is U-valued & y is U-valued
holds (U-concatenation).(x,y)=x^y
proof
let x,y be FinSequence; set f=U-concatenation; assume x is U-valued &
y is U-valued; then reconsider xx=x, yy=y as FinSequence of U by Lm1;
f.(xx,yy)=xx^yy by Lm10; hence thesis;
end;
theorem Th5: for x being set holds ::#th5 1, to be replaced by Th30
(x is non empty FinSequence of D iff x in D*\{{}})
proof
let x be set;
thus x is non empty FinSequence of D implies x in D*\{{}}
proof
assume x is non empty FinSequence of D;
then not x in {{}} & x in D* by FINSEQ_1:def 11, TARSKI:def 1;
hence thesis by XBOOLE_0:def 5;
end;
assume x in D*\{{}}; then
x in D* & not x in {{}} by XBOOLE_0:def 5;
hence thesis by FINSEQ_1:def 11, TARSKI:def 1;
end;
Lm11: B is f-unambiguous & A c= B implies A is f-unambiguous
proof
assume A0: B is f-unambiguous & A c= B; then
[:A,D:] c= [:B,D:] by ZFMISC_1:95; then
f is [:A,D:]-one-to-one by A0,Lm4;
hence thesis;
end;
Lm12: {} is f-unambiguous
proof
reconsider A=[:{},D:] as empty set;
f is A-one-to-one;hence thesis;
end;
Lm13:
for f,g being FinSequence holds dom <:f,g:>=Seg (min (len f, len g))
proof
let f,g be FinSequence; set m=len f, n=len g, l=min(m,n);
thus dom <:f,g:> = dom f /\ dom g by FUNCT_3:def 7 .=
Seg m /\ dom g by FINSEQ_1:def 3 .=
Seg m /\ Seg n by FINSEQ_1:def 3 .= Seg l by FINSEQ_2:2;
end;
::##################### Preliminary lemmas ############################
::############################## END ##################################
::############################ Type tuning ############################
registration
let D be non empty set;
cluster D-pr1 -> associative for BinOp of D;
coherence
proof
now
let a,b,c be Element of D; D-pr1.(a,D-pr1.(b,c))=a &
D-pr1.(D-pr1.(a,b),c)=D-pr1.(a,c) by FUNCT_3:def 4;
hence D-pr1.(a,D-pr1.(b,c))=D-pr1.(D-pr1.(a,b),c) by FUNCT_3:def 4;
end;
hence thesis;
end;
end;
registration
let D be set;
cluster associative for BinOp of D;
existence
proof
per cases;
suppose D is non empty; then reconsider DD=D as non empty set;
set f = DD-pr1;
reconsider ff=f as BinOp of D; take ff; thus thesis;
end;
suppose D is empty; then reconsider DD=D as empty set;
set f = the BinOp of {}; f is associative & f is BinOp of DD; hence thesis;
end;
end;
end;
definition
let X be set, Y be Subset of X;
redefine func Y* -> non empty Subset of X*; :: redefines * (FINSEQ_1, definition)
coherence by FINSEQ_1:62;
end;
registration
let D be non empty set;
cluster D-concatenation -> associative for (BinOp of D*);
coherence by MONOID_0:67;
end;
registration
let D be non empty set;
cluster D* \ {{}} -> non empty;
coherence
proof
set x = the Element of D;
<*x*> in D* & not <*x*> in {{}} by FINSEQ_1:def 11;
hence thesis by XBOOLE_0:def 5;
end;
end;
registration ::#exreg4 1
let D be non empty set, m be Nat;
cluster m-element for Element of D*;
existence
proof
set p = the m-element FinSequence of D;
reconsider pp=p as
Element of D* by FINSEQ_1:def 11; take pp; thus thesis;
end;
end;
definition
let X be set;
let f be Function;
redefine attr f is X-one-to-one means :Def6: :: redefines -one-to-one (FOMODEL0, definition)
(for x,y being set st x in X /\ dom f & y in X /\ dom f & f.x=f.y holds x=y);
compatibility by Lm3;
end;
registration
let D,f;
cluster f-unambiguous for set;
existence proof take {}; thus thesis by Lm12; end;
end;
registration
::# cfr cluster trivial -> one-to-one Function in NECKLACE.MIZ
::# this alternate proof tries to reuse existing results instead
let f be Function, x be set;
cluster f|{x} -> one-to-one for Function;
coherence
proof
set g=f|{x}; per cases;
suppose x in dom f; then g = x .--> (f.x) by FUNCT_7:6; hence thesis; end;
suppose not x in dom f; then reconsider
gg=g as empty Function by RELAT_1:152, ZFMISC_1:50; gg is one-to-one;
hence thesis;
end;
end;
end;
registration
let e be empty set;
identify e* with {e};
compatibility by FUNCT_7:17;
identify {e} with e*;
compatibility;
end;
registration
cluster empty -> empty-membered for set;
coherence;
::#thanks to cluster with_non-empty_element -> non empty set from SETFAM_1;
let e be empty set;
cluster {e} -> empty-membered;
coherence
proof
not ex x being non empty set st x in {e} by TARSKI:def 1;
hence thesis by SETFAM_1:def 10;
end;
end;
registration
let U; let m1 be non zero Nat;
cluster m1-tuples_on U -> with_non-empty_elements;
coherence
proof
not {} is Element of m1-tuples_on U;
hence thesis by SETFAM_1:def 8;
end;
end;
registration
let X be empty-membered set;
cluster -> empty-membered for Subset of X;
coherence
proof
let Y be Subset of X;
not ex x being non empty set st x in Y by SETFAM_1:def 10;
hence thesis by SETFAM_1:def 10;
end;
end;
registration
let A; let m0 be zero number;
cluster m0-tuples_on A -> empty-membered for set;
coherence by Lm6;
end;
registration
let e be empty set; let m1 be non zero Nat;
cluster m1-tuples_on e -> empty for set;
coherence by FINSEQ_3:119;
end;
registration
let D,f; let e be empty set;
cluster e /\ f -> f-unambiguous for set;
coherence by Lm12;
end;
registration
let U; let e be empty set;
cluster e/\U -> U-prefix for set;
coherence
proof
set f=U-concatenation; e/\f is f-unambiguous; hence thesis;
end;
end;
registration
let U;
cluster U-prefix for set;
existence proof take {}/\U; thus thesis; end;
end;
::############################ Type tuning ############################
::############################## END ##################################
::########################### MultPlace ###############################
definition
let D,f;
let x be FinSequence of D;
func MultPlace(f,x) -> Function means :Def7:
dom it=NAT & it.0=x.1 & for n being Nat holds it.(n+1)=f.(it.n,x.(n+2));
existence
proof
deffunc F(Nat, set) = f.($2, x.($1+2));
consider f1 being Function such that A1: dom f1 = NAT &
f1.0=x.1 & for n being Nat holds f1.(n+1) = F (n,f1.n) from NAT_1:sch 11;
take f1;
thus thesis by A1;
end;
uniqueness
proof
let IT1, IT2 be Function;
assume A2:
dom IT1=NAT & IT1.0 = x.1 &
for n being Nat holds IT1.(n+1) = f.(IT1.n, x.(n+2));
assume A3:
dom IT2=NAT & IT2.0 = x.1 &
for n being Nat holds IT2.(n+1) = f.( IT2.n, x.(n+2));
deffunc RecFun(Nat,set)=f.( $2, x.($1+2));
A4: dom IT1=NAT by A2;
A5: IT1.0=x.1 by A2;
A6: for n being Nat holds IT1.(n+1) = RecFun(n, IT1.n) by A2;
A7: dom IT2=NAT by A3;
A8: IT2.0=x.1 by A3;
A9: for n being Nat holds IT2.(n+1) = RecFun(n, IT2.n) by A3;
thus thesis from NAT_1:sch 15(A4,A5,A6,A7,A8,A9);
end;
end;
Lm14: for x being FinSequence of D holds 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
let x be FinSequence of D;
defpred Q[Nat] means $1+1<=len x implies MultPlace(f,x).$1 in D;
A1: Q[0]
proof
assume 0+1<=len x;
then 1 in Seg len x;
then 1 in dom x by FINSEQ_1:def 3;
then x.1 in rng x & rng x c= D by FUNCT_1:def 3;
then x.1 in D & MultPlace(f,x).0 = x.1 by Def7;
hence thesis;
end;
A2: for m being Nat st Q[m] holds Q[m+1]
proof
let m be Nat;
assume A3: Q[m];
assume A4: (m+1)+1 <= len x;
then m+2 <= len x & 1<=m+2 by NAT_1:12;
then m+2 in Seg len x;
then m+2 in dom x by FINSEQ_1:def 3; then
A5: x.(m+2) in rng x & rng x c= D by FUNCT_1:def 3;
A6: (m+1<=m+2 implies m+1 <= len x) by A4, XXREAL_0:2;
[MultPlace(f,x).m , x.(m+2)] in [:D,D:]
by A6, A3, XREAL_1:8 , A5, ZFMISC_1:def 2;
then f.((MultPlace(f,x)).m, x.(m+2)) in D by FUNCT_2:5;
hence thesis by Def7;
end;
defpred P[Nat] means
for n being Nat st n >= ($1+1) holds MultPlace(f,x|n).$1 = MultPlace(f,x).$1;
A7:P[0]
proof
let n be Nat; assume
A8: n>= 0+1;
MultPlace(f,x|n).0 = (x|n).1 by Def7
.= x.1 by FINSEQ_3:112, A8
.=MultPlace(f,x).0 by Def7;
hence thesis;
end;
A9: for m being Nat st P[m] holds P[m+1]
proof
let m be Nat; assume
A10: P[m]; let n be Nat; assume
A11: n >= m+1+1; then
A12: m+2>=m+1 & n>=m+2 by XREAL_1:8;
MultPlace(f,x|n).(m+1)=f.( MultPlace(f,x|n).m, (x|n).(m+2)) by Def7
.= f.(MultPlace(f,x).m, (x|n).(m+2)) by A10,XXREAL_0:2, A12
.= f.(MultPlace(f,x).m, x.(m+2)) by A11, FINSEQ_3:112
.= MultPlace(f,x).(m+1) by Def7;
hence thesis;
end;
defpred R[Nat] means P[$1] & Q[$1];
A13: R[0] by A7,A1;
A14: for m being Nat st R[m] holds R[m+1] by A9,A2;
for m being Nat holds R[m] from NAT_1:sch 2(A13,A14);
hence thesis;
end;
definition
let D,f;
let x be Element of D*\{{}};
func MultPlace(f,x) -> Function equals MultPlace(f, x qua Element of D*);
coherence;
end;
definition
let D,f;
::# MultPlace is an operator which transforms a BinOp f into a function
::# operating # on an arbitrary (positive and natural) number of arguments by
::# recursively # associating f on the left # Too late I realized something
::# similar (yielding a functor rather than # a function, though) was
::# introduced in FINSOP_1
func MultPlace(f) -> Function of D*\{{}}, D means :Def9:
for x being Element of D*\{{}} holds
it.x=MultPlace(f,x).(len x - 1);
existence
proof
defpred P[Element of D*\{{}}, Element of D] means
$2=MultPlace(f,$1).(len $1 - 1);
A1: for x being Element of D*\{{}} ex y being Element of D st P[x,y]
proof
let x be Element of D*\{{}};
reconsider x1=x as Element of D*;
not x1 in {{}} by XBOOLE_0:def 5;
then x1 <> {} by TARSKI:def 1;
then len x1 >= 1 by FINSEQ_1:20;
then len x1 - 1 in NAT by INT_1:3, XREAL_1:48;
then reconsider m=(len x1 - 1) as Nat;
A2: m + 1 <= len x1;
reconsider y=MultPlace(f,x1).m as Element of D
by Lm14, A2;
take y;
thus thesis;
end;
consider g being Function of D*\{{}}, D such that
A3:for x being Element of D*\{{}} holds P[x,g.x] from FUNCT_2:sch 3(A1);
take g;
thus thesis by A3;
end;
uniqueness
proof
let IT1,IT2 be Function of D*\{{}}, D;
A4: dom IT1=D*\{{}} & dom IT2=D*\{{}} by FUNCT_2:def 1;
assume A5: for x being Element of D*\{{}} holds
IT1.x=MultPlace(f,x).(len x - 1);
assume A6: for x being Element of D*\{{}} holds
IT2.x=MultPlace(f,x).(len x - 1);
now
let x be object; assume x in dom IT1;
then reconsider xx=x as Element of D*\{{}};
IT1.x=MultPlace(f,xx).(len xx - 1) by A5 .= IT2.x by A6;
hence IT1.x=IT2.x;
end;
hence thesis by FUNCT_1:2, A4;
end;
end;
Lm15: for x being non empty FinSequence of D,
y being Element of D holds (MultPlace(f)).(<*y*>) = y &
(MultPlace(f)).(x^<*y*>) = f.((MultPlace(f)).x, y)
proof
set F=MultPlace(f);
let x be non empty FinSequence of D, y be Element of D;
consider k being Nat such that A1: k+1 = len x by NAT_1:6;
reconsider x0=x as Element of D*\{{}} by Th5;
reconsider x1=x^<*y*> as non empty FinSequence of D;
1 in Seg 1; then 1 in dom <* y *> by FINSEQ_1:def 8; then
A2: x1.(len x + 1)=(<*y*>).1 by FINSEQ_1:def 7 .= y;
A3: x1|(len x)=x|(len x) by FINSEQ_5:22 .= x by FINSEQ_3:49;
A4: len <*y*> =1 by FINSEQ_1:40; then A5: len x1=len x + 1 by FINSEQ_1:22;
reconsider y1=<* y *> as non empty FinSequence of D;
reconsider y2=y1 as Element of D*\{{}} by Th5;
len y2 - 1 =0 by A4; then F.(y2) = MultPlace(f, y2).0 by Def9
.= y2.1 by Def7 .= y;
hence F.(<* y *>) = y;
reconsider x2=x1 as Element of D*\{{}} by Th5;
F.x2 = (MultPlace(f,x2)).(len x2 - 1) by Def9
.= f.((MultPlace(f,x2)).k, x2.(k+2)) by Def7, A1, A5
.= f.((MultPlace(f,x0)).(len x - 1), x2.(len x + 1)) by A3, A1, Lm14
.= f.(F.x0, y) by A2, Def9;
hence thesis;
end;
Lm16: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
A1: dom f=[:D,D:] by FUNCT_2:def 1;
let X be set;
thus f is [:X,D:]-one-to-one implies
(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
assume
A2: f is [:X,D:]-one-to-one;
let x,y,d1,d2 be set;
assume A3: x in X/\D & y in X/\D & d1 in D & d2 in D & f.(x,d1)=f.(y,d2);
then [x,d1] in [:X/\D,D/\D:] & [y,d2] in [:X/\D,D/\D:] by ZFMISC_1:def 2;
then A4: [x,d1] in [:X,D:] /\ [:D,D:] & [y,d2] in [:X,D:] /\ [:D,D:]
by ZFMISC_1:100; [x,d1] = [y,d2] by A1,A2 , A4, A3;
hence x=y & d1=d2 by XTUPLE_0:1;
end;
assume
A5: 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;
now
let x,y be set; assume
A6: x in [:X,D:] /\ dom f & y in [:X,D:] /\ dom f & f.x=f.y; then
A7: x in [:X/\D, D/\D:] & y in [:X/\D,D/\D:] & f.x=f.y by ZFMISC_1:100,A1;
then consider x1,d1 being object such that
A8: x1 in X/\D & d1 in D & x=[x1,d1] by ZFMISC_1:def 2;
consider x2,d2 being object such that
A9: x2 in X/\D & d2 in D & y=[x2,d2] by ZFMISC_1:def 2,A7;
x1 in X/\D & x2 in X/\D & d1 in D & d2 in D & f.(x1,d1)=f.(x2,d2) by A8,A9,
A6;
then x1=x2 & d1=d2 by A5; hence x=y by A8,A9;
end;
hence f is [:X,D:]-one-to-one;
end;
definition ::#def10 1
let D,f; let X be set;
redefine attr X is f-unambiguous means :Def10: :: redefines -unambiguous (FOMODEL0, definition)
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
by Lm16;
end;
Lm17:f is associative implies for d being Element of D holds
(for m being Nat, x being Element of (m+1)-tuples_on D holds
(MultPlace(f)).(<*d*>^x)=f.(d,(MultPlace(f)).x))
proof
set F=MultPlace(f);
assume A1: f is associative;
let d be Element of D;
defpred P[Nat] means for x being Element of ($1+1)-tuples_on D holds
F.(<*d*>^x) = f.(d, F.x);
A2: P[0]
proof
let x be Element of (0+1)-tuples_on D;
consider xx being Element of D such that A3: x=<*xx*> by FINSEQ_2:97;
F.(<*d*>^x)=
f.(F.(<*d*>), xx ) by Lm15, A3
.= f.(d,xx) by Lm15 .= f.(d,F.x) by Lm15,A3;
hence thesis;
end;
A4: for m being Nat holds (P[m] implies P[m+1])
proof
let m be Nat;
assume A5: P[m];
let x be Element of ((m+1)+1)-tuples_on D;
m+1+0 <= m+1+1 & len x = (m+1)+1 by CARD_1:def 7,XREAL_1:8;
then len(x|(m+1))=m+1 by FINSEQ_1:59; then
reconsider xx=x|(m+1) as Element of (m+1)-tuples_on D by FINSEQ_2:92;
reconsider xxx=xx as non empty FinSequence of D;
reconsider y=x /. len x as Element of D;
reconsider XX=F.xxx as Element of D by FUNCT_2:5, Th5;
A6: (m+1)+1 = len x by CARD_1:def 7; then
F.(<*d*>^x)=F.(<*d*>^(x|(m+1) ^ <*y*>)) by FINSEQ_5:21
.= F.((<*d*> ^ xx)^<*y*>) by FINSEQ_1:32
.= f.(F.(<*d*>^xx), y) by Lm15 .= f.(f.(d, F.xx), y) by A5
.= f.(d, f.(XX, y )) by A1
.= f.(d,F.(xxx^<*y*>)) by Lm15 .= f.(d,F.x) by FINSEQ_5:21, A6;
hence thesis;
end;
thus for m being Nat holds P[m] from NAT_1:sch 2(A2,A4);
end;
Lm18: (f is associative & X is f-unambiguous) implies
(MultPlace(f)).:((m+1)-tuples_on X) is f-unambiguous
proof
set F=MultPlace(f);
assume A1: f is associative;
assume A2: X is f-unambiguous;
defpred P[Nat] means F.:(($1+1)-tuples_on X) is f-unambiguous;
A3: P[0]
proof
set Z=(0+1)-tuples_on X;
set Y=F.:Z;
for x,y,d1,d2 being set st x in Y/\D & y in Y/\D & d1 in D &
d2 in D & f.(x,d1)=f.(y,d2) holds x=y & d1=d2
proof
let x,y,d1,d2 be set;
assume x in Y/\D; then x in Y by XBOOLE_0:def 4;
then consider uu being object such that A4:
uu in dom F & [uu,x] in F & uu in Z by RELAT_1:110;
assume y in Y/\D; then y in Y by XBOOLE_0:def 4;
then consider vv being object such that A5:
vv in dom F & [vv,y] in F & vv in Z by RELAT_1:110;
assume d1 in D;
then reconsider d11=d1 as Element of D;
assume d2 in D;
then reconsider d22=d2 as Element of D;
reconsider u=uu as Element of 1-tuples_on X by A4;
reconsider v=vv as Element of 1-tuples_on X by A5;
assume f.(x,d1)=f.(y,d2); then
A6: f.(x,d1)=f.(y,d2) & F.u=x & F.v=y by A4,A5,FUNCT_1:def 2;
consider ee being Element of X such that A7: u=<*ee*> by FINSEQ_2:97;
consider ff being Element of X such that A8: v=<*ff*> by FINSEQ_2:97;
reconsider eee=ee, fff=ff as Element of D;
f.(F.<*eee*>,d1)=f.(F.<*fff*>,d2) & F.<*eee*>=eee & F.<*fff*>=fff
by A6, A7, A8, Lm15;
then ee in X/\D & ff in X/\D & d11 in D & d22 in D
& f.(ee,d11)=f.(ff,d22) by XBOOLE_0:def 4;
hence thesis by A6, A7, A8, A2;
end;
hence thesis by Def10;
end;
A9: for m being Nat st P[m] holds P[m+1]
proof
let m be Nat;
assume A10: P[m]; set Z=(m+1+1)-tuples_on X; set Y=F.:Z;
for x,y,d1,d2 being set st x in Y/\D & y in Y/\D & d1 in D &
d2 in D & f.(x,d1)=f.(y,d2) holds x=y & d1=d2
proof
let x,y,d1,d2 be set;
assume x in Y/\D; then x in Y by XBOOLE_0:def 4;
then consider uu being object such that A11:
uu in dom F & [uu,x] in F & uu in Z by RELAT_1:110;
assume y in Y/\D; then y in Y by XBOOLE_0:def 4;
then consider vv being object such that A12:
vv in dom F & [vv,y] in F & vv in Z by RELAT_1:110;
assume d1 in D;
then reconsider d11=d1 as Element of D;
assume d2 in D;
then reconsider d22=d2 as Element of D;
reconsider u=uu as Element of (m+1+1)-tuples_on X by A11;
reconsider v=vv as Element of (m+1+1)-tuples_on X by A12;
len u=m+1+1 & len v=m+1+1 & m+1 <= m+1+1
by CARD_1:def 7, NAT_1:11; then
A13: u=(u|(m+1))^<*u/.(len u)*> & v=(v|(m+1))^<*v/.(len v)*>
& len (u|(m+1))=m+1 & len (v|(m+1))=m+1 by FINSEQ_5:21, FINSEQ_1:59;
then reconsider u1=u|(m+1),v1=v|(m+1) as Tuple of m+1, X by CARD_1:def 7;
rng u1 c= D & rng v1 c= D by XBOOLE_1:1;
then reconsider u2=u1, v2=v1 as non empty FinSequence of D
by FINSEQ_1:def 4;
reconsider u3=u2, v3=v2 as Element of D*\{{}} by Th5;
reconsider u4=u2, v4=v3 as Element of (m+1)-tuples_on X by FINSEQ_2:131;
reconsider ul=u/.len u, vl=v/.len v as Element of D by TARSKI:def 3;
A14: ul in X/\D & vl in X /\ D by XBOOLE_0:def 4;
A15: F.(u2^<*ul*>)=f.(F.u2,ul) & F.(v2^<*vl*>)=f.(F.v2,vl) by Lm15;
A16: f.(f.(F.u3,ul),d11)=f.(F.u3,f.(ul,d11)) &
f.(f.(F.v3,vl),d22)=f.(F.v3,f.(vl,d22)) by A1;
assume
f.(x,d1)=f.(y,d2); then
A17: f.(x,d1)=f.(y,d2) & F.u=x & F.v=y by A11,A12,FUNCT_1:def 2;
dom F=D*\{{}} by FUNCT_2:def 1; then
u3 in dom F & v3 in dom F &
u4 in (m+1)-tuples_on X & v4 in (m+1)-tuples_on X; then
F.u4 in F.:((m+1)-tuples_on X) & F.v4 in F.:((m+1)-tuples_on X)
& f.(ul,d11) in D & f.(vl,d22) in D by FUNCT_1:def 6; then
F.u4 in F.:((m+1)-tuples_on X) /\ D & F.v4 in F.:((m+1)-tuples_on X) /\D
& f.(ul,d11) in D & f.(vl,d22) in D by XBOOLE_0:def 4; then
A18: F.u3=F.v3 & f.(ul,d11)=f.(vl,d22) by A17, A13, A15, A16, A10, Def10;
thus x=y & d1=d2 by A18,A2, A14, A17, A13, A15;
end;
hence thesis by Def10;
end;
for m being Nat holds P[m] from NAT_1:sch 2(A3,A9);
hence thesis;
end;
Lm19: f is associative & Y is f-unambiguous implies
(MultPlace(f)).:((m+1)-tuples_on Y) is f-unambiguous
proof
set F=MultPlace(f); A1: dom F = D*\{{}} by FUNCT_2:def 1;
assume f is associative & Y is f-unambiguous; then A2:
f is associative & Y/\D is f-unambiguous by XBOOLE_1:17, Lm11;
A3: F.:((m+1)-tuples_on Y) =
F.:( (D*\{{}}) /\ (m+1)-tuples_on Y) by A1, RELAT_1:112 .=
F.: ( (D* /\ (m+1)-tuples_on Y)\{{}}) by XBOOLE_1:49 .=
F.: (((m+1)-tuples_on (Y/\D))\{{}}) by Th2 .=
F.: (((m+1)-tuples_on (Y/\D))\(0-tuples_on Y)) by Lm6
.= F.:((m+1)-tuples_on (Y/\D)) by Lm5, XBOOLE_1:83;
per cases;
suppose Y/\D <> {}; then reconsider YY=Y/\D as non empty Subset of D by
XBOOLE_1:17; F.:((m+1)-tuples_on Y)=F.:((m+1)-tuples_on YY) by A3;
hence thesis by Lm18, A2;
end;
suppose Y/\D = {}; then
F.:((m+1)-tuples_on Y) = {} by A3; hence thesis;
end;
end;
Lm20: (f is associative & X is f-unambiguous) implies
(MultPlace(f)) is ((m+1)-tuples_on X)-one-to-one
proof
set F=MultPlace(f);
A1: dom F=D*\{{}} by FUNCT_2:def 1;
defpred P[Nat] means F is (($1+1)-tuples_on X)-one-to-one; assume
A2: f is associative & X is f-unambiguous;
A3: P[0]
proof
now
let x,y be set; assume
A4: x in (0+1)-tuples_on X /\ dom F &
y in (0+1)-tuples_on X /\ dom F & F.x=F.y; then
A5: x is Element of 1-tuples_on X & y is Element of 1-tuples_on X & F.x=F.y
by XBOOLE_0:def 4;
consider u being Element of X such that A6: x=<*u*> by FINSEQ_2:97,A5;
consider v being Element of X such that A7: y=<*v*> by FINSEQ_2:97,A5;
reconsider uu=u,vv=v as Element of D;
uu=F.y by A4, A6, Lm15 .= vv by A7,Lm15;
hence x=y by A6,A7;
end;
hence F is ((0+1)-tuples_on X)-one-to-one;
end;
A8: for m being Nat st P[m] holds P[m+1]
proof
let m be Nat; assume A9: P[m];
set goal=(m+1+1)-tuples_on X;
now
let x,y be set; assume
A10: x in goal /\ dom F & y in goal /\ dom F & F.x=F.y;
reconsider xx=x,yy=y as Element of (m+1+1)-tuples_on X by XBOOLE_0:def 4, A10;
len xx=m+1+1 & len yy=m+1+1 & m+1+0<=m+1+1 by CARD_1:def 7, NAT_1:11;
then len(xx|(m+1))=m+1 & len(yy|(m+1))=m+1 by FINSEQ_1:59; then
reconsider x1=xx|(m+1),y1=yy|(m+1) as Element of (m+1)-tuples_on X
by FINSEQ_2:92;
reconsider x11=x1, y11=y1 as non empty FinSequence of X;
rng x11 c= D & rng y11 c= D by XBOOLE_1:1; then
reconsider x111=x11, y111=y11 as non empty FinSequence of D by FINSEQ_1:def 4;
reconsider xl=xx/.len xx,yl=yy/.len yy as Element of D by TARSKI:def 3;
A11: F.(x111^<*xl*>)=f.(F.x111,xl) & F.(y111^<*yl*>)=f.(F.y111,yl)
by Lm15;
len xx=m+1+1 & len yy=m+1+1 by CARD_1:def 7; then
A12: xx=x1^<*xl*> & yy=y1^<*yl*> by FINSEQ_5:21;
A13: x111 in dom F & x1 in (m+1)-tuples_on X &
y111 in dom F & y1 in (m+1)-tuples_on X by Th5,A1;
then
F.x1 in F.:((m+1)-tuples_on X) & F.x111 in D &
F.y1 in F.:((m+1)-tuples_on X) & F.y111 in D by PARTFUN1:4, FUNCT_1:def 6;
then A14: F.x1 in F.:((m+1)-tuples_on X) /\ D &
F.y1 in F.:((m+1)-tuples_on X) /\ D & xl in D & yl in D
& f.(F.x1,xl)=f.(F.y1,yl) by XBOOLE_0:def 4, A12, A11, A10;
F.:((m+1)-tuples_on X) is f-unambiguous by A2, Lm18;
then A15: F.x1=F.y1 & xl=yl by A14;
x1 in (m+1)-tuples_on X /\ dom F &
y1 in (m+1)-tuples_on X /\ dom F by A13,XBOOLE_0:def 4;
hence x=y by A15,A9,Def6, A12;
end;
hence F is goal-one-to-one;
end;
for m being Nat holds P[m] from NAT_1:sch 2(A3,A8);
hence thesis;
end;
Lm21: (f is associative & Y is f-unambiguous) implies
(MultPlace(f)) is ((m+1)-tuples_on Y)-one-to-one
proof
assume A1: f is associative & Y is f-unambiguous; set F=MultPlace(f);
A2: F|((m+1)-tuples_on Y)=(F|(D*\{{}}))|((m+1)-tuples_on Y)
.= F|((D*\{{}})/\((m+1)-tuples_on Y)) by RELAT_1:71 .=
F|(D*/\((m+1)-tuples_on Y)\{{}}) by XBOOLE_1:49 .=
F|(D*/\(((m+1)-tuples_on Y)\{{}})) by XBOOLE_1:49 .=
F|(D*/\(((m+1)-tuples_on Y)\0-tuples_on Y)) by Lm6 .=
F|(D*/\((m+1)-tuples_on Y)) by XBOOLE_1:83, Lm5 .=
F|((m+1)-tuples_on (Y/\D)) by Th2;
A3: Y/\D is f-unambiguous by Lm11, A1, XBOOLE_1:17;
per cases;
suppose D/\Y <> {}; then reconsider X=D/\Y as non empty Subset of D
by XBOOLE_1:17;
F is ((m+1)-tuples_on X)-one-to-one by Lm20,A3,A1; then
F|((m+1)-tuples_on Y) is one-to-one by A2; hence thesis;
end;
suppose D/\Y={};
hence thesis by A2;
end;
end;
::########################### MultPlace ###############################
::############################## END ##################################
::########################### FirstChar ###############################
definition
let D;
::# A function-like extracting the first item of a non empty FinSequence of D
func D-firstChar -> Function of D*\{{}}, D equals
MultPlace(D-pr1);
coherence;
end;
Lm22: for w being non empty FinSequence of D holds D-firstChar.w=w.1
proof
let w be non empty FinSequence of D;
consider d being Element of D, df1 being FinSequence of D such that A1:
d = w.1 & w=<*d*>^df1 by FINSEQ_3:102;
set f=D-pr1, F=MultPlace(f);
per cases;
suppose len w <= 1;
then len w <= 0 or len w=0+1 by NAT_1:8;
then w=<*d*> by A1, FINSEQ_1:40;
hence thesis by Lm15;
end;
suppose
A2: len w > 1;
len w = len <*d*> + len df1 by A1, FINSEQ_1:22 .= 1 + len df1 by FINSEQ_1:40;
then len df1 <>0 by A2; then consider k being Nat such that
A3: len df1=k+1 by NAT_1:6;
reconsider df11 = df1 as Element of (k+1)-tuples_on D by A3, FINSEQ_2:133;
reconsider df111=df11 as Element of D*\{{}} by Th5;
F.w =
(pr1(D,D)).(d,(MultPlace(f)).df111) by A1, Lm17 .= w.1 by FUNCT_3:def 4, A1;
hence thesis;
end;
end;
theorem Th6: for p being FinSequence st p is U-valued & p is non empty
holds U-firstChar.p=p.1
proof
let p be FinSequence; assume p is U-valued & p is non empty; then
reconsider pp=p as non empty FinSequence of U by Lm1;
U-firstChar.pp=pp.1 by Lm22; hence thesis;
end;
::########################### FirstChar ###############################
::############################## END ##################################
::########################### MultiCat #################################
::#When f is concatenation of strings, MultPlace(f) can be extended to the
::#empty finsequence of strings in the immediate way, obtaining the multiCat
::#function, which chains an arbitrary (natural) number of strings
definition
let D;
func D-multiCat -> Function equals
({} .--> {}) +* MultPlace(D-concatenation);
coherence;
end;
definition
let D;
redefine func D-multiCat -> Function of D**,D*; :: redefines -multiCat (FOMODEL0, definition)
coherence
proof
A1: {{}} c= D** & {{}} c= D* by ZFMISC_1:31, FINSEQ_1:49; then
A2: {{}}\/D** = D** & {{}}\/D*=D* by XBOOLE_1:12;
set f={} .--> {}; set g=MultPlace(D-concatenation);
A3: dom f = {{}} & rng f c= {{}} by FUNCOP_1:13;
A4: dom g = D**\{{}} & rng g c= D* by FUNCT_2:def 1;
dom f \/ dom g = {{}} \/ D** by XBOOLE_1:39,A4;
then A5: dom f \/ dom g = D** by A1, XBOOLE_1:12;
rng f \/ rng g c= D* & rng (f +* g) c= rng f \/ rng g
by A2, A3, XBOOLE_1:13, FUNCT_4:17; then
dom (D-multiCat)=D** & rng (D-multiCat) c= D*
by FUNCT_4:def 1, A5;
hence thesis by RELSET_1:4, FUNCT_2:67;
end;
end;
Lm23:D-multiCat | (D**\{{}}) = MultPlace(D-concatenation)
proof
set f=D-concatenation; set F=MultPlace(f);
dom F=D**\{{}} by FUNCT_2:def 1; hence thesis;
end;
Lm24:D-multiCat | (Y\{{}}) = (MultPlace(D-concatenation)) | Y
proof
set F=D-multiCat; F|(Y\{{}})=(F|(D**))|(Y\{{}}) .= F|(D**/\(Y\{{}}))
by RELAT_1:71 .= F|((D** /\ Y )\{{}}) by XBOOLE_1:49 .=
D-multiCat|(Y/\(D**\{{}})) by XBOOLE_1:49 .= (D-multiCat|(D**\{{}}))|Y
by RELAT_1:71 .= (MultPlace(D-concatenation)) |Y by Lm23; hence thesis;
end;
Lm25: ({} .--> {}) tolerates MultPlace(D-concatenation)
proof
set f={}.-->{}; set g=MultPlace(D-concatenation);
dom f = {{}} & dom g=D**\{{}} by FUNCT_2:def 1;
then for x being object st x in dom g /\ dom f holds f.x=g.x
by XBOOLE_1:79, XBOOLE_0:def 7;
hence thesis by PARTFUN1:def 4;
end;
registration
let D; let e be empty set;
cluster (D-multiCat).e -> empty for set;
coherence
proof
set g=MultPlace(D-concatenation), f={}.-->{};
{} in dom f by TARSKI:def 1; then A1:
{} in dom f & {} in dom g \/ dom f by XBOOLE_0:def 3;
D-multiCat=g +* f by Lm25, FUNCT_4:34; then e={} & (D-multiCat).{}=f.{}
by A1, FUNCT_4:def 1; hence thesis;
end;
end;
registration
let D;
cluster -> D-prefix for (Subset of 1-tuples_on D);
coherence
proof
set f=D-concatenation, D1=1-tuples_on D; let X be Subset of D1;
now
let x1,x2,d1,d2 be set; assume A1:
x1 in X/\(D*) & x2 in X/\(D*) & d1 in D* & d2 in D*; then
reconsider x11=x1, x22=x2 as Element of D1;
reconsider x111=x11, x222=x22 as 1-element FinSequence; reconsider
x1111=x11,x2222=x22 as Element of D* by FINSEQ_2:142, TARSKI:def 3;
reconsider xx1=x1111,xx2=x2222,dd1=d1,dd2=d2 as FinSequence of D
by FINSEQ_1:def 11, A1;
len xx1=1 & len xx2= 1 by CARD_1:def 7; then
A2: xx1=<*xx1.1*> & xx2=<*xx2.1*> by FINSEQ_1:40;
A3: f.(x1,d1)=xx1^dd1 & f.(x2,d2)=xx2^dd2 by Lm10; assume
A4: f.(x1,d1)=f.(x2,d2);
A5: xx1.1= (xx1^dd1).1 by A2, FINSEQ_1:41 .= xx2.1
by A2, A4, A3, FINSEQ_1:41;
thus x1=x2 & d1=d2 by FINSEQ_1:33, A5, A2, A4, A3;
end;
hence thesis by Def10;
end;
end;
theorem Th7: ::#Th7
A is D-prefix implies (D-multiCat).:(m-tuples_on A) is D-prefix
proof
reconsider f=D-concatenation as BinOp of (D*);
set F=D-multiCat, Y=F.:(m-tuples_on A); {} in D** by FINSEQ_1:49; then
A1: {} in dom F by FUNCT_2:def 1;
per cases;
suppose m=0; then
A2: Y=F.:({<*>A}) by FINSEQ_2:94 .= Im(F,{}) .= {F.{}}
by FUNCT_1:59, A1 .= {{}};
for x,y,d1,d2 being set st x in Y/\(D*) & y in Y/\(D*) &
d1 in D* & d2 in D* & f.(x,d1)=f.(y,d2) holds (x=y & d1=d2)
proof
let x,y,d1,d2 be set; assume
A3: x in Y/\(D*) & y in Y/\(D*) & d1 in D* & d2 in D* & f.(x,d1)=f.(y,d2);
then
x in Y & x in D* & y in Y & y in D* by XBOOLE_0:def 4; then
A4: x={} & y={} by TARSKI:def 1,A2;
reconsider xx=x as Element of D* by A3;
reconsider yy=y as Element of D* by A3;
reconsider d11=d1 as Element of D* by A3;
reconsider d22=d2 as Element of D* by A3;
d11 = xx^d11 by A4,FINSEQ_1:34 .=
f.(yy,d22) by Lm10, A3 .=
{}^d22 by A4,Lm10 .= d22 by FINSEQ_1:34;
hence x=y & d1=d2 by A4;
end;
hence thesis by Def10;
end;
suppose m<>0; then
consider k being Nat such that A5: m=k+1 by NAT_1:6;
set B=(k+1)-tuples_on A; B misses 0-tuples_on A by Lm5; then
B misses {{}} by Lm6; then A6: B\{{}}=B by XBOOLE_1:83;
assume A is D-prefix; then
A7:
(MultPlace(f)).:B is f-unambiguous by Lm19;
F.:B = (F|(B\{{}})).:(B\{{}}) by RELAT_1:129, A6
.= ((MultPlace(f))|B) .: B by A6, Lm24
.= (MultPlace(f)).:B by RELAT_1:129;
hence thesis by A5, A7;
end;
end;
theorem A is D-prefix implies D-multiCat is (m-tuples_on A)-one-to-one
proof
set f=D-concatenation, F=D-multiCat, Z=m-tuples_on A; assume
A1: A is D-prefix;
per cases;
suppose m=0;
then Z=Funcs(Seg 0,A) by Lm7 .= {{}} by FUNCT_5:57;
then F|Z is one-to-one;
hence thesis;
end;
suppose m<>0; then consider k being Nat such that A2: m=k+1 by NAT_1:6;
reconsider kk=k+1 as Element of NAT by ORDINAL1:def 12;
set ZZ=kk-tuples_on A;
(MultPlace(f)) is ZZ-one-to-one by A1, Lm21; then
A3: (MultPlace(f)) | ZZ is one-to-one;
len {} = 0; then not {} in ZZ by FINSEQ_2:132; then {{}}
misses ZZ by ZFMISC_1:50; then ZZ\{{}} = ZZ by XBOOLE_1:83;
then F|Z is one-to-one by Lm24, A3,A2; hence thesis;
end;
end;
theorem (m+1)-tuples_on Y c= Y*\{{}} ::#Th9
proof
reconsider k=m, K=m+1 as Element of NAT by ORDINAL1:def 12;
A1: 0-tuples_on Y misses K-tuples_on Y by Lm5;
K-tuples_on Y c= Y*\ (0-tuples_on Y) by FINSEQ_2:134, XBOOLE_1:86, A1;
hence thesis by Lm6;
end;
theorem m is zero implies m-tuples_on Y={{}} by Lm6; ::#Th10
theorem i-tuples_on Y = Funcs(Seg i,Y) by Lm7;
::#extending FUNCT_2:111
theorem x in m-tuples_on A implies x is FinSequence of A
proof
assume A1: x in m-tuples_on A; then
reconsider p=x as m-element FinSequence by FINSEQ_2:141;
p in Funcs(Seg m,A) by A1, Lm7; then consider f being Function
such that A2: p=f & dom f = Seg m & rng f c= A by FUNCT_2:def 2;
thus x is FinSequence of A by A2, FINSEQ_1:def 4;
end;
definition
let A,X be set;
redefine func chi (A,X) -> Function of X, BOOLEAN; :: redefines chi (FUNCT_3, definition)
coherence
proof
chi(A,X) is Function of X,{{},1} & {{},1}=BOOLEAN; hence thesis;
end;
end;
theorem
(MultPlace(f)).(<*d*>) = d & for x being non empty FinSequence of D holds
(MultPlace(f)).(x^<*d*>) = f.((MultPlace(f)).x, d) by Lm15;
theorem Th14:
for d being non empty Element of D** holds
D-multiCat.d=(MultPlace(D-concatenation)).d
proof
let d be non empty Element of D**; set f=D-concatenation, F=D-multiCat;
not d in {{}} by TARSKI:def 1; then
d in D**\{{}} by XBOOLE_0:def 5; hence
F.d = (F|(D**\{{}})).d by FUNCT_1:49 .= (MultPlace(f)).d by Lm23;
end;
theorem for d1,d2 be Element of (D*) holds D-multiCat.(<*d1,d2*>)=d1^d2
proof
let d1, d2 be Element of D*; set F=D-multiCat, f=D-concatenation, d =
<*d1,d2*>; reconsider dd = <*d1*>^<*d2*> as non empty Element of D**;
A1: F.dd=(MultPlace(f)).(dd) by Th14; thus F.d = f.((MultPlace(f)).<*d1*>,d2)
by Lm15, A1 .= f.(d1,d2) by Lm15 .= d1^d2 by Lm10;
end;
registration
let f,g be FinSequence;
cluster <:f,g:> -> FinSequence-like;
coherence
proof
set m=len f, n=len g, l=min(m,n);
A1:l is Nat by TARSKI:1;
dom <:f,g:>=Seg l by Lm13; hence thesis by A1; end;
end;
registration
let m; let f,g be m-element FinSequence;
cluster <:f,g:> -> m-element;
coherence
proof
set l=min (len f, len g);
A1: len f=m & len g =m by CARD_1:def 7;
reconsider h=<:f,g:> as FinSequence; reconsider ll=l as
Element of NAT by ORDINAL1:def 12; dom h=Seg ll by Lm13; then
len h=ll by FINSEQ_1:def 3; hence thesis by CARD_1:def 7, A1;
end;
end;
registration
let X,Y be set; let f be X-defined Function, g be Y-defined Function;
cluster <:f,g:> -> (X/\Y)-defined for Function;
coherence
proof
reconsider F=dom f as Subset of X;
reconsider G=dom g as Subset of Y;
set h=<:f,g:>;
A1: dom h = G /\ F by FUNCT_3:def 7;
thus thesis by XBOOLE_1:27, A1;
end;
end;
registration
let X be set; let f,g be X-defined Function;
cluster <:f,g:> -> X-defined for Function;
coherence;
end;
registration
let X,Y be set;
let f be total X-defined Function, g be total Y-defined Function;
cluster <:f,g:> -> total for (X/\Y)-defined Function;
coherence
proof
reconsider h=<:f,g:> as (X/\Y)-defined Function;
dom f=X & dom g=Y by PARTFUN1:def 2; then dom h=X/\Y by FUNCT_3:def 7;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let X be set; let f,g be total X-defined Function;
cluster <:f,g:> -> total for X-defined Function;
coherence;
end;
registration
let X,Y be set; let f be X-valued Function, g be Y-valued Function;
cluster <:f,g:> -> [:X,Y:]-valued for Function;
coherence
proof
set h=<:f,g:>; rng h c= [:rng f, rng g:] by FUNCT_3:51;
hence thesis by XBOOLE_1:1;
end;
end;
registration ::#exreg 7
let D; cluster D-valued for FinSequence;
existence
proof set p = the FinSequence of D; take p; thus thesis; end;
end;
registration
let D, m;
cluster m-element D-valued for FinSequence;
existence
proof set p = the m-element FinSequence of D; take p; thus thesis; end;
end;
registration
let X,Y be non empty set;
let f be Function of X,Y; let p be X-valued FinSequence;
cluster f*p -> FinSequence-like;
coherence
proof
rng p c= X; then reconsider pp=p as FinSequence of X by FINSEQ_1:def 4;
f*pp is FinSequence of Y; hence thesis;
end;
end;
registration
let X,Y be non empty set; let m;
let f be Function of X,Y; let p be m-element X-valued FinSequence;
cluster f*p -> m-element for set;
coherence
proof
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
rng p c= X & dom f=X by FUNCT_2:def 1; then
dom (f*p)=dom p by RELAT_1:27 .= Seg (len p) by FINSEQ_1:def 3
.= Seg mm by CARD_1:def 7; then
len (f*p)=mm by FINSEQ_1:def 3;
hence thesis by CARD_1:def 7;
end;
end;
definition
let D,f; let p,q be Element of D*;
func f AppliedPairwiseTo (p,q) -> FinSequence of D equals f*<:p,q:>;
coherence
proof
rng (f*<:p,q:>) c= D; hence thesis by FINSEQ_1:def 4;
end;
end;
registration
let D,f,m; let p,q be m-element Element of D*;
cluster f AppliedPairwiseTo (p,q) -> m-element for set;
coherence;
end;
notation
let D,f; let p,q be Element of D*;
synonym f _\ (p,q) for f AppliedPairwiseTo (p,q);
end;
definition
redefine func INT equals NAT \/ ([:{0},NAT:] \ {[0,0]}); :: redefines INT (INT_1, redefinition) → INT (NUMBERS, definition)
compatibility
proof
INT=NAT \ {[0,0]} \/ ([:{0},NAT:] \ {[0,0]}) by NUMBERS:def 4, XBOOLE_1:42.=
NAT \/ ([:{0},NAT:] \ {[0,0]}) by ZFMISC_1:57, ARYTM_3:32; hence thesis;
end;
end;
theorem Th16: for p being FinSequence st p is Y-valued & p is m-element holds
p in m-tuples_on Y
proof
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
let p be FinSequence; assume p is Y-valued & p is m-element; then
rng p c= Y & len p = mm by CARD_1:def 7;
hence thesis by FINSEQ_2:132;
end;
::##############################Automatizations###############################
::#To automatize things like A/\B c= A
notation
let A,B;
synonym A typed/\ B for A/\B;
end;
definition
let A,B;
redefine func A typed/\ B -> Subset of A; :: redefines typed/\ (FOMODEL0, synonym) → /\ (XBOOLE_0, definition)
coherence by XBOOLE_1:17;
end;
registration
let A,B;
identify A typed/\ B with B typed/\ A;
compatibility;
end;
registration
let A,B;
identify A/\B with A typed/\ B;
compatibility;
end;
definition
let B,A be object;
func A null B -> set equals A;
coherence by TARSKI:1;
end;
registration
let A,B;
reduce A null B to A;
reducibility;
end;
registration
let A; let B be Subset of A;
identify A/\B with B null A;
compatibility by XBOOLE_1:28;
identify B null A with A/\B;
compatibility;
end;
registration
let A,B,C;
cluster (B\A) /\ (A/\C) -> empty for set; ::# Change A/\C to Subset A
coherence
proof
set X=B\A, Y=A/\C; X misses A & Y c= A by XBOOLE_1:79;
hence thesis by XBOOLE_0:def 7, XBOOLE_1:63;
end;
end;
definition
let A,B;
func A typed\ B -> Subset of A equals A\B;
coherence;
end;
registration
let A,B;
identify A\B with A typed\ B;
compatibility;
end;
definition
::# to automatize like: A null B c= A\/B; then A c= A\/B; this is mainly
::# not to have to remember each time what XBOOLE_1 theorem is to be invoked,
::# as long as this file is imported via definitions directive
let A,B;
func A \typed/ B -> Subset of A\/B equals A;
coherence by XBOOLE_1:7;
end;
registration
let A,B;
identify A \typed/ B with A null B;
compatibility;
identify A null B with A \typed/ B;
compatibility;
end;
registration ::# to automate things like X\/(X/\Y)=X
let A; let B be Subset of A;
identify A\/B with A null B;
compatibility by XBOOLE_1:12;
identify A null B with A\/B;
compatibility;
end;
reserve X for set, f for Function;
reserve U1,U2 for non empty set;
Lm26: f c= g implies iter(f,m) c= iter(g,m)
proof
assume A1: f c= g; defpred P[Nat] means iter(f,$1) c= iter(g,$1);
A2: P[0]
proof
A3: iter(f,0)=id field f & iter(g,0)=id field g by FUNCT_7:68;
dom f c= dom g & rng f c= rng g by RELAT_1:11, A1; then
dom f \/ rng f c= dom g \/ rng g by XBOOLE_1:13;
hence thesis by A3, FUNCT_4:3;
end;
A4: for n st P[n] holds P[n+1]
proof
let n; assume P[n]; then
f*iter(f,n) c= g*iter(g,n) by A1, RELAT_1:31; then
iter(f,n+1) c= g*iter(g,n) by FUNCT_7:71; hence thesis by FUNCT_7:71;
end;
P[n] from NAT_1:sch 2(A2,A4); hence thesis;
end;
Lm27: R[*] is_transitive_in field R
proof
set X=field R, S=R[*];
now
let x,y,z be object; assume A1: x in X & y in X & z in X;
assume A2: [x,y] in S & [y,z] in S;
consider p1 being FinSequence such that A3: len p1 >= 1 & p1.1 = x &
p1.(len p1) = y & for i being Nat st i >= 1 & i < len p1 holds
[p1.i,p1.(i+1)] in R by A2, FINSEQ_1:def 17;
consider m being Nat such that A4: len p1=m+1 by NAT_1:6, A3;
consider p2 being FinSequence such that A5: len p2 >= 1 & p2.1 = y &
p2.(len p2) = z & for i being Nat st i >= 1 & i < len p2 holds
[p2.i,p2.(i+1)] in R by A2, FINSEQ_1:def 17;
A6: 1 in dom p2 by FINSEQ_3:25, A5;
reconsider l1=len p1, l2=len p2 as non zero Nat by A3, A5;
reconsider p11=p1|(Seg m) as FinSequence;
set p=p11^p2;
A7: m+0<m+1 by XREAL_1:8;
A8: len p11=m by A7, A4, FINSEQ_1:17;
A9: m+l2>=0+1 by A5, XREAL_1:7;
A10: n>=1 & n<=len p2 implies p.(m+n) = p2.n
proof
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
assume n>=1 & n<=len p2; then n in Seg len p2; then
n in dom p2 by FINSEQ_1:def 3; hence thesis
by FINSEQ_1:def 7, A8;
end;
A11: p.1=x
proof
per cases;
suppose A12: m=0;
thus p.1 = x by A12, A4, A3, A10, A5;
end;
suppose m<>0;
then 0+1<=m by INT_1:7; then 1 in Seg m;
then A13: 1 in dom p11 by A7, A4, FINSEQ_1:17;
hence p.1=p11.1 by FINSEQ_1:def 7 .= x by A3, FUNCT_1:47, A13;
end;
end;
l2 in Seg l2 by A5; then
l2 in dom p2 by FINSEQ_1:def 3; then
A14: p.(len p11+len p2) = z by FINSEQ_1:def 7, A5;
A15: for i being Nat st i>=1 & i<len p holds [p.i,p.(i+1)] in R
proof
let i be Nat; assume
A16: i >= 1 & i < len p; then
A17: i+1>=1 & i>=1 & i<len p by NAT_1:11;
per cases by XXREAL_0:1;
suppose i < m; then A18: i<l1 & i<m & i+1<=m
by INT_1:7, A7, A4, XXREAL_0:2; then
i in Seg m & i+1 in Seg m by A17; then
A19: i in dom p11 & i+1 in dom p11 by A7, A4, FINSEQ_1:17; then
p.i = p11.i & p.(i+1)=p11.(i+1) by FINSEQ_1:def 7; then
p.i = p1.i & p.(i+1)=p1.(i+1) by A19, FUNCT_1:47;
hence [p.i, p.(i+1)] in R by A3, A16, A18;
end;
suppose
A20: i = m;
A21: m in dom p11 by A20, A16, A8, FINSEQ_3:25;
then
A22: p.m = p11.m by FINSEQ_1:def 7 .= p1.m by FUNCT_1:47,A21;
A23: p.(m+1)= p1.(m+1) by
A3, A6, A4, A8, FINSEQ_1:def 7, A5;
thus [p.i, p.(i+1)] in R by A20, A22, A23, A3, A16, A7, A4;
end;
suppose A24: i > m;
then consider j being Nat such that A25: i=m+j by NAT_1:10;
j<>0 by A24, A25; then
A26: j>=0+1 by INT_1:7; then
A27: j>=1 & j+1>=1+0 by XREAL_1:7;
m+j<m+l2 by A25, A16, A8, FINSEQ_1:22; then
A28: j<l2 by XREAL_1:7; then
A29: j<=l2 & j+1<=l2 by INT_1:7;
j in Seg l2 & j+1 in Seg l2 by A29,A27; then
A30: j in dom p2 & j+1 in dom p2 by FINSEQ_1:def 3;
A31: p.i = p2.j by FINSEQ_1:def 7, A30, A25, A8;
A32: p.(i+1)=p.(len p11 +(j+1)) by A25, A8 .=
p2.(j+1) by FINSEQ_1:def 7,A30;
thus [p.i, p.(i+1)] in R by A31, A32, A5,A28,A26;
end;
end;
x in X & z in X & len p >= 1 & p.1=x & p.(len p)=z &
for i being Nat st i>=1 & i<len p holds [p.i,p.(i+1)] in R
by A1,A9, A8, FINSEQ_1:22,A11,A14,A15; hence
[x,z] in S by FINSEQ_1:def 17;
end;
hence thesis by RELAT_2:def 8;
end;
Lm28: field (R[*]) c= field R
proof
set RR=R[*], LH=field RR, RH=field R;
let x be object; assume
A1: x in LH;
per cases by A1, XBOOLE_0:def 3;
suppose x in dom RR; then consider y being object such that
A2: [x,y] in RR by XTUPLE_0:def 12;
thus x in RH by A2, FINSEQ_1:def 17;
end;
suppose x in rng RR; then consider y being object such that
A3: [y,x] in RR by XTUPLE_0:def 13;
thus x in RH by FINSEQ_1:def 17,A3;
end;
end;
Lm29: R[*] is_reflexive_in field R
proof
set RR=R[*], X=field R;
now
let x be object; reconsider p=<*x*> as 1-element FinSequence;
len p=1 & p.1=x by FINSEQ_1:40; then
A1: len p >= 1 & p.1=x & p.(len p)=x &
for i st i>=1 & i<len p holds [p.i, p.(i+1)] in R;
assume x in X; hence [x,x] in RR by A1, FINSEQ_1:def 17;
end;
hence thesis by RELAT_2:def 1;
end;
Lm30: field (R[*]) = field R by LANG1:18,RELAT_1:16,Lm28;
registration
let R be Relation;
cluster R[*] -> transitive for Relation;
coherence
proof
R[*] is_transitive_in field R by Lm27; then
R[*] is_transitive_in field (R[*]) by Lm30;
hence thesis by RELAT_2:def 16;
end;
cluster R[*] -> reflexive for Relation;
coherence
proof
R[*] is_reflexive_in field R by Lm29; then
R[*] is_reflexive_in field (R[*]) by Lm30; hence thesis by RELAT_2:def 9;
end;
end;
Lm31: iter (f,0) c= f[*]
proof
set LH=iter(f,0), RH=f[*];
LH = id (field f) by FUNCT_7:68 .= id (field RH) by Lm30;
hence thesis by RELAT_2:1;
end;
Lm32: iter (f,m+1) c= f[*]
proof
set RH=f[*];
defpred P[Nat] means iter(f,$1+1) c= RH;
A1: P[0]
proof
A2: iter(f,1)=f by FUNCT_7:70;
thus thesis by LANG1:18, A2;
end;
A3: for n st P[n] holds P[n+1]
proof
let n; assume P[n];
then iter (f,n+1) c= RH & f c= RH by LANG1:18; then
A4: (iter (f,n+1))*f c= RH*RH by RELAT_1:31;
RH*RH c= RH by RELAT_2:27; then (iter (f,n+1))*f c= RH by A4;
hence thesis by FUNCT_7:69;
end;
for n holds P[n] from NAT_1:sch 2(A1,A3); hence thesis;
end;
Lm33: iter (f,m) c= f[*]
proof
per cases;
suppose m=0; hence thesis by Lm31; end;
suppose m<>0; then consider n such that A1: m=n+1 by NAT_1:6;
thus thesis by Lm32,A1;
end;
end;
Lm34:
(rng f c= dom f & x in dom f & g.0=x & for i st i < m holds g.(i+1)=f.(g.i))
implies g.m=iter(f,m).x
proof
assume A1: rng f c= dom f & x in dom f; then
A2: x in (dom f \/ rng f) by XBOOLE_0:def 3;
defpred P[Nat] means (g.0=x & for i st i < $1 holds g.(i+1)=f.(g.i))
implies g.($1)=(iter(f,$1)).x;
A3: P[0]
proof
field f = dom f \/ rng f; then
A4: iter(f,0)=id (dom f \/ rng f) by FUNCT_7:68;
assume g.0=x & for i st i < 0 holds g.(i+1)=f.(g.i);
hence thesis by A4, FUNCT_1:17, A2;
end;
A5: for n st P[n] holds P[n+1]
proof
let n; assume
A6: P[n]; assume
A7: g.0=x; assume
A8: for i st i < n+1 holds g.(i+1)=f.(g.i);
A9: for i st i < n holds g.(i+1)=f.(g.i)
proof
let i; assume i<n; then i+0<n+1 by XREAL_1:8; hence thesis by A8;
end;
A10: x in dom (iter (f,n)) by A1, FUNCT_7:74;
n+0<(n+1) by XREAL_1:8; then
g.(n+1)= f.(g.n) by A8 .=
(f*iter(f,n)).x by A10, FUNCT_1:13, A9, A6, A7
.= (iter(f,n+1)).x by FUNCT_7:71; hence thesis;
end;
for n holds P[n] from NAT_1:sch 2(A3,A5); hence thesis;
end;
definition
func plus -> Function of COMPLEX, COMPLEX means
:Def18: for z being Complex holds it.z=z+1;
existence
proof
defpred P[set,set] means for z being Complex st z=$1 holds $2=z+1;
A1: for x be Element of COMPLEX ex zz being Element of COMPLEX st P[x,zz]
proof
let x be Element of COMPLEX;
reconsider z0=x as Complex; reconsider
z1=z0+1 as Element of COMPLEX by XCMPLX_0:def 2; take z1;
thus P[x,z1];
end;
consider f being Function of COMPLEX, COMPLEX such that
A2: for x being Element of COMPLEX holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f;
now
let z be Complex; reconsider
zz=z as Element of COMPLEX by XCMPLX_0:def 2;
z=zz & P[zz,f.zz] by A2; hence f.z=z+1;
end; hence thesis;
end;
uniqueness
proof
let IT1,IT2 be Function of COMPLEX, COMPLEX;
assume A3: for z being Complex holds IT1.z=z+1;
assume A4: for z being Complex holds IT2.z=z+1;
now
let zz be Element of COMPLEX; thus IT1.zz=zz+1 by A3 .=IT2.zz by A4;
end;
hence thesis by FUNCT_2:63;
end;
end;
Lm35: (rng f c= dom f & x in dom f & p.1=x &
for i st i>=1 & i < m+1 holds p.(i+1)=f.(p.i)) implies p.(m+1)=iter(f,m).x
proof
A1: dom plus=COMPLEX by FUNCT_2:def 1; then
reconsider
Z=0 as Element of dom plus by XCMPLX_0:def 2;
reconsider g=p*plus as Function;
A2: for z being Complex holds g.z=p.(z+1)
proof
let z be Complex; reconsider
zz=z as Element of dom plus by XCMPLX_0:def 2, A1;
thus g.z = p.(plus.zz) by FUNCT_1:13 .= p.(z+1) by Def18;
end;
assume A3: rng f c= dom f & x in dom f;
assume p.1=x; then p.(0+1)=x; then A4: g.0=x by A2;
assume A5: for i st i >= 1 & i < m+1 holds p.(i+1)=f.(p.i);
now
let j be Nat; reconsider jz=j as Complex;
assume j<m; then
j+1 >=0+1 & j+1<m+1 by XREAL_1:7,8; then
p.(j+1+1)=f.(p.(j+1)) by A5
.= f.(g.j) by A2;
hence g.(j+1)=f.(g.j) by A2;
end;
then g.m=iter(f,m).x by Lm34,A4,A3; hence p.(m+1)=iter(f,m).x by A2;
end;
Lm36: z in f[*] & rng f c= dom f implies ex n st z in iter (f,n)
proof
set LH=f[*]; assume
A1: z in LH; then consider x,y being object such that
A2: z=[x,y] by RELAT_1:def 1;
consider p being FinSequence such that
A3: len p >= 1 & p.1 = x & p.(len p) = y &
for i being Nat st i >= 1 & i < len p holds [p.i,p.(i+1)] in f
by A2, A1, FINSEQ_1:def 17; assume A4: rng f c= dom f; then
A5: field f = dom f & x in field f
by A2,A1 ,FINSEQ_1:def 17, XBOOLE_1:12;
consider m being Nat such that A6: m+1=len p by A3, NAT_1:6; take m;
for i st i >=1 & i < len p holds p.i in dom f & p.(i+1)=f.(p.i)
proof
let i; assume i >= 1 & i < len p; then A7: [p.i,p.(i+1)] in f by A3; hence
p.i in dom f by XTUPLE_0:def 12; hence p.(i+1)=f.(p.i) by FUNCT_1:def 2, A7;
end; then
A8: m+1 >= 1 & p.1 = x & p.(m+1) = y &
for i being Nat st i >= 1 & i < m+1 holds p.(i+1)=f.(p.i) by A3, A6;
x in dom iter (f,m) & p.(m+1)=iter(f,m).x by A5, A4, A8, Lm35, FUNCT_7:74;
hence z in iter (f,m) by A2, A3, A6, FUNCT_1:1;
end;
Lm37: rng f c= dom f implies
f[*]=union the set of all iter(f,mm) where mm is Element of NAT
proof
set F=the set of all iter (f,mm) where mm is Element of NAT;
set LH=f[*], RH=union F;
now
let x be object; assume x in RH; then consider X being set such that
A1: x in X & X in F by TARSKI:def 4;
consider mm being Element of NAT such that
A2: X=iter(f,mm) by A1;
x in iter (f,mm) & iter (f,mm) c= f[*] by A1, A2, Lm33;
hence x in LH;
end; then
A3: RH c= LH;
assume A4: rng f c= dom f;
now
let x be object; assume x in LH; then consider m such that
A5: x in iter(f,m) by A4, Lm36; reconsider
mm=m as Element of NAT by ORDINAL1:def 12;
x in iter (f,mm) & iter(f,mm) in F by A5; hence
x in RH by TARSKI:def 4;
end; then
A6: LH c= RH;
thus thesis by A3, A6;
end;
theorem rng f c= dom f implies f[*] = ::#Th17
union the set of all iter(f,mm) where mm is Element of NAT by Lm37;
theorem f c= g implies iter(f,m) c= iter(g,m) by Lm26; ::#Th18
registration
let X be functional set;
cluster union X -> Relation-like for set;
::# This is stated elsewhere (CARD_4, COMPUT_1, MSUALG_8,ORDINAL1,
::# TREES_2, WELLFND1), but always in too strong a form
coherence
proof
now
let x be object; assume x in union X; then consider Y such that
A1: x in Y & Y in X by TARSKI:def 4;
thus ex y,z being object st x=[y,z] by A1, RELAT_1:def 1;
end;
hence thesis;
end;
end;
theorem Y c= Funcs(A,B) implies union Y c= [:A,B:] by Lm2; ::#Th19
registration
let Y; let R be Y-valued Relation;
identify Y|`R with R null Y;
compatibility;
end;
registration
let Y;
cluster Y \ Y -> empty for set;
coherence by XBOOLE_1:37;
end;
registration
let D,d;
cluster {(id D).d} \ {d} -> empty for set;
coherence;
end;
registration
let p be FinSequence, q be empty FinSequence;
identify p^q with p null q;
compatibility by FINSEQ_1:34;
identify p null q with p^q;
compatibility;
identify q^p with p null q;
compatibility by FINSEQ_1:34;
identify p null q with q^p;
compatibility;
end;
registration
let Y; let R be Y-defined Relation;
identify R|Y with R null Y;
compatibility;
identify R null Y with R|Y;
compatibility;
end;
theorem Th20: f={[x,f.x] where x is Element of dom f: x in dom f}
proof
set RH={[x,f.x] where x is Element of dom f: x in dom f};
now let z be object; assume
A1: z in f; then consider x, y being object such that
A2: z=[x,y] by RELAT_1:def 1;
reconsider xx=x as Element of dom f by FUNCT_1:1, A2, A1;
z=[xx,f.xx] & xx in dom f by A2, FUNCT_1:1, A1;
hence z in RH;
end; then
A3: f c= RH;
now let z be object; assume
A4: z in RH;
consider x being Element of dom f such that
A5: z=[x,f.x] & x in dom f by A4;
thus z in f by A5, FUNCT_1:1;
end;
then RH c= f; hence thesis by A3;
end;
theorem Th21: for R being total Y-defined Relation holds id Y c= R*(R~)
proof
set X=Y; let R be total X-defined Relation; reconsider f=id X as Function;
A1: f={[x,f.x] where x is Element of dom f: x in dom f} by Th20;
now
let z be object;
assume z in f; then consider x being Element of dom f such that
A2: z=[x,(id X).x] & x in dom (id X) by A1;
x in dom R by A2, PARTFUN1:def 2; then consider y being object such that
A3: [x,y] in R by XTUPLE_0:def 12; [y,x] in R~ by A3, RELAT_1:def 7;
then [x,x] in R*(R~) by A3, RELAT_1:def 8;
hence z in R*(R~) by A2;
end;
hence thesis;
end;
theorem (m+n)-tuples_on D=D-concatenation.: [:m-tuples_on D,n-tuples_on D:]
proof
reconsider m,n as Element of NAT by ORDINAL1:def 12;
set U=D, LH=(m+n)-tuples_on U, M=m-tuples_on U, N=n-tuples_on U,
C=U-concatenation, RH=C.:[:M,N:];
A1: LH=the set of all z^t where z is Tuple of m,U, t is Tuple of n,U
by FINSEQ_2:105;
A2: dom C=[:U*,U*:] by FUNCT_2:def 1;
A3: M c= U* & N c= U* by FINSEQ_2:134;
now
let y be object; assume y in LH; then
consider Tz being Tuple of m,U, Tt being Tuple of n,U such that
A4: y=Tz^Tt by A1;
reconsider zz=Tz as Element of M by FINSEQ_2:131;
reconsider tt=Tt as Element of N by FINSEQ_2:131;
reconsider x=[zz,tt] as Element of [:M,N:];
reconsider xx=x as Element of dom C by A2, A3, ZFMISC_1:96, TARSKI:def 3;
A5: C.:{x} c= RH by RELAT_1:123;
y= C.(Tz,Tt) by A4, Lm10 .= C.x; then
y in {C.xx} by TARSKI:def 1; then y in Im(C,xx) by FUNCT_1:59;
hence y in RH by A5;
end; then
A6: LH c= RH;
now
let y be object; assume y in RH; then consider x being object such that
A7:x in dom C & x in [:M,N:] & y=C.x by FUNCT_1:def 6;
consider z,t being object such that
A8:z in M & t in N & x=[z,t] by ZFMISC_1:def 2, A7;
reconsider zz=z as Element of M by A8; reconsider tt=t as Element of N by A8;
reconsider zzz=zz, ttt=tt as FinSequence of U;
reconsider Tz=zz as Tuple of m, U; reconsider Tt=tt as Tuple of n, U;
y= C.(zzz,ttt) by A7, A8 .= Tz^Tt by Lm10;
hence y in LH by A1;
end;
then RH c= LH; hence thesis by A6;
end;
theorem Th23: for P,Q being Relation holds (P\/Q)"Y = P"Y \/ (Q"Y)
proof
let P,Q be Relation; set R=P\/Q, LH=R"Y, RH=P"Y \/ (Q"Y);
reconsider PP=P null Q, QQ=Q null P as Subset of R;
now
let x be object; assume x in LH; then consider y being object such that
A1: [x,y] in R & y in Y by RELAT_1:def 14;set z=[x,y];
(z in P & y in Y) or(z in Q & y in Y) by XBOOLE_0:def 3, A1; then
x in P"Y or x in Q"Y by RELAT_1:def 14;hence x in RH by XBOOLE_0:def 3;
end; then
A2: LH c= RH; reconsider PX=PP"Y, QX=QQ"Y as Subset of LH
by RELAT_1:144; PX \/ QX c= LH; hence thesis by A2;
end;
Lm38: chi(A,B) = (B --> 0) +* (A/\B --> 1)
proof
set f=B --> 0, g= A/\B --> 1, IT=f+*g;
A1: dom f=B & dom g=A/\B & dom IT=dom f\/dom g by FUNCT_4:def 1;
now
let x be object; assume
A2: x in B; then
A3: x in B & x in dom IT & x in (dom f \/ dom g) by XBOOLE_1:22, A1;
thus x in A implies IT.x=1
proof
assume
A4: x in A; then
A5: x in A/\B by A2, XBOOLE_0:def 4;
x in dom g by A4, A2, XBOOLE_0:def 4;
then IT.x = g.x by A3, FUNCT_4:def 1 .= 1 by FUNCOP_1:7, A5; hence thesis;
end;
thus not x in A implies IT.x={}
proof
assume not x in A; then not x in A/\B; then
not x in dom g; then IT.x = f.x by A3, FUNCT_4:def 1
.= 0 by FUNCOP_1:7, A2; hence thesis;
end;
end;
hence thesis by FUNCT_3:def 3, XBOOLE_1:22, A1;
end;
Lm39: chi(A,B) = (B\A --> 0) +* (A/\B --> 1)
proof
set Z=B\A, O=A/\B, f=B --> 0, g=O --> 1, IT=chi(A,B); reconsider BB=B/\B,
OO=O, ZZ=Z as Subset of B; reconsider OOO=O/\O as Subset of O;
A1: O\/Z=B & dom IT=BB by XBOOLE_1:51, FUNCT_3:def 3;
A2: B/\OO=OO & Z/\O={} & B/\ZZ=ZZ;
A3: (f+*g)|Z = f|Z +* (g|Z) & (f+*g)|O = f|O +* (g|O) by FUNCT_4:71;
A4: f|Z=(B/\Z) --> 0 & g|Z={} --> 1 & f|O=OOO-->0 & g|O=g
by FUNCOP_1:12, A2; then dom (f|O)=OOO & dom (g|O)=O; then
A5: (f|O) +* (g|O) = g|O by FUNCT_4:19;
thus IT=IT|Z +* IT|O by FUNCT_4:70, A1 .= (f +* g)|Z +* IT|O by Lm38 .=
(((B/\Z) --> 0) +* {}) +* g|O by A3, Lm38, A4,A5 .=
(Z --> 0) +* g;
end;
Lm40: chi(A,B)=(B\A --> 0) \/ (A/\B --> 1)
proof
set f=(B\A)-->0, g=(A/\B)-->1; (B\A) /\ (A/\B)={}; then
f tolerates g by FUNCOP_1:87, XBOOLE_0:def 7;
then f+*g=f\/g by FUNCT_4:30; hence thesis by Lm39;
end;
theorem (chi(A,B))"{0}=B\A & (chi(A,B))"{1}=A/\B ::#Th24
proof
set f=B\A --> 0, g=A/\B --> 1, IT=chi(A,B);
A1: 0 in {0} & 1 in {1} & not 1 in {0} & not 0 in {1} by TARSKI:def 1;
A2: f"{1}={} & g"{0}={} by A1, FUNCOP_1:16;
thus IT"{0} =(f\/g)"{0} by Lm40.=f"{0}\/g"{0} by Th23.= B\A
by A1, FUNCOP_1:14, A2;
thus IT"{1} =(f\/g)"{1} by Lm40.=f"{1}\/g"{1} by Th23.= A/\B
by A1,FUNCOP_1:14, A2;
end;
theorem for y being non empty set holds (y=f.x iff x in f"{y}) ::#Th25
proof
let y be non empty set; thus y=f.x implies x in f"{y}
proof
assume y=f.x; then x in dom f & f.x in {y} by FUNCT_1:def 2, TARSKI:def 1;
hence thesis by FUNCT_1:def 7;
end;
assume x in f"{y}; then x in dom f & f.x in {y} by FUNCT_1:def 7;
hence thesis by TARSKI:def 1;
end;
theorem ::#Th26
f is Y-valued & f is FinSequence-like implies f is FinSequence of Y
by Lm1;
registration
let Y; let X be Subset of Y;
cluster X-valued -> Y-valued for Relation;
coherence
by XBOOLE_1:1;
end;
Lm41: for R being total Y-defined Relation ex
f being Function of Y, rng R st f c= R & dom f=Y
proof
set X=Y; let R be total X-defined Relation;
A1: dom R=X by PARTFUN1:def 2;
defpred P[object,object] means [$1,$2] in R;
A2: for x being object st x in X
ex y being object st P[x,y] by XTUPLE_0:def 12, A1;
consider f such that
A3: dom f=X & for x being object st x in X holds P[x,f.x]
from CLASSES1:sch 1(A2);
A4: f={[x,f.x] where x is Element of dom f: x in dom f} by Th20;
A5: now
let z be object;
assume z in f; then consider x being Element of dom f such that
A6: z=[x,f.x] & x in dom f by A4;
thus z in R by A6, A3;
end; then
f c= R; then rng f c= rng R by RELAT_1:11; then
reconsider g=f as Function of X, rng R by A3, RELSET_1:4, FUNCT_2:67;
take g; thus thesis by A5, A3;
end;
Lm42: (dom f c= dom R & R c= f) implies R=f
proof ::# generalizing GRFUNC_1:3
set X=dom f; assume
A1: X c= dom R & R c= f; then
A2: X c= dom R & dom R c= X by RELAT_1:11;
reconsider RR=R as X-defined Relation
by RELAT_1:def 18, A1, RELAT_1:11; reconsider P=RR as total X-defined Relation
by PARTFUN1:def 2, A2, XBOOLE_0:def 10;
consider g being Function of X, rng P such that
A3: g c= P & dom g=X by Lm41;
f c= R by GRFUNC_1:3, A3, A1, XBOOLE_1:1;
hence thesis by A1;
end;
Lm43: for Q being Y-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
let Q be Y-defined Relation; assume Q is total; then
reconsider QQ=Q as total Y-defined Relation; set tQ=QQ~;
assume R is Y-defined; then reconsider RR=R as Y-defined Relation;
assume P*Q*(Q~)*R is Function-like; then reconsider f=P*Q*tQ*R as Function;
A1: f=(P*Q)*(tQ*R) by RELAT_1:36 .=
P*(Q*(tQ*R)) by RELAT_1:36 .= P*(Q*tQ*RR) by RELAT_1:36;
(id Y)*RR c= Q*tQ*RR by RELAT_1:30, Th21; then
A2: RR|Y c= Q*tQ*RR by RELAT_1:65;
assume rng P c= dom R; then
A3: dom (P*R)=dom P by RELAT_1:27;
dom (P*(Q*tQ)) c= dom P & dom ((P*Q*tQ)*R) c= dom (P*Q*tQ) by RELAT_1:25;
then dom (P*Q*tQ) c= dom P & dom f c= dom (P*Q*tQ) by RELAT_1:36; then
dom f c= dom (P*R) by A3;
hence thesis by A2, A1, RELAT_1:29, Lm42;
end;
registration
let A,U;
cluster quasi_total -> total for Relation of A,U;
coherence;
end;
theorem for Q being quasi_total Relation of B, U1, ::#Th27
R being quasi_total Relation of B, U2, P being Relation of
A, B st P*Q*(Q~)*R is Function-like holds P*Q*(Q~)*R=P*R
proof
let Q be quasi_total Relation of B, U1;
let R be quasi_total Relation of B, U2; let P be Relation of A, B;
reconsider QQ=Q as total B-defined Relation;
reconsider RR=R as total B-defined Relation;
A1: dom R=B & rng P c= B by PARTFUN1:def 2;
assume P*Q*(Q~)*R is Function-like; hence thesis by A1, Lm43;
end;
theorem for p,q being FinSequence st p is non empty holds (p^q).1=p.1
proof
let p,q be FinSequence; assume p is non empty; then reconsider
p as non empty FinSequence; set n=len p;
1<=1 & 1<=n by NAT_1:14; then 1 in Seg n; then
1 in dom p by FINSEQ_1:def 3; hence thesis by FINSEQ_1:def 7;
end;
registration ::# to be generalized for p being X-valued, q being Y-valued
let U; let p,q be U-valued FinSequence;
cluster p^q -> U-valued for FinSequence;
coherence;
end;
definition
let X be set;
redefine mode FinSequence of X -> Element of X*; :: redefines FinSequence (FINSEQ_1, definition)
coherence by FINSEQ_1:def 11;
end;
definition ::#def21 1
let U,X;
redefine attr X is U-prefix means for p1, q1, p2, q2 :: redefines -prefix (FOMODEL0, definition)
being U-valued FinSequence st p1 in X & p2 in X & p1^q1=p2^q2 holds
(p1=p2 & q1=q2);
compatibility
proof
set f=U-concatenation, D=U*;
defpred Q[set] means $1 is FinSequence of U;
defpred P[] means 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);
thus X is U-prefix implies P[]
proof
assume X is U-prefix; then
A1: X is f-unambiguous; let p1,q1,p2,q2
be U-valued FinSequence;
A2: Q[p1] & Q[p2] & Q[q1] & Q[q2] by Lm1; assume
p1 in X & p2 in X; then
A3: p1 in X/\D & p2 in X/\D & q1 in U* & q2 in U* by A2,XBOOLE_0:def 4;
assume p1^q1=p2^q2; then f.(p1,q1)=p2^q2 by Th4 .= f.(p2,q2) by Th4; hence
p1=p2 & q1=q2 by A1, A3;
end;
assume A4: P[];
now
let x1, x2, d1, d2 be set; assume
A5: x1 in X/\D & x2 in X/\D & d1 in D & d2 in D;
then reconsider x11=x1, x22=x2, d11=d1, d22=d2 as Element of D;
assume f.(x1,d1)=f.(x2,d2);
then x11^d11=f.(x22,d22) by Th4 .= x22^d22 by Th4;
hence x1=x2 & d1=d2 by A4, A5;
end;
hence thesis by Def10;
end;
end;
registration
let X be set;
cluster -> X-valued for Element of X*;
coherence;
end;
registration
let U, m; let X be U-prefix set;
cluster (U-multiCat).:(m-tuples_on X) -> U-prefix for set;
coherence by Th7;
end;
theorem Th29:
(X \+\ Y={} iff X=Y) & (X\Y={} iff X c= Y) &
for x being object holds ({x}\Y={} iff x in Y)
proof
set Z=X \+\ Y, Z1=X\Y, Z2=Y\X;
thus Z={} implies X=Y
proof
assume Z={}; then Z1={} & Z2={}; then
X c= Y & Y c= X by XBOOLE_1:37; hence thesis;
end;
thus X=Y implies Z={};
thus X\Y={} iff X c= Y by XBOOLE_1:37;
thus thesis by ZFMISC_1:60;
end;
registration
let P;
cluster P \ [:dom P, rng P:] -> empty;
coherence by RELAT_1:7, Th29;
end;
registration
let X,Y,Z be set;
cluster X\/Y\/Z \+\ (X\/(Y\/Z)) -> empty;
coherence by XBOOLE_1:4, Th29;
end;
registration
let x;
cluster (id {x}) \+\ {[x,x]} -> empty for set;
coherence proof id {x} = {[x,x]} by SYSREL:13; hence thesis; end;
end;
registration
let x,y;
cluster (x.-->y) \+\ {[x,y]} -> empty for set;
coherence proof x.-->y={[x,y]} by ZFMISC_1:29; hence thesis; end;
end;
registration
let x;
cluster (id {x}) \+\ (x.-->x) -> empty for set;
coherence
proof
(id {x}) \+\ {[x,x]} = {} & (x.-->x) \+\ {[x,x]}={};
hence thesis by Th29;
end;
end;
theorem x in D*\{{}} iff (x is D-valued FinSequence & x is non empty)
proof
(x is D-valued FinSequence & x is non empty) iff
(x is non empty FinSequence of D) by Lm1; hence thesis by Th5;
end;
reserve f for BinOp of D;
theorem Th31:
(MultPlace(f)).(<*d*>) = d & for x being D-valued FinSequence st
x is non empty holds (MultPlace(f)).(x^<*d*>) = f.((MultPlace(f)).x, d)
proof
set F=MultPlace f; thus F.<*d*>=d by Lm15;
let x be D-valued FinSequence; assume x is non empty; then
reconsider xx=x as non empty FinSequence of D by Lm1;
F.(xx^<*d*>)=f.(F.xx,d) by Lm15; hence thesis;
end;
reserve a,a1,a2,b,b1,b2,A,B,C,X,Y,Z,x,x1,x2,y,y1,y2,z for set,
U,U1,U2,U3 for non empty set, u,u1,u2 for Element of U,
P,Q,R for Relation, f,f1,f2,g,g1,g2 for Function,
k,m,n for Nat, kk,mm,nn for Element of NAT, m1, n1 for non zero Nat,
p, p1, p2 for FinSequence, q, q1, q2 for U-valued FinSequence;
registration
let p,x,y;
cluster p +~ (x,y) -> FinSequence-like;
coherence
proof
set IT=p+~(x,y); dom IT=dom p by FUNCT_4:99 .= Seg (len p)
by FINSEQ_1:def 3; hence thesis;
end;
end;
definition
let x,y,p;
func (x,y)-SymbolSubstIn p -> FinSequence equals p +~ (x,y);
coherence;
end;
registration
let x,y,m; let p be m-element FinSequence;
cluster (x,y)-SymbolSubstIn p -> m-element for FinSequence;
coherence
proof
set IT=(x,y)-SymbolSubstIn p;
reconsider mm=m as Element of NAT by ORDINAL1:def 12; dom IT = dom p
by FUNCT_4:99.= Seg len p by FINSEQ_1:def 3 .= Seg mm by CARD_1:def 7;
then len IT=mm by FINSEQ_1:def 3; hence thesis by CARD_1:def 7;
end;
end;
registration
let x, U, u; let p be U-valued FinSequence;
cluster (x,u)-SymbolSubstIn p -> U-valued for FinSequence;
coherence;
end;
definition
let X,x,y; let p be X-valued FinSequence;
redefine func (x,y)-SymbolSubstIn p equals :: redefines -SymbolSubstIn (FOMODEL0, definition)
(id X +* (x,y))*p;
compatibility
proof rng p c= X; hence thesis by FUNCT_7:116; end;
end;
definition
let U, x, u, q;
redefine func (x,u)-SymbolSubstIn q -> FinSequence of U; :: redefines -SymbolSubstIn (FOMODEL0, definition)
coherence by Lm1;
end;
Lm44:
(u=u1 implies (u1,x2)-SymbolSubstIn <*u*>=<*x2*>) &
(u<>u1 implies (u1,x2)-SymbolSubstIn <*u*>=<*u*>)
proof
set X=U, s=u, s1=u1, s2=x2, w=<*s*>, IT=(s1,s2)-SymbolSubstIn w, f1=1.-->s1,
f2=1.-->s2,f=1.-->s,subst=s1 .--> s2, I=id X, w1=<*s1*>, w2=<*s2*>;
A1: w \+\ f={} & w2 \+\ f2={} & w1 \+\ f1={}; then
A2: w=f & w2=f2 & w1=f1 by Th29;
A3: dom subst={s1} & dom f2={1} & dom f1={1} & dom f={1}
& rng f={s} by FUNCOP_1:8; s1 in {s1} by TARSKI:def 1; then
A4: subst.s1=s2 by FUNCOP_1:7;
A5: IT = w +* (subst*f) by A1, Th29;
thus s=s1 implies IT = w2
proof
assume A6: s=s1; then s in dom subst by TARSKI:def 1; then
IT = f +* f2 by A6, A2, A4, FUNCOP_1:17 .=
w2 by A2, FUNCT_4:19, A3; hence IT=w2;
end;
assume s<>s1; then
subst*f={} by A3, ZFMISC_1:11, RELAT_1:44;
hence thesis by A5;
end;
Lm45: (x, u)-SymbolSubstIn (q1^q2) =
((x, u)-SymbolSubstIn q1) ^ (x, u)-SymbolSubstIn q2
proof
set s1=x, s2=u, w1=q1, w2=q2, w=w1^w2, IT1=(s1, s2)-SymbolSubstIn w1,
IT2=(s1, s2)-SymbolSubstIn w2,IT=(s1, s2)-SymbolSubstIn w,f=s1.-->s2,I=id U;
reconsider g=I+*(s1,s2) as Function of U, U;
reconsider w11=w1, w22=w2, ww=w as FinSequence of U by Lm1; thus
IT = (g*w11) ^ (g*w22) by FINSEQOP:9 .= IT1 ^ IT2;
end;
definition ::#def24 1
let U, x, u; set D=U*;
deffunc F(Element of U*)=(x,u)-SymbolSubstIn $1;
func x SubstWith u -> Function of U*, U* means :Def22:
for q holds it.q = (x, u)-SymbolSubstIn q;
existence
proof
consider f being Function of D,D such that
A1: for x being Element of D holds f.x=F(x) from FUNCT_2:sch 4;
take f;
now
let q; reconsider qq=q as FinSequence of U by Lm1;
reconsider qqq=qq as Element of D; f.qqq=F(qqq) by A1;
hence f.q = (x,u)-SymbolSubstIn q;
end;
hence thesis;
end;
uniqueness
proof
let IT1, IT2 be Function of D, D; assume
A2: for q holds IT1.q = (x, u)-SymbolSubstIn q; assume
A3: for q holds IT2.q = (x, u)-SymbolSubstIn q;
now let w be Element of D; thus IT1.w=F(w) by A2 .= IT2.w by A3; end;
hence thesis by FUNCT_2:63;
end;
end;
Lm46: (u=u1 implies (u1 SubstWith u2).<*u*>=<*u2*>) &
(u<>u1 implies (u1 SubstWith u2).<*u*>=<*u*>)
proof
set e=u1 SubstWith u2, es=(u1,u2)-SymbolSubstIn <*u*>;
es=e.<*u*> by Def22; hence thesis by Lm44;
end;
registration
let U, x, u;
cluster x SubstWith u -> FinSequence-yielding for Function;
coherence
proof
set e=x SubstWith u;
for y being object st y in dom e holds e.y is FinSequence;
hence thesis by PRE_POLY:def 3;
end;
end;
Lm47: (x SubstWith u).(q1^q2)=((x SubstWith u).q1)^((x SubstWith u).q2)
proof
set e=x SubstWith u, w1=q1, w2=q2, w=w1^w2, W1=(x,u)-SymbolSubstIn w1,
W2=(x,u)-SymbolSubstIn w2, W=(x,u)-SymbolSubstIn w;
e.w1=W1 & e.w2=W2 & e.w=W by Def22; hence thesis by Lm45;
end;
registration
let U,x,u,m; let p be U-valued m-element FinSequence;
cluster (x SubstWith u).p -> m-element for FinSequence;
coherence
proof (x SubstWith u).p=(x,u)-SymbolSubstIn p by Def22; hence thesis; end;
end;
registration
let U,x,u; let e be empty set;
cluster (x SubstWith u).e -> empty for set;
coherence
proof
rng e = U/\{};
then reconsider ee=e as U-valued 0-element FinSequence by RELAT_1:def 19;
(X SubstWith u).ee is 0-element; hence thesis;
end;
end;
registration
let U;
cluster U-multiCat -> FinSequence-yielding for Function;
coherence
proof
set f=U-multiCat;
for x being object st x in dom f holds f.x is FinSequence;
hence thesis by PRE_POLY:def 3;
end;
end;
registration
let U,m1,n; let p be (m1+n)-element U-valued FinSequence;
cluster {p.m1} \ U -> empty for set;
coherence
proof
consider m such that A1: m1=m+1 by NAT_1:6;
set IT={p.m1}\U, M=m1+n; p in M-tuples_on U by Th16; then
p is Element of Funcs(Seg M,U) by Lm7; then
reconsider f=p as Function of Seg M, U; 1<=m+1 & m+1<=m+1+n by NAT_1:11;
then reconsider ms=m1 as Element of Seg M by A1, FINSEQ_1:1;
f.ms in U;
hence thesis by ZFMISC_1:60;
end;
end;
registration
let U,m,n; let p be (m+1+n)-element Element of U*;
cluster {p.(m+1)} \ U -> empty for set;
coherence;
end;
registration
let x;
cluster <*x*> \+\ {[1,x]} -> empty for set;
coherence;
end;
registration ::#funcreg39 1
let m; let p be (m+1)-element FinSequence;
cluster p|Seg m ^ <*p.(m+1)*> \+\ p -> empty for set;
coherence
proof
set q=p|Seg m; len p=m+1 by CARD_1:def 7; then
p=q^<*p.(m+1)*> by FINSEQ_3:55; hence thesis;
end;
end;
registration
let m,n; let p be (m+n)-element FinSequence;
cluster p|Seg m -> m-element for FinSequence;
coherence
proof
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
set q=p|(Seg m), N=m+n; m + 0 <= N & len p=N by XREAL_1:7, CARD_1:def 7;
then Seg m c= Seg N & dom p = Seg N by FINSEQ_1:5, def 3; then
reconsider M=Seg m as Subset of dom p;
dom q = M null (dom p) by RELAT_1:61 .= Seg mm;
then len q=mm by FINSEQ_1:def 3; hence thesis by CARD_1:def 7;
end;
end;
registration
cluster {{}}-valued -> empty-yielding for Relation;
coherence;
cluster empty-yielding -> {{}}-valued for Relation;
coherence;
end;
theorem Th32: U-multiCat.x=(MultPlace(U-concatenation)).x
proof
set D=U*, f=U-concatenation, F=MultPlace f, G=U-multiCat;
set g = {} .--> {};
reconsider g as {{}}-valued Function;
dom f=[:D,D:] & dom F=D*\{{}} & dom G=D* by FUNCT_2:def 1; then
reconsider dF=dom F as Subset of dom G;
per cases;
suppose x in dom F; hence G.x=F.x by FUNCT_4:13; end;
suppose A1: not x in dom F; hence G.x = g.x by FUNCT_4:11 .=
F.x by FUNCT_1:def 2, A1; end;
end;
theorem Th33: p is U*-valued implies
(U-multiCat).(p^<*q*>) = (U-multiCat.p)^q
proof
set C=U-multiCat, g=U-concatenation, G=MultPlace g;
reconsider qq=q as FinSequence of U by Lm1;
per cases;
suppose p is empty; then reconsider e=p as empty set;
A1: (C.e)^q=q & C.(e^<*q*>) = C.(<*q*>);
C.(e^<*q*>)=G.(<*qq*>) by Th32 .= qq by Th31; hence thesis
by A1; end;
suppose A2: not p is empty; assume p is U*-valued; then reconsider
pp=p as non empty U*-valued FinSequence by A2;
reconsider ppp=pp as non empty FinSequence of U* by Lm1;
C.(pp^<*q*>)= G.(pp^<*qq*>) by Th32 .= g.(G.pp, qq) by Th31 .=
g.(C.ppp, q) by Th32 .= (C.p) ^ q by Th4; hence thesis;
end;
end;
Lm48: p is U*-valued implies
(x SubstWith u).(U-multiCat.p)=U-multiCat.((x SubstWith u)*p)
proof
set S=U, C=S-multiCat, SS=U, strings=U*, e=x SubstWith u, m=len p,
F=U-firstChar, FF=strings-firstChar, g=SS-concatenation, G=MultPlace g;
defpred P[Nat] means for p being $1-element strings-valued FinSequence
holds e.(C.p)=C.(e*p);
A1: P[0];
A2: for n st P[n] holds P[n+1]
proof
let n; set n1=n+1; assume
A3: P[n]; let p be n1-element strings-valued FinSequence;
reconsider q=p|Seg n as n-element strings-valued FinSequence;
reconsider qq=q as n-element FinSequence of strings by Lm1;
p is (n1+0)-element; then {p.n1}\strings={}; then
reconsider z=p.n1 as Element of strings by ZFMISC_1:60;
reconsider f=e.z as Element of SS*; q^<*z*> \+\ p ={}; then
A4: q^<*z*>=p by Th29;
C.(e*p)= C.((e*qq)^<*f*>) by FINSEQOP:8,A4 .=
(C.(e*qq))^f by Th33 .= (e.(C.qq)) ^ f by A3 .= e.((C.qq)^z) by Lm47
.= e.(C.p) by Th33, A4; hence thesis;
end;
A5: for n holds P[n] from NAT_1:sch 2(A1, A2);
assume p is U*-valued; then
reconsider pp=p as m-element U*-valued FinSequence by CARD_1:def 7;
e.(C.pp)=C.(e*pp) by A5; hence thesis;
end;
registration
let Y; let X be Subset of Y; let R be total Y-defined Relation;
cluster R|X -> total for X-defined Relation;
coherence
proof
set IT=R|X; dom R=Y by PARTFUN1:def 2; then
A1: dom IT=X null Y by RELAT_1:61;
reconsider ITT=IT as X-defined Relation;
thus thesis by A1, PARTFUN1:def 2;
end;
end;
theorem (u=u1 implies (u1,x2)-SymbolSubstIn <*u*>=<*x2*>) &
(u<>u1 implies (u1,x2)-SymbolSubstIn <*u*>=<*u*>) ::#Th34
by Lm44;
theorem (u=u1 implies (u1 SubstWith u2).<*u*>=<*u2*>) &
(u<>u1 implies (u1 SubstWith u2).<*u*>=<*u*>) ::#Th35
by Lm46;
theorem (x SubstWith u).(q1^q2)=((x SubstWith u).q1)^((x SubstWith u).q2)
by Lm47;
theorem p is U*-valued implies ::#Th37
(x SubstWith u).(U-multiCat.p)=U-multiCat.((x SubstWith u)*p)
by Lm48;
theorem (U-concatenation).:(id (1-tuples_on U)) =
the set of all <*u,u*> where u is Element of U ::#Th38
proof
set f=U-concatenation, U1=1-tuples_on U, D=id U1, U2=2-tuples_on U, A=f.:D,
B= the set of all <*u,u*> where u is Element of U;
D c= [:U1, U1:] & U1 c= U* by FINSEQ_2:142; then
[:U1, U1:] c= [:U*, U*:] by ZFMISC_1:96; then
reconsider DD=D as Subset of [:U*, U*:] by XBOOLE_1:1;
A1: U1=the set of all <*u*> where u is Element of U by FINSEQ_2:96;
A2: dom D=U1 & dom f=[:U*, U*:] by FUNCT_2:def 1; then
A3: D={[x,D.x] where x is Element of U1: x in U1} by Th20;
now
let y be object; assume y in A; then consider x being object such that
A4: x in dom f & x in D & y=f.x by FUNCT_1:def 6;
consider p being Element of U1 such that
A5: x=[p,D.p] & p in U1 by A4, A3; consider u being Element of U such that
A6: p=<*u*> by A5, A1;
reconsider pp=p as FinSequence of U;
y=f.(pp,pp) by A4, A5; then
y = <*u,u*> by Th4, A6; hence y in B;
end; then
A7: A c= B;
now
let y be object; assume y in B; then consider u being Element of U such that
A8: y=<*u,u*>; reconsider p=<*u*> as Element of
U1 by FINSEQ_2:98; reconsider pp=p as FinSequence of U;
[p,D.p]=[p,p] & p in U1; then [p,p] in D by A3; then
reconsider dd=[p,p] as Element of D;
A9: dd in DD null [:U*, U*:]; y = f.(pp,pp) by A8, Th4 .= f.dd;
hence y in f.:D by A9, A2, FUNCT_1:def 6;
end;
then B c= A; hence thesis by A7;
end;
registration
let f,U,u;
cluster ((f|U).u) \+\ f.u -> empty for set;
coherence proof (f|U).u=f.u by FUNCT_1:49; hence thesis; end;
end;
registration ::#funcreg43 1
let f,U1,U2; let u be Element of U1, g be Function of U1,U2;
cluster (f*g).u \+\ f.(g.u) -> empty for set;
coherence
proof
dom g=U1 by FUNCT_2:def 1; then
(f*g).u=f.(g.u) by FUNCT_1:13; hence thesis;
end;
end;
registration
cluster non negative -> natural for Integer;
coherence
proof
let i be Integer; assume i is non negative;
then i in NAT by INT_1:3; hence thesis;
end;
end;
registration
let x,y be Real;
cluster max(x,y)-x -> non negative for ExtReal;
coherence
proof
set z=max(x,y);
x+(-x)<=z+(-x) by XREAL_1:6, XXREAL_0:25;
then 0<=z-x; hence thesis;
end;
end;
theorem x is boolean implies (x=1 iff x<>0) ::#Th38
by XBOOLEAN:def 3;
registration
let Y; let X be Subset of Y;
cluster X\Y -> empty for set;
coherence by XBOOLE_1:37;
end;
registration
let x,y be object;
cluster {x}\{x,y} -> empty for set;
coherence proof x in {x,y} by TARSKI:def 2;hence thesis by ZFMISC_1:60;end;
end;
registration
let x,y be set;
cluster ([x,y]`1) \+\ x -> empty for set;
coherence;
end;
registration
let x,y;
cluster ([x,y]`2) \+\ y -> empty for set;
coherence;
end;
registration
let n be positive Nat;
let X be non empty set;
cluster n-element for Element of X*\{{}};
existence
proof
consider m such that
A1: n=m+1 by NAT_1:6; set x = the Element of (m+1)-tuples_on X;
reconsider mm=m+1 as Element of NAT by ORDINAL1:def 12;
A2: x in mm-tuples_on X & mm-tuples_on X c= X* by FINSEQ_2:134;
not x in {{}}; then
reconsider xx=x as Element of X*\{{}} by A2, XBOOLE_0:def 5;
take xx; thus thesis by A1;
end;
end;
registration
let m1;
cluster (m1+0)-element -> non empty for FinSequence;
coherence;
end;
registration
let R,x;
cluster R null x -> Relation-like for set;
coherence;
end;
registration
let f be Function-like set; let x;
cluster f null x -> Function-like for set;
coherence;
end;
registration
let p be FinSequence-like Relation; let x;
cluster p null x -> FinSequence-like for Relation;
coherence;
end;
registration
let p,x;
cluster p null x -> (len p)-element for FinSequence;
coherence by CARD_1:def 7;
end;
registration
::#need card (non empty) -> non empty from CARD_1 (len being synonym of card)
let p be non empty FinSequence;
cluster len p -> non zero for number;
coherence;
end;
registration
let R be Relation, X be set;
cluster R|X -> X-defined for Relation;
coherence
by RELAT_1:58;
end;
registration
let x; let e be empty set;
cluster e null x -> empty for set;
coherence;
end;
registration
let X; let e be empty set;
cluster e null X -> X-valued for Relation;
coherence
proof rng e=rng e /\ X; hence thesis; end;
end;
registration
let Y be non empty FinSequence-membered set;
cluster Y-valued -> FinSequence-yielding for Function;
coherence
proof
let f; assume f is Y-valued; then
A1: rng f c= Y;
now
let x be object;
assume A2: x in dom f; then reconsider D=dom f as non empty set;
reconsider xx=x as Element of D by A2;
reconsider ff=f as Function of D, Y by FUNCT_2:2, A1;
ff.xx in Y; hence f.x is FinSequence;
end;
hence thesis by PRE_POLY:def 3;
end;
end;
registration
let X,Y;
cluster -> FinSequence-yielding for Element of Funcs (X,Y*);
coherence;
end;
theorem Th40: f is X*-valued implies f.x in X*
proof
assume f is X*-valued; then
A1: rng f c= X*;
per cases;
suppose A2: x in dom f; then reconsider D=dom f as non empty set;
reconsider e=x as Element of D by A2;
reconsider ff=f as Function of D, X* by FUNCT_2:2, A1;
ff.e is Element of X*; hence thesis;
end;
suppose not x in dom f; then f.x = {} by FUNCT_1:def 2;
hence thesis by FINSEQ_1:49;
end;
end;
registration
let m,n; let p be m-element FinSequence;
cluster p null n -> (Seg (m+n))-defined for Relation;
coherence
proof
dom p= Seg len p by FINSEQ_1:def 3; then
m+0<=m+n & dom p = Seg m by CARD_1: def 7, XREAL_1:6;
hence thesis by FINSEQ_1:5;
end;
end;
Lm49: 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
let p1,p2,q1,q2 be FinSequence; set P=p1^p2, Q=q1^q2; assume
p1 is m-element & q1 is m-element; then reconsider x=p1, y=q1 as
m-element FinSequence;
Seg (len p1)=dom p1 & Seg (len q1)=dom q1 by FINSEQ_1:def 3; then
A1: dom x=Seg m & dom y=Seg m by CARD_1:def 7; assume
A2: P=Q; x null 0 is (Seg(m+0))-defined & y null 0 is (Seg(m+0))-defined;
then reconsider p11=p1, q11=q1 as (Seg m)-defined FinSequence;
A3: p11 null (Seg m) = (q11^q2)|(Seg m) by A1,A2,FINSEQ_6:11
.= q11 null (Seg m) by A1, FINSEQ_6:11;
hence p1=q1; thus p2=q2 by A3, A2, FINSEQ_1:33;
end;
registration
let m,n; let p be m-element FinSequence; let q be n-element FinSequence;
cluster p^q -> (m+n)-element for FinSequence;
coherence;
end;
theorem for p1,p2,q1,q2 being FinSequence st p1 is m-element & ::#Th41
q1 is m-element & (p1^p2=q1^q2 or p2^p1=q2^q1) holds (p1=q1 & p2=q2)
proof ::#weakening FINSEQ_1:33
let p1,p2,q1,q2 be FinSequence;
set m1=len p1, m2=len p2, n1=len q1, n2=len q2; assume p1 is m-element
& q1 is m-element; then reconsider p11=p1, q11=q1 as m-element
FinSequence; reconsider p22=p2 null p2 as m2-element FinSequence;
reconsider q22=q2 null q2 as n2-element FinSequence;
set PA=p11^p22, PB=p22^p11, QA=q11^q22, QB=q22^q11;
A1: len PA=m+m2 & len PB=m2+m & len QA=m+n2 & len QB=n2+m by CARD_1:def 7;
assume
A2: p1^p2=q1^q2 or p2^p1=q2^q1; then
A3: PA=QA or PB=QB;
reconsider q22 as m2-element FinSequence by A2, A1;
p22 is m2-element & q22 is m2-element;
hence thesis by A3, Lm49;
end;
theorem (U-multiCat.x is U1-valued & x in U**) implies
x is FinSequence of (U1*) ::#Th42
proof
set C=U-multiCat, f=U-concatenation, F=MultPlace f, D=U*;
{} null (U*) is U*-valued Relation; then
reconsider e={} as U*-valued FinSequence;
defpred P[Nat] means for p being ($1+1)-element U*-valued FinSequence
st C.p is U1-valued holds p is U1*-valued;
A1: P[0]
proof
let p be (0+1)-element U*-valued FinSequence;
reconsider ppp=p as (1+0)-element U*-valued FinSequence;
{ppp.1} \ U* ={}; then reconsider
p1=p.1 as Element of U* by ZFMISC_1:60;
A2: len p=1 by CARD_1:def 7; p={}^<*p.1*> by A2, FINSEQ_1:40; then
A3: C.p=(C.e)^(p1) by Th33 .= {}^p.1 .= p.1;
p is 1-element FinSequence of U* by Lm1; then
reconsider pp=p as 1-element Element of U**;
assume C.p is U1-valued; then reconsider u1=C.pp as FinSequence of U1
by Lm1; u1=p.1 by A3; then reconsider q=p.1 as Element of U1*;
<*q*> is FinSequence of U1*; hence thesis by A2, FINSEQ_1:40;
end;
A4: for n st P[n] holds P[n+1]
proof
let n; reconsider NN =
n+1 as non zero Element of NAT by ORDINAL1:def 12; assume
A5: P[n]; let p be (n+1+1)-element U*-valued FinSequence; assume
A6: C.p is U1-valued;
reconsider pp=p null p as (n+2)-element U*-valued FinSequence;
reconsider ppp=pp as (NN+1)-element U*-valued FinSequence;
reconsider pppp=ppp as (NN+1+0)-element U*-valued FinSequence;
reconsider p1=ppp|(Seg NN) as NN-element U*-valued FinSequence;
{pppp.(NN+1)} \ U* = {}; then
reconsider u=ppp.(NN+1) as Element of U* by ZFMISC_1:60;
A7: ppp \+\ (p1 ^ <*ppp.(NN+1)*>)={}; then
p=p1^<*u*> by Th29; then
A8: C.p=(C.p1)^u by Th33; then rng (C.p) c= U1 &
rng (C.p1) c= rng (C.p) by A6, FINSEQ_1:29; then
reconsider q= C.p1 as
U1-valued FinSequence by XBOOLE_1:1, RELAT_1:def 19; q is U1-valued; then
reconsider p11=p1 as NN-element U1*-valued FinSequence by A5;
rng u c= rng (C.p) & rng (C.p) c= U1 by A8, FINSEQ_1:30, A6;
then u is U1-valued by XBOOLE_1:1; then
u is FinSequence of U1 by Lm1; then reconsider uu=u as Element of U1*;
p11^<*uu*> is U1*-valued; hence thesis by A7, Th29;
end;
A9: for n holds P[n] from NAT_1:sch 2(A1,A4); assume
A10: C.x is U1-valued & x in U**;
per cases;
suppose x is empty; then reconsider xx=x as empty set;
xx null (U1*) is (U1*)-valued FinSequence;
hence thesis by Lm1;
end;
suppose not x is empty; then reconsider xx=x as non empty U*-valued
FinSequence by A10; consider m such that
A11: len xx=m+1 by NAT_1:6; xx null {} is (m+1)-element by A11; then reconsider
xxx=xx as (m+1)-element U*-valued FinSequence;
xxx is U1*-valued by A10, A9; hence thesis by Lm1;
end;
end;
registration
let U;
cluster total for reflexive Relation of U;
existence
proof
set R = the total symmetric transitive reflexive Relation of U;
take R; thus thesis;
end;
end;
registration
let m;
cluster (m+1)-element -> non empty for FinSequence;
coherence;
end;
registration
let U,u;
cluster (id U).u \+\ u -> empty for set;
coherence;
end;
registration
let U; let p be U-valued non empty FinSequence;
cluster {p.1}\U -> empty for set;
coherence
proof
consider m such that A1: len p=m+1 by NAT_1:6; reconsider pp=p as
(1+m)-element
U-valued FinSequence by A1, CARD_1:def 7; {pp.1}\U = {}; hence thesis;
end;
end;
theorem (x1=x2 implies f+*(x1.-->y1)+*(x2.-->y2)=f+*(x2.-->y2)) &
(x1<>x2 implies f+*(x1.-->y1)+*(x2.-->y2)=f+*(x2.-->y2)+*(x1.-->y1)) ::#Th43
proof
set f1=x1.-->y1, f2=x2.-->y2, LH=f+*f1+*f2;
hereby
assume x1=x2; then {x1} = dom f2;
then dom f1 = dom f2; then
f1+*f2 = f2 by FUNCT_4:19; hence LH=f+*f2 by FUNCT_4:14;
end;
assume x1<>x2; then {x1} misses {x2} by ZFMISC_1:11; then
f1 tolerates f2 by FUNCOP_1:87; then f+*(f1+*f2)=f+*(f2+*f1) by FUNCT_4:34 .=
f+*f2+*f1 by FUNCT_4:14; hence LH=f+*f2+*f1 by FUNCT_4:14;
end;
registration
let X,U;
cluster U-valued total for X-defined Function;
existence
proof set f = the total PartFunc of X,U; take f; thus thesis; end;
end;
registration
let X, U; let P be U-valued total X-defined Relation;
let Q be total U-defined Relation;
cluster P*Q -> total for X-defined Relation;
coherence
proof
rng P c= U & dom Q=U by PARTFUN1:def 2; then
dom (P*Q)=dom P by RELAT_1:27 .= X
by PARTFUN1:def 2; hence thesis by PARTFUN1:def 2;
end;
end;
theorem ::#Th44
p^p1^p2 is X-valued implies (p2 is X-valued & p1 is X-valued & p is X-valued)
proof
set q=p^p1^p2; assume q is X-valued; then rng q c= X & rng (p^p1) c= rng q
& rng p2 c= rng q by FINSEQ_1:29,30; then rng p2 c= X
& rng p c= rng (p^p1) & rng p1 c= rng (p^p1) & rng (p^p1) c= X by
FINSEQ_1:29, 30;
hence thesis by XBOOLE_1:1;
end;
registration
let X; let R be Relation;
cluster R null X -> (X \/ rng R)-valued for Relation;
coherence
proof rng R null X c= rng R \/ X; hence thesis; end;
end;
registration
let X,Y be functional set;
cluster X\/Y -> functional;
coherence
proof
now
let x be object;
assume x in X\/Y; then x in X or x in Y by XBOOLE_0:def 3;
hence x is Function;
end;
hence thesis by FUNCT_1:def 13;
end;
end;
registration
cluster FinSequence-membered -> finite-membered for set;
coherence
proof
let X; assume
A1: X is FinSequence-membered;
for x st x in X holds x is finite by A1;
hence thesis by FINSET_1:def 6;
end;
end;
definition
let X be functional set;
func SymbolsOf X -> set equals
union {rng x where x is Element of X\/{{}}: x in X};
coherence;
end;
Lm50: for X being functional set st X is finite &
X is finite-membered holds SymbolsOf X is finite
proof
let X be functional set; set Y=X\/{{}},
F={rng y where y is Element of Y: y in X}; assume
A1: X is finite;
F is finite from FRAENKEL:sch 21(A1); then reconsider
FF=F as finite set;
assume X is finite-membered; then reconsider YY=Y as
finite-membered set;
now
let y; assume y in F; then consider x being Element of Y such that
A2: y=rng x & x in X; reconsider xx=x as Element of YY; xx is finite;
hence y is finite by A2;
end; then reconsider FFF=FF as finite-membered finite set by FINSET_1:def 6;
union FFF is finite; hence thesis;
end;
registration
cluster trivial for FinSequence-membered non empty set;
existence
proof set U=the non empty set; take IT={the Element of U*}; thus thesis; end;
end;
registration
let X be functional finite finite-membered set;
cluster SymbolsOf X -> finite for set;
coherence by Lm50;
end;
registration
let X be finite FinSequence-membered set;
cluster SymbolsOf X -> finite for set;
coherence;
end;
theorem Th45: SymbolsOf {f} = rng f ::#Th45
proof
set P=f, X={P}, F={rng x where x is Element of X\/{{}}: x in X}, LH=union F,
RH=rng P;
X null {{}} c= X\/{{}}; then reconsider XX=X as Subset of X\/{{}};
reconsider PP=P as Element of XX by TARSKI:def 1;
reconsider PPP=PP as Element of X\/{{}} by TARSKI:def 3;
now
let y be object; assume y in LH; then consider z such that
A1: y in z & z in F by TARSKI:def 4; consider x being Element of X\/{{}}
such that
A2: z=rng x & x in X by A1;
thus y in RH by A1, A2, TARSKI:def 1;
end; then
A3: LH c= RH;
now
let y be object; assume y in RH; then y in rng PP & rng PPP in F; hence
y in LH by TARSKI:def 4;
end; then
RH c= LH; hence thesis by A3;
end;
registration
let P be Function;
cluster SymbolsOf {P} \+\ rng P -> empty;
coherence by Th29, Th45;
end;
registration
let z be non zero Complex;
cluster |.z.| -> positive for ExtReal;
coherence by COMPLEX1:47;
end;
scheme Sc1 {A() -> set, B() -> set, F(set) -> set}:
{F(x) where x is Element of A(): x in A()} =
{F(x) where x is Element of B(): x in A()}
provided
A1: A() c= B()
proof
set LH={F(x) where x is Element of A(): x in A()}, RH=
{F(x) where x is Element of B(): x in A()};
now
let y be object;
assume y in LH; then consider x being Element of A() such that
A2: y=F(x) & x in A();
reconsider xx=x as Element of B() by A2, A1;
y=F(xx) & xx in A() by A2; hence y in RH;
end; then
A3: LH c= RH;
now
let y be object;
assume y in RH; then consider x being Element of B() such that
A4: y=F(x) & x in A(); reconsider xx=x as Element of A() by A4;
thus y in LH by A4;
end; then
RH c= LH; hence thesis by A3;
end;
definition
let X be functional set;
redefine func SymbolsOf X equals :: redefines SymbolsOf (FOMODEL0, definition)
union {rng x where x is Element of X: x in X};
compatibility
proof
set F1={rng x where x is Element of X: x in X}, F2=
{rng x where x is Element of X\/{{}}:x in X};X null {{}} c= X\/{{}}; then
A1: X c= X\/{{}};
F1=F2 from Sc1 (A1); hence thesis;
end;
end;
Lm51: for B being functional set, 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
let B be functional set; let A be Subset of B;
set AF={rng x where x is Element of A: x in A}, BF=
{rng x where x is Element of B:x in B};
let y be object;
assume y in AF; then consider x being Element of A such that
A1: y=rng x & x in A; reconsider xb=x as Element of B by A1;
thus y in BF by A1;
end;
theorem for B being functional set, A being Subset of B holds
SymbolsOf A c= SymbolsOf B by Lm51, ZFMISC_1:77;
theorem Th47: for A,B being functional set holds
SymbolsOf (A\/B) = SymbolsOf A \/ (SymbolsOf B)
proof
let A, B be functional set;
set AF={rng x where x is Element of A: x in A}, BF=
{rng x where x is Element of B: x in B}, F=
{rng x where x is Element of A\/B: x in A\/B};
A null B c= A\/B & B null A c= A\/B; then reconsider
AFF=AF, BFF=BF as Subset of F by Lm51;
A1: AFF \/ BFF c= F;
now
let y be object; assume y in F\BF; then
A2: y in F & not y in BF by XBOOLE_0:def 5; then
consider x being Element of A\/B such that
A3: y=rng x & x in A\/B;
not x in B by A3, A2;
then
A4: x in A null {{}} by A3, XBOOLE_0:def 3; then reconsider xx=x as
Element of A\/{{}};
thus y in AF by A4, A3;
end; then
F\BF \/ BF c= AF \/ BF by XBOOLE_1:9, TARSKI:def 3;
then F null BFF c= AF \/ BF by XBOOLE_1:39; then
A5: AF \/ BF = F by A1;
thus thesis by A5, ZFMISC_1:78;
end;
registration
let X; let F be Subset of bool X;
cluster union F \ X -> empty for set;
coherence;
end;
theorem Th48: X=X\Y\/(X/\Y)
proof
reconsider x=X\Y as Subset of X; X=x\/(X\x) by XBOOLE_1:45 .=
x\/(X/\Y) by XBOOLE_1:48; hence thesis;
end;
theorem m-tuples_on A meets n-tuples_on B implies m=n
by Lm5;
theorem B is D-prefix & A c= B implies A is D-prefix;
theorem Th51: f c= g iff for x st x in dom f holds (x in dom g & f.x = g.x)
proof
defpred Q1[] means for x being object st x in dom f holds x in dom g;
defpred Q2[] means for x being object st x in dom f holds f.x=g.x;
Q1[] & Q2[] iff dom f c= dom g & Q2[];
hence thesis by GRFUNC_1:2;
end;
registration
let X,Y be set;
cluster ((X\Y)\/(X/\Y)) \+\ X -> empty;
coherence by Th29, Th48;
let Z be set;
cluster ((X/\Y) \/ (X/\Z)) \+\ (X/\(Y\/Z)) -> empty;
coherence by XBOOLE_1:23, Th29;
cluster ((X\Y)\Z) \+\ (X\(Y\/Z)) -> empty;
coherence by XBOOLE_1:41, Th29;
end;
registration
let X,Y be functional set;
cluster SymbolsOf X \/ SymbolsOf Y \+\ SymbolsOf (X\/Y) -> empty;
coherence by Th47, Th29;
end;
registration
let U;
cluster non empty -> non empty-yielding for Element of (U*\{{}})*;
coherence
proof
set D=(U*\{{}})*; let p be Element of D; assume p is non empty; then
consider m such that
A1: m+1=len p by NAT_1:6;
reconsider pp=p as (1+m)-element (U*\{{}})-valued
FinSequence by A1, CARD_1:def 7;
{pp.1} \ (U*\{{}}) = {}; then pp.1 in U*\{{}} by ZFMISC_1:60; then
p.1 in U* & not p.1 in {{}} by XBOOLE_0:def 5; then
p.1 <> {} by TARSKI:def 1; hence thesis;
end;
end;
registration
let e be empty set;
cluster -> empty for Element of e*;
coherence;
end;
theorem Th52: (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
reconsider e={} as Element of {{}} by TARSKI:def 1;
defpred P[Nat] means for U1, U2, p st p is ($1+1)-element
holds
(p is {}*-valued implies U1-multiCat.p={}) &
(U1-multiCat.p = {} & p is U1*-valued implies p is {{}}-valued) &
(U1-multiCat.p <> {} & U2-multiCat.p <> {} implies U1-multiCat.p=
U2-multiCat.p);
A1: P[0]
proof
let U1, U2, p; set C1=U1-multiCat, C2=U2-multiCat;
A2: dom C1=U1** & dom C2=U2** by FUNCT_2:def 1;
{} /\ U1={}; then reconsider EE={} as Subset of U1; {}/\U2={}; then
reconsider EE2={} as Subset of U2; reconsider E2=EE2* as non empty Subset of
U2*; reconsider eu2={} as Element of E2 by TARSKI:def 1;
reconsider E=EE* as non empty Subset of U1*;
reconsider euu={} as Element of E by TARSKI:def 1;
assume p is (0+1)-element; then reconsider pp=p as (1+0)-element FinSequence;
len pp = 1 by CARD_1:def 7; then
A3: p= {}^<*p.1*> by FINSEQ_1:40 .= euu ^ <*p.1*>;
hereby
assume p is {}*-valued; then p=euu ^ <*euu*> by A3; hence C1.p=
C1.euu^euu by Th33 .= {}^{} .= {};
end;
hereby
assume A4: C1.p={} & p is U1*-valued; then reconsider
ppp=pp as non empty U1*-valued FinSequence; {ppp.1}\U1*={}; then
reconsider l=pp.1 as Element of U1* by ZFMISC_1:60; C1.p =
C1.euu^l by Th33, A3 .= {}^l .= l; then
p=euu ^ <*euu*> by A3, A4; hence p is {{}}-valued;
end;
hereby
assume C1.p<>{} & C2.p<>{}; then
A5: p in U1** & p in U2** by FUNCT_1:def 2, A2;
reconsider p1=pp as non empty U1*-valued FinSequence by A5;
reconsider p2=pp as non empty U2*-valued FinSequence by A5;
A6: {p1.1} \ U1* ={} & {p2.1}\U2*={};
reconsider u1=p1.1 as Element of U1* by A6, ZFMISC_1:60;
reconsider u2=p2.1 as Element of U2* by A6, ZFMISC_1:60;
A7: C1.p= C1.euu^u1 by A3, Th33 .= {}^u1 .= u1;
C2.p = C2.eu2^u2 by A3, Th33 .= {}^u1 .= u1;
hence C1.p=C2.p by A7;
end;
end;
A8: for n st P[n] holds P[n+1]
proof
let n; assume
A9: P[n];
let U1,U2; set C1=U1-multiCat, C2=U2-multiCat;
A10: dom C1=U1** & dom C2=U2** by FUNCT_2:def 1;
let p; assume
A11: p is (n+1+1)-element;
thus p is {}*-valued implies C1.p={}
proof
{} /\ U1={}; then reconsider EE={} as Subset of U1;
reconsider E=EE* as non empty Subset of U1*;
assume p is {}*-valued; then reconsider pp=p as (n+1+1+0)-element {}*-valued
FinSequence by A11; reconsider p1=pp|(Seg (n+1)) as (n+1)-element
E-valued FinSequence; {pp.(n+1+1)} \ {}* = {}; then
reconsider x1=pp.(n+1+1) as Element of E by ZFMISC_1:60;
pp \+\ p1 ^ <*x1*>={}; then pp=p1^<*x1*> & p1 is U1*-valued by Th29;
then C1.pp=C1.p1 ^ x1 by Th33 .= C1.p1 ^ {} .= {} by A9; hence thesis;
end;
thus C1.p={} & p is U1*-valued implies p is {{}}-valued
proof
assume
A12: C1.p={} & p is U1*-valued; then reconsider
pp=p as (n+1+1+0)-element U1*-valued FinSequence by A11;
reconsider p1=pp|(Seg (n+1)) as (n+1)-element U1*-valued FinSequence;
{pp.(n+1+1)} \ U1* = {}; then
reconsider x1=pp.(n+1+1) as Element of U1* by ZFMISC_1:60;
A13: pp \+\ p1 ^ <*x1*> = {}; then
pp=p1^<*x1*> by Th29; then
C1.p1^x1 = {} by Th33, A12; then C1.p1 = {} & x1=e;
then C1.p1 = {} & <*x1*>=<*e*>; then
reconsider p11=p1, x11=<*x1*> as {{}}-valued FinSequence by A9;
p11^x11 is {{}}-valued; hence p is {{}}-valued by A13, Th29;
end;
assume
A14: C1.p<>{} & C2.p <> {}; then
p in U1** by A10, FUNCT_1:def 2; then reconsider p1=p as
(n+1+1+0)-element U1*-valued FinSequence by A11;
reconsider q1=p1|(Seg (n+1)) as (n+1)-element U1*-valued FinSequence;
{p1.(n+1+1)} \ U1* = {}; then
reconsider x1=p1.(n+1+1) as Element of U1* by ZFMISC_1:60;
p in U2** by A14, A10, FUNCT_1:def 2; then reconsider p2=p as
(n+1+1+0)-element U2*-valued FinSequence by A11;
reconsider q2=p2|(Seg (n+1)) as (n+1)-element U2*-valued FinSequence;
{p2.(n+1+1)} \ U2*={}; then reconsider x2=p2.(n+1+1) as Element of U2*
by ZFMISC_1:60; p1 \+\ q1^<*x1*>={} & p2 \+\ q2^<*x2*> = {}; then
p1=q1^<*x1*> & p2=q2^<*x2*> by Th29; then
A15: C1.p1=C1.q1^x1 & C2.p2=C2.q2^x2 by Th33; assume
A16: C1.p <> C2.p; then
C1.q1 = {} or C2.q2={} by A9, A15; then
q1 is {{}}-valued by A9; then C1.q1={} & C2.q2={} by A9;
hence contradiction by A16, A15;
end;
A17: for n holds P[n] from NAT_1:sch 2(A1, A8);
set C1=U1-multiCat, C2=U2-multiCat;
A18: dom C1=U1** & dom C2=U2** by FUNCT_2:def 1;
hereby
assume
A19: C1.x<>{} & C2.x<>{}; then x in U1** & x <> {} by A18, FUNCT_1:def 2;
then reconsider p=x as non empty FinSequence;
consider m such that
A20: len p=m+1 by NAT_1:6;
reconsider pp=p as (m+1)-element FinSequence by A20, CARD_1:def 7;
C1.pp<>{} & C2.pp<>{} implies C1.pp=C2.pp by A17;
hence C1.x=C2.x by A19;
end;
hereby
assume
A21: p is {}*-valued;
per cases;
suppose p={}; hence C1.p={};
end;
suppose not p={}; then consider m such that
A22: m+1=len p by NAT_1:6; reconsider pp=p as (m+1)-element FinSequence by
A22, CARD_1:def 7;
C1.pp={} by A21, A17; hence C1.p={};
end;
end;
assume
A23: C1.p={} & p is U1*-valued;
per cases;
suppose p={}; hence p is {}*-valued;
end;
suppose not p={}; then consider m such that
A24: m+1=len p by NAT_1:6; reconsider pp=p as (m+1)-element FinSequence by
A24, CARD_1:def 7;
pp is {}*-valued by A23, A17;
hence p is {}*-valued;
end;
end;
registration
let U, x;
cluster U-multiCat.x -> U-valued;
coherence proof U-multiCat.x in U* by Th40; hence thesis; end;
end;
definition
let x;
func x null equals x;
coherence;
end;
registration
let x;
reduce x null to x;
reducibility;
end;
registration
let Y be with_non-empty_elements set;
cluster non empty -> non empty-yielding for Y-valued Relation;
coherence
proof
let R be Y-valued Relation; assume R is non empty; then reconsider
Y0 = rng R as non empty set; set y=the Element of Y0;
now
assume Y0 c= {{}}; then y in {{}} & y in Y by TARSKI:def 3;
hence contradiction;
end; hence thesis;
end;
end;
registration
let X;
cluster X\{{}} -> with_non-empty_elements;
coherence
proof
{} in {{}} by TARSKI:def 1; then not {} in X\{{}} by XBOOLE_0:def 5;
hence thesis by SETFAM_1:def 8;
end;
end;
registration
let X be with_non-empty_elements set;
cluster -> with_non-empty_elements for (Subset of X);
coherence
proof
let Y be Subset of X;
not {} in Y; hence thesis by SETFAM_1:def 8;
end;
end;
registration
let U;
cluster U* -> infinite for set;
coherence proof omega c= card (U*) by CARD_4:14; hence thesis; end;
end;
registration
let U;
cluster U* -> with_non-empty_element for set;
coherence;
end;
registration
let X be with_non-empty_element set;
cluster with_non-empty_elements for non empty Subset of X;
existence
proof set x = the non empty Element of X; take IT={x}; thus thesis; end;
end;
Lm52: p <> {} & p is Y-valued & Y c= U* & Y is with_non-empty_elements
implies U-multiCat.p <> {}
proof
assume p<>{}; then reconsider pp=p as non empty FinSequence; assume
A1: p is Y-valued & Y c= U* & Y is with_non-empty_elements; then
rng pp c= Y & Y c= U*; then reconsider YY=Y as
with_non-empty_elements non empty Subset of U* by A1;
reconsider pp as non empty YY-valued FinSequence by A1; pp is U*-valued &
not pp is {}*-valued;
hence thesis by Th52;
end;
theorem U1 c= U2 & Y c= U1* & p is Y-valued & p<>{} &
Y is with_non-empty_elements implies U1-multiCat.p=U2-multiCat.p
proof
assume U1 c= U2; then reconsider U11=U1 as non empty Subset of U2;
assume Y c= U1*; then reconsider Y1=Y as Subset of U11*;
reconsider Y2 = Y1 as Subset of U2* by XBOOLE_1:1; assume
p is Y-valued; then reconsider p1=p as Y1-valued
FinSequence; reconsider p2=p1 as Y2-valued FinSequence;
assume p <> {} & Y is with_non-empty_elements; then
U1-multiCat.p1 <> {} & U2-multiCat.p2 <> {} by Lm52; hence thesis by Th52;
end;
theorem (ex p st x=p & p is X*-valued) implies U-multiCat.x is X-valued
proof
set C=U-multiCat;
A1: dom C=U** by FUNCT_2:def 1; given p such that
A2: x=p & p is X*-valued; x is FinSequence of X* by A2, Lm1;
then reconsider px=x as Element of X**;
per cases;
suppose
A3: C.p<>{}; then p in U** & p<>{} by FUNCT_1:def 2, A1; then
reconsider pp=x as non empty FinSequence of U* by Lm1, A2;
A4: pp is X*-valued & not pp is {}*-valued by Th52, A2, A3;
reconsider XX=X as non empty set by Th52, A2, A3; set CX=XX-multiCat;
reconsider pxx=px as Element of XX**; CX.pp<>{} by Th52, A4;
hence thesis by Th52, A3, A2;
end;
suppose C.p={}; then reconsider e=C.p as empty set;
rng e c= X; hence thesis by A2;
end;
end;
registration
let X,m;
cluster (m-tuples_on X) \ (X*) -> empty for set;
coherence
proof
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
mm-tuples_on X c= X* by FINSEQ_2:134; hence thesis;
end;
end;
theorem (A/\B)* = A* /\ (B*)
proof
set X=A/\B; reconsider XA=A/\B as Subset of A; reconsider XB=A/\B as
Subset of B; XA* c= A* & XB* c= B*; then A1: X* c= A* /\ (B*) by XBOOLE_1:19;
now
let x be object; assume
A2: x in A*/\(B*); reconsider pa=x as A-valued FinSequence by A2;
set m=len pa, mA=m-tuples_on A, mB=m-tuples_on B, mX=m-tuples_on X;
mX\(X*)={}; then A3: mX c= X* by XBOOLE_1:37;
reconsider pb=x as B-valued FinSequence by A2;
pa is m-element & pb is m-element by CARD_1:def 7; then
pa in mA & pb in mB by Th16; then pa in mA/\mB by XBOOLE_0:def 4; then
pa in mX by Th3; hence x in X* by A3;
end; then A*/\(B*) c= X*; hence thesis by A1;
end;
theorem Th56: (P\/Q)|X = P|X \/ (Q|X)
proof
set R1=P|X, R2=Q|X, R=P\/Q, LH=R|X, RH=R1\/R2;
(P null Q)|X c= (P\/Q)|X & (Q null P)|X c= (P\/Q)|X by RELAT_1:76; then
A1: RH c= LH by XBOOLE_1:8;
now
let z be object; assume A2: z in LH; then consider x,y being object such that
A3: z=[x,y] by RELAT_1:def 1;
A4: x in X & [x,y] in (P\/Q) by RELAT_1:def 11, A2, A3;
(x in X & [x,y] in P) or (x in X & [x,y] in Q) by A4, XBOOLE_0:def 3;
then [x,y] in P|X or [x,y] in Q|X by RELAT_1:def 11;
hence z in P|X \/ (Q|X) by XBOOLE_0:def 3, A3;
end; then LH c= RH; hence thesis by A1;
end;
registration
let X;
cluster (bool X) \ X -> non empty for set;
coherence
proof
not bool X c= X by CARD_1:25;
hence thesis by XBOOLE_1:37;
end;
end;
registration
let X; let R be Relation;
cluster R null X -> (X\/dom R)-defined for Relation;
coherence
proof
dom R null X c= dom R \/ X;
hence thesis;
end;
end;
theorem Th57: f|X +* g = f|(X\dom g) \/ g
proof
set f1=f|(X\dom g), a1=g;
dom f1 c= X\dom a1 & X\dom a1 misses dom a1 by
XBOOLE_1:79; then
A1: f1 tolerates a1 by PARTFUN1:56, XBOOLE_1:63;
f|X +* a1 = f|(X\dom a1\/(X/\dom a1)) +* a1 by Th48 .=
f1 +* f|(X/\dom a1) +* a1 by FUNCT_4:78 .=
f1 +* (f|(X/\dom a1) +*(a1 null {} null ({}\/dom a1)))
by FUNCT_4:14 .= f1 +* (f|X|dom a1 +* a1|(dom a1))
by RELAT_1:71 .= f1 +* (f|X +* a1)|(dom a1) by FUNCT_4:71
.= f1 +* a1 .= f1 \/ a1 by A1, FUNCT_4:30; hence thesis;
end;
registration
let X; let f be X-defined Function, g be total X-defined Function;
identify f+*g with g null f;
compatibility
proof
dom g=X & dom f c= X by PARTFUN1:def 2;
hence thesis by FUNCT_4:19;
end;
identify g null f with f+*g;
compatibility;
end;
theorem Th58: not y in proj2 X implies [:A,{y}:] misses X
proof
set X2=proj2 X, Y=[:A,{y}:], Z=X/\Y; assume A1: not y in X2; assume
Y meets X; then Z<>{};
then consider z being object such that
A2: z in Z; set x1=z`1, y1=z`2;
x1 in A & y1 in {y} & z=[x1,y1] & z in X by A2, MCART_1:10,21; then
y1=y & y1 in X2 by TARSKI:def 1, XTUPLE_0:def 13;
hence contradiction by A1;
end;
definition
let X;
func X-freeCountableSet -> set equals
[:NAT, {the Element of (bool proj2 X\proj2 X)}:];
::#Might use ZFMISC_1:127 instead?
coherence;
end;
theorem Th59: X-freeCountableSet/\X={} & X-freeCountableSet is infinite
proof
set X2=proj2 X, Y=(bool X2)\X2, y=the Element of Y, IT=X-freeCountableSet;
not y in X2 by XBOOLE_0:def 5;
hence IT/\X={} by XBOOLE_0:def 7, Th58;
thus thesis;
end;
registration
let X;
cluster X-freeCountableSet -> infinite for set;
coherence;
end;
registration
let X;
cluster X-freeCountableSet /\ X -> empty;
coherence by Th59;
end;
registration
let X;
cluster X-freeCountableSet -> countable for set;
coherence by CARD_4:7;
end;
registration
cluster NAT\INT -> empty;
coherence
proof
set X=NAT null ([:{0},NAT:] \ {[0,0]}); reconsider
XX=X as Subset of INT; XX\INT ={}; hence thesis;
end;
end;
registration
let x,p;
cluster (<*x*>^p).1 \+\ x -> empty for set;
coherence proof (<*x*>^p).1=x by FINSEQ_1:41; hence thesis; end;
end;
registration
let m; let m0 be zero number; let p be m-element FinSequence;
cluster p null m0 -> total for (Seg (m+m0))-defined Relation;
coherence
proof
reconsider l=len p as Element of NAT; dom p = Seg l by FINSEQ_1:def 3
.= Seg m by CARD_1:def 7;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let U, q1, q2;
cluster U-multiCat.<*q1, q2*> \+\ q1^q2 -> empty for set;
coherence
proof
reconsider f=U-concatenation as BinOp of U*; q1 is FinSequence of U
by Lm1; then reconsider q11=q1 as Element of U*; set F=MultPlace f,
p=<*q11*>, C=U-multiCat; C.<*q1, q2*>=(C.p)^q2 by Th33
.= (F.p)^q2 by Th32 .= q1^q2 by Lm15; hence thesis;
end;
end;
registration
let f; let e be empty set;
identify f +* e with f null e;
compatibility;
identify f null e with f+*e;
compatibility;
identify e+*f with f null e;
compatibility;
identify f null e with e+*f;
compatibility;
end;
registration
let X be infinite set;
cluster denumerable for Subset of X;
existence
proof
consider Y such that A1: Y c= X & card Y=omega by CARD_3:87;
reconsider YY=Y as Subset of X by A1; take YY;
thus YY is denumerable by A1, CARD_3:def 15;
end;
end;
registration
let X be countable finite-membered set;
cluster union X -> countable for set;
coherence
proof
for Y st Y in X holds Y is countable;
hence thesis by CARD_4:12;
end;
end;
registration
let X be countable finite-membered functional set;
cluster SymbolsOf X -> countable for set;
coherence
proof
deffunc F(Relation)=rng $1; defpred P[set] means $1 in X;
reconsider A=X\/{{}} as non empty finite-membered functional set;
set IT={F(x) where x is Element of A: P[x]};
A1: now
let y; assume y in IT; then consider x being Element of A such that
A2: y=F(x) & P[x];
thus y is finite by A2;
end;
card IT c= card X from TREES_2:sch 2;
then reconsider ITT=IT as countable finite-membered set
by A1, FINSET_1:def 6, WAYBEL12:1;
union ITT=SymbolsOf X; hence thesis;
end;
end;
registration
let A,B be countable set;
cluster A\/B -> countable for set;
coherence by CARD_2:85;
end;
theorem Th60: union X c= Y implies X c= bool Y
proof
assume A1: union X c= Y & not X c= bool Y;
then consider A being object such that
A2: A in X & not A in bool Y;
reconsider AA=A as set by TARSKI:1;
AA c= Y by A2, A1, SETFAM_1:41; hence contradiction by A2;
end;
theorem Th61:
for X being set holds
A is_finer_than B & X is_finer_than Y implies A\/X is_finer_than B\/Y
proof
let X be set;
set LH=A\/X, RH=B\/Y; assume
A1: A is_finer_than B & X is_finer_than Y;
now
let Z be set; assume
A2: Z in LH;
per cases by XBOOLE_0:def 3, A2;
suppose
Z in A; then consider b being set such that
A3: b in B & Z c= b by SETFAM_1:def 2, A1; take b;
thus b in RH by A3, XBOOLE_0:def 3; thus Z c= b by A3;
end;
suppose Z in X; then consider y being set such that
A4: y in Y & Z c= y by SETFAM_1:def 2, A1; take y;
thus y in RH by A4, XBOOLE_0:def 3; thus Z c= y by A4;
end;
end; hence thesis by SETFAM_1:def 2;
end;
theorem Th62: A is_finer_than B implies A\/B is_finer_than B
proof
assume A is_finer_than B; then
A\/B is_finer_than B\/B by Th61; hence thesis;
end;
theorem Th63: B is c=directed & A is_finer_than B implies
A\/B is c=directed
proof
assume
A1: B is c=directed & A is_finer_than B;
reconsider BB=B as
c=directed set by A1; reconsider X=A\/BB as non empty set;
now
let a, b be set; assume a in X; then consider aa being set such that
A2: aa in B & a c= aa by SETFAM_1:def 2, A1, Th62; assume
b in X; then consider bb being set such that
A3: bb in B & b c= bb by SETFAM_1:def 2, A1, Th62;
consider cc being set such that
A4: aa\/bb c= cc & cc in B by A1, A2, A3, COHSP_1:5; take cc;
a\/b c= aa\/bb by A2, A3, XBOOLE_1:13; hence a\/b c= cc by A4;
thus cc in X by A4, XBOOLE_0:def 3;
end; hence A\/B is c=directed by COHSP_1:6;
end;
theorem Th64: INTERSECTION(X,Y) is_finer_than X
proof
now
let xy be set;assume xy in INTERSECTION(X,Y);then consider x,y such that
A1: x in X & y in Y & xy=x/\y by SETFAM_1:def 5;
take x; thus x in X & xy c= x by A1;
end;
hence thesis by SETFAM_1:def 2;
end;
theorem Y is c=directed implies for X being finite Subset of union Y
ex y st y in Y & X c= y ::#COHSP_1:13 with shorter proof
proof
set F=Y; assume
A1: F is c=directed; let X be finite Subset of union F;
X/\union F = union INTERSECTION ({X},F) by SETFAM_1:25; then
reconsider FF=INTERSECTION({X}, F) as finite Subset-Family of X by Th60;
A2: X null union F = union FF by SETFAM_1:25;
F\/FF is c=directed & FF null F c= F\/FF by Th63, Th64, A1; then
consider a being set such that
A3: union FF c= a & a in F\/FF by COHSP_1:def 4;
a in F or (a in FF & FF is_finer_than F) by A3, Th64, XBOOLE_0:def 3;
then consider b being set such that
A4: b in F & a c= b by SETFAM_1:def 2; take b;
thus b in F & X c= b by A2, A3, A4;
end;
Lm53: X is Subset of Funcs(A,B) implies X is Subset-Family of [:A,B:]
proof
A1: Funcs(A,B) c= bool [:A,B:] by FRAENKEL:2;
assume X is Subset of Funcs (A, B); hence thesis by A1, XBOOLE_1:1;
end;
theorem ::#Th66
X is Subset of Funcs(A,B) implies X is Subset-Family of [:A,B:] by Lm53;
Lm54: for x,y being Element of U st x in Y iff y in Y
holds [(chi(Y,U)).x, (chi(Y,U)).y] in (id BOOLEAN)
proof
let x,y be Element of U; set f=chi(Y,U);
assume A1: x in Y iff y in Y;
per cases;
suppose x in Y; then f.x=1 & y in Y by A1, RFUNCT_1:63; then
f.x=1 & f.y=1 & 1 in BOOLEAN by RFUNCT_1:63; hence thesis by RELAT_1:def 10;
end;
suppose not x in Y; then f.x=0 & not y in Y by A1, RFUNCT_1:64; then
f.x=0 & f.y=0 & 0 in BOOLEAN by RFUNCT_1:64; hence thesis by RELAT_1:def 10;
end;
end;
theorem for x,y being Element of U st x in Y iff y in Y ::#Th67
holds [(chi(Y,U)).x, (chi(Y,U)).y] in (id BOOLEAN) by Lm54;
definition
let A,R;
func R typed| A -> Subset of R equals R|A;
coherence by RELAT_1:59;
end;
registration
let A,R;
identify R typed| A with R|A;
compatibility;
identify R|A with R typed| A;
compatibility;
end;
Lm55: R|(A\B) = R|A \ [:B, rng R:]
proof
set lh=R|(A\B), rh=R|A \ [:B, rng R:];
lh = R|A \ (R|B) by RELAT_1:80 .= R|A \ (R /\ [: B, rng R :])
by RELAT_1:67 .= (((R|A) null R) \ R) \/ rh
by XBOOLE_1:54 .= {} \/ rh; hence thesis;
end;
Lm56: f +* g = f \ [: dom g, rng f :] \/ g
proof
set df=dom f, dg=dom g, rf=rng f;
f|df +* g = f|(df \ dg) \/ g by Th57 .= f|df \ [:dg, rf:] \/ g by Lm55;
hence thesis;
end;
Lm57: A/\C=A\(A\/B\C)
proof
set Y=A\/B; A\(Y\C)=(A null B \Y)\/(A/\C) by XBOOLE_1:52 .= {} \/ (A/\C);
hence thesis;
end;
registration
let A,B,C;
cluster A\(A\/B\C) \+\ (A/\C) -> empty;
coherence by Lm57, Th29;
end;
definition
let X; let P be set;
func P |1 X -> set equals P /\ [:X, proj2 P:];
coherence;
end;
registration
let X, P;
identify P |1 X with P | X;
compatibility by RELAT_1:67;
identify P|X with P |1 X;
compatibility;
end;
Lm58: P|(dom P \ X)= P\[:X, rng P:]
proof
set A=dom P, B=rng P, C=[:A\X, B:];
P\[:A, B:]={}; then reconsider P as Subset of [:A, B:] by Th29;
P\(P\/[:A, B:]\C) \+\ (P/\C) = {} &
[:A, B:] \ ([:A, B:] \/ {} \[:X,B:]) \+\ [:A, B:] /\ [:X, B:] ={}; then
A1: P\([:A, B:] null P \ C) = P/\C
& [:A, B:] \ ([:A,B:] \ [:X,B:])= [:A,B:] /\ [:X,B:] by Th29;
P|(A\X) = P\([:A,B:] /\ [:X, B:]) by A1, ZFMISC_1:102 .=
P\[:A,B:] \/ (P \ [:X,B:])
by XBOOLE_1:54 .= {} \/ (P\[:X,B:]); hence thesis;
end;
definition
let P,Q;
func P +*1 Q equals P\[:dom Q, rng P:] \/ Q; ::# could be extended to sets
coherence;
func P +*2 Q equals P|(dom P \ dom Q) \/ Q;
coherence;
func P +*3 Q equals P|(dom P) \ (P|(dom Q)) \/ Q;
coherence;
end;
registration
let P,Q;
identify P +*1 Q with P +*2 Q;
compatibility by Lm58;
identify P +*2 Q with P +*3 Q;
compatibility by RELAT_1:80;
end;
registration
let f,g;
identify f +* g with f +*1 g;
compatibility by Lm56;
identify f +*1 g with f +* g;
compatibility;
end;
registration
let U be non empty set, u be Element of U, q be U-valued FinSequence;
set f=U-firstChar, p=<*u*>, P=p^q;
cluster U-firstChar.(<*u*>^q) \+\ u -> empty;
coherence
proof P.1 \+\ u = {}; then u = P.1 by Th29 .= f.P by Th6; hence thesis; end;
end;
registration
cluster negative integer for Real;
existence
proof take -1;thus thesis; end;
cluster positive -> natural for Integer;
coherence;
end;
registration
let X,Y; let x be Subset of X, y be Subset of Y;
cluster x\Y \ (X\y) -> empty for set;
coherence
proof x\Y c= X\y by XBOOLE_1:35; hence thesis; end;
end;
registration
let X,Y; let x be Subset of X, y be Subset of Y;
cluster x\Y \ (X\y) -> empty for set;
coherence;
end;
registration
let X,Y; let x be Subset of X;
cluster x\Y \ (X\Y) -> empty for set;
coherence proof x\Y \ (X\(Y/\Y))={}; hence thesis; end;
end;
registration
let X,Y; let x be Subset of X, y be Subset of Y;
cluster (x\/y \ Y)\X -> empty for set;
coherence proof x\/y\Y = x\Y \/ (y\Y) by XBOOLE_1:42 .= x\Y; hence thesis;end;
end;
theorem (dom f c= dom R & R c= f) implies R=f by Lm42; ::#Th68
begin ::# Schemes
registration
let T be trivial set, x,y be Element of T;
cluster x \+\ y -> empty for set;
coherence
proof
set t=the Element of T;
per cases;
suppose T={}; then
x={} & y={} by SUBSET_1:def 1; hence thesis;
end;
suppose T<>{}; then consider t being object such that
A1: T={t} by ZFMISC_1:131;
x=t by A1, TARSKI:def 1 .= y by A1, TARSKI:def 1;
hence thesis;
end;
end;
end;
scheme
FraenkelTrivial {E() -> trivial set, F(object) -> object, P[set,set]}:
{F(x) where x is Element of E(): P[x, E()]} c= {F(the Element of E())}
proof
set e=the Element of E(), LH=
{F(x) where x is Element of E(): P[x, E()]}, RH={F(e)};
let z be object;
assume z in LH; then consider x being Element of E() such that
A1: z=F(x) & P[x, E()];
x \+\ e = {}; then z=F(e) by A1, Th29; hence z in RH by TARSKI:def 1;
end;
scheme OnSingleTonsGen ::# extending ALTCAT_2:sch 1 ::#sch 3
{X() -> set, F (set) -> set, P[set]}:
{[o,F(o)] where o is Element of X(): P[o]} is Function
proof
deffunc G(set)=[$1, F($1)];
defpred Q[set, set] means P[$1];
per cases;
suppose X() is non empty; then reconsider XX=X() as non empty set;
{[o,F(o)] where o is Element of XX: P[o]} is Function from ALTCAT_2:sch 1;
hence thesis;
end;
suppose X() is empty; then reconsider XX=X() as trivial set;
{G(o) where o is Element of XX: Q[o, XX]} c= {G(the Element of XX)} from
FraenkelTrivial; hence thesis;
end;
end;
scheme FraenkelInclusion {X()->set, F(set,set)->set, P[set,set]}:
X() c= {F(x,X()) where x is Element of X() :P[x,X()]}
provided
A1: for y being set st y in X() ex x being set st
x in X() & P[x,X()] & y=F(x,X())
proof
set Y={F(z,X()) where z is (Element of X()) :P[z,X()]};
let y be object;
assume y in X(); then consider x being set such that
A2: x in X() & P[x,X()] & y=F(x,X()) by A1;
thus y in Y by A2;
end;
scheme FraenkelInclusion2 {X()->set, P[set,set]}:
X() c= {x where x is Element of X():P[x,X()]}
provided
A1: for x being set st x in X() holds P[x,X()]
proof
deffunc F(set, set)=$1;
set Y={F(x,X()) where x is Element of X(): P[x,X()]};
A2: for y being set st y in X() ex x being set st
x in X() & P[x,X()] & y=F(x,X()) by A1;
X() c= Y from FraenkelInclusion (A2); hence thesis;
end;
scheme FraenkelEq {X()->non empty set, P[set]}: ::# superfluous `non empty'
X() = {x where x is Element of X(): P[x]}
provided
A1: for x being set st x in X() holds P[x]
proof
set Y={x where x is Element of X(): P[x]};
A2: Y c= X() from FRAENKEL:sch 10;
defpred Q[set,set] means P[$1];
set Z={x where x is Element of X(): Q[x, X()]};
A3: for x being set st x in X() holds Q[x,X()] by A1;
X() c= Z from FraenkelInclusion2 (A3);
hence thesis by A2;
end;
begin ::# Registrations, notations, redefinitions, type tuning
registration
let Y be set, X be Subset of Y;
cluster proj1 X \ proj1 Y -> empty;
coherence by XTUPLE_0:8, Th29;
cluster proj2 X \ proj2 Y -> empty;
coherence by XTUPLE_0:9, Th29;
end;
registration
let X,Y;
cluster proj1 [:X,Y:]\X -> empty;
coherence by FUNCT_5:10, Th29;
cluster proj1 [:X,Y:]/\X \+\ (proj1 [:X,Y:]) -> empty;
coherence
proof
set LH=proj1 [:X,Y:]; LH \ X={}; then
reconsider LH as Subset of X by Th29;
LH /\ X = LH null X; hence thesis;
end;
cluster proj2 [:X,Y:]\Y -> empty;
coherence by FUNCT_5:10, Th29;
cluster proj2 [:X,Y:]/\Y \+\ (proj2 [:X,Y:]) -> empty;
coherence
proof
set LH=proj2 [:X,Y:]; LH \ Y = {}; then
reconsider LH as Subset of Y by Th29;
LH /\ Y = LH null Y; hence thesis;
end;
cluster proj2 X \/ proj2 Y \+\ proj2(X\/Y) -> empty;
coherence by XTUPLE_0:27, Th29;
cluster proj1 X \/ proj1 Y \+\ proj1(X\/Y) -> empty;
coherence by XTUPLE_0:23, Th29;
let y be Subset of Y;
cluster (X\Y)/\y -> empty;
coherence proof (X\Y)/\(Y/\y)={}; hence thesis; end;
end;
registration
let X; let U be non empty set;
cluster proj1 [:X,U:] \+\ X -> empty;
coherence
proof proj1 [:X,U:]=X by FUNCT_5:9; hence thesis; end;
cluster proj2 [:U,X:] \+\ X -> empty;
coherence
proof proj2 [:U,X:]=X by FUNCT_5:9; hence thesis; end;
end;
registration
let X; let Y be non empty set;
reduce proj1 [:X,Y:] to X;
reducibility proof proj1 [:X,Y:] \+\ X={}; hence thesis by Th29; end;
reduce proj2 [:Y,X:] to X;
reducibility proof proj2 [:Y,X:] \+\ X={}; hence thesis by Th29; end;
end;
registration
let R,X;
cluster R.:X \ rng R -> empty;
coherence by RELAT_1:111,Th29;
end;
registration
let A,B,X,Y;
cluster [:A,B:] \ [:A\/X, B\/Y:] -> empty;
coherence
proof
A null X c= A\/X & B null Y c= B\/Y; hence thesis by ZFMISC_1:96, Th29;
end;
end;
registration
let X,Y,Z;
cluster X/\Y/\Z \+\ (X/\(Y/\Z)) -> empty;
coherence by Th29, XBOOLE_1:16;
end;
registration
let X,Y;
reduce X\Y\/(X/\Y) to X;
reducibility by Th48;
end;
registration
let P; let X be Subset of dom P;
reduce dom (P | X) to X;
reducibility by RELAT_1:62;
end;
registration
let X; let x,y be Subset of X;
cluster x\/y \ X -> empty;
coherence;
end;
registration ::: to appear in FUNCT_*
let X;
cluster id X -> onto;
coherence;
end;
registration
cluster symmetric -> involutive for Function;
coherence
proof
let g; set G=field g, D=dom g, C=rng g; assume g is symmetric; then
A1: g is_symmetric_in G by RELAT_2:def 11;
now
let x; set y=g.x; assume A2: x in D null C; then y in C null D & [x,y] in
g by FUNCT_1:3, def 2; then
[y,x] in g by A2, A1, RELAT_2:def 3; hence x=g.y by FUNCT_1:1;
end;
hence thesis by PARTIT_2:def 2;
end;
end;
registration
cluster non empty involutive for Function; ::# WHY NEEDED?
existence proof take id 1; thus thesis; end;
end;
registration
let f be non empty involutive Function; let x be Element of dom f;
reduce f.(f.x) to x;
reducibility by PARTIT_2:def 2;
end;
registration
let X,Y;
cluster [:X,Y:] -> Y-valued;
coherence
proof rng [:X,Y:] \ Y={}; hence thesis by Th29; end;
end;
registration
let x,y;
cluster [:{x},{y}:] +* [:{y},{x}:] -> symmetric;
coherence
proof
set a=y, b=x, f=(x,y)-->(a,b); reconsider R=f as Relation;
per cases;
suppose x=y; then
A1: f={[x,x]} by ZFMISC_1:29; {[x,x]} \+\ id{x}={}; hence thesis by A1,Th29;
end;
suppose
A2: x<>y;
A3: f=[:{x},{a}:]+*[:{y},{b}:] .=
[:{x},{a}:]|{x} \/ [:{y},{b}:]
by ZFMISC_1:14, A2 .= [:{x},{a}:] \/ [:{y},{b}:];
::# up to here could have used PARTFUN1:56 + FUNCT_4:30 instead
::# also FUNCT_4:67
R~=[:{x},{a}:]~ \/ [:{y},{b}:]~ by RELAT_1:23, A3 .=
[:{x},{a}:]~ \/ [:{b},{y}:] by SYSREL:5 .=
R by A3, SYSREL:5;
hence thesis by RELAT_2:13;
end;
end;
end;
registration
let X,P; let x be Subset of X;
cluster P"x \ (P"X) -> empty;
coherence by RELAT_1:143, Th29;
end;
registration
let X,P;
cluster P"(X\/rng P) \+\ dom P -> empty;
coherence
proof
set D=dom P, C=rng P, XX=X\/C;
P"(C null X)\ P"XX = {}; then P"C c= P"XX by Th29; then
D c= P"XX & P"XX c= D by RELAT_1:134,132;
hence thesis by XBOOLE_0:def 10, Th29;
end;
end;
registration
let X; let R be total X-defined Relation;
cluster X \+\ dom R -> empty;
coherence by PARTFUN1:def 2, Th29;
end;
registration
let P be non empty Relation;
cluster -> pair for Element of P;
coherence
proof
let x be Element of P;
consider y,z being object such that
A1: x=[y,z] by RELAT_1:def 1; thus thesis by A1;
end;
end;
registration
let X; let Y be non empty set; let f be Y-valued total X-defined Function;
cluster {f} \ Funcs(X,Y) -> empty;
coherence
proof
f=f & dom f=X & rng f c= Y by PARTFUN1:def 2; then
f in Funcs(X,Y) by FUNCT_2:def 2; hence thesis by Th29;
end;
end;
registration
let X be non empty set; let f be X-valued total X-defined Function;
cluster rng f \ dom f -> empty;
coherence
proof
set D=dom f, C=rng f; D=X & C c= X by PARTFUN1:def 2;
hence thesis;
end;
end;
registration
let X; let Y be Subset of X;
reduce id X .: Y to Y;
reducibility by FUNCT_1:92;
end;
registration
let A,B; let a be Subset of A;
cluster a\(A\B) \+\ a/\B -> empty;
coherence proof a\(A \/ a \B) \+\ a/\B={}; hence thesis; end;
end;
definition
let a,b;
func a doubleton b equals {a}\/{b};
coherence;
end;
registration ::# To automate {a,b}={a}\/{b}
let a,b;
identify {a,b} with a doubleton b;
compatibility by ENUMSET1:1;
identify a doubleton b with {a,b};
compatibility;
identify a doubleton b with b doubleton a;
compatibility;
end;
definition
let X,Y;
func X .:1 Y -> set equals proj2 (X |1 Y);
coherence;
end;
registration
let P,X;
identify P.:X with P .:1 X;
compatibility by RELAT_1:115;
identify P .:1 X with P.:X;
compatibility;
end;
notation ::# Fallback notation for when ambiguities arise
let P,Q;
synonym P >*>↑ Q for P*Q;
end;
notation
let f,g;
synonym g <*<↑ f for g*f;
end;
definition
let P,Q;
redefine func P +*1 Q -> Subset of P\/Q; :: redefines +*1 (FOMODEL0, definition)
coherence
proof
set dp=dom P, dq=dom Q, rp=rng P, rq=rng Q, R=P\/Q; reconsider
p=P\[:dq,rp:] as Subset of P; p c= P & P null Q c= P \/ Q; then
reconsider p as Subset of R by XBOOLE_1:1; reconsider QQ=Q null P as
Subset of R; p\/QQ \ R ={}; hence thesis;
end;
end;
Lm59: for x being Element of [:f,g:] st f<>{} & g<>{} holds
x`1 is pair & x`2 is pair
proof
set F=[:f,g:], D=dom F, C=rng F, df=dom f, dg=dom g, rf=rng f, rg=rng g;
let x be Element of F; assume f<>{} & g<>{}; then reconsider
U=[:[:df,dg:],[:rf,rg:]:] as non empty Relation;
A1: F c= [:D,C:] & D=[:df,dg:] & C=[:rf,rg:]
by FUNCT_3:def 8, RELAT_1:7, FUNCT_3:67; then
reconsider F as Function-like Relation-like Subset of U; F<>{} by A1;
then x in F; then reconsider xx=x as Element of U;
consider a,b being object such that
A2: a in [:df,dg:] & b in [:rf,rg:] & xx=[a,b] by ZFMISC_1:def 2;
reconsider a,b as set by TARSKI:1;
thus x`1 is pair & x`2 is pair by A2;
end;
registration
let f,g be non empty Function; let x be Element of [:f,g:];
cluster x`1 -> pair;
coherence by Lm59;
cluster x`2 -> pair;
coherence by Lm59;
end;
Lm60: P * [:B,C:] c= [: P"B, C:]
proof
set A=P"B, R1=[:B,C:], R2=[:A,C:], Q=P*R1;
A1: dom R1 \ B ={};
dom Q=P"(dom R1) by RELAT_1:147; then
reconsider DQ=dom Q as Subset of A by A1, Th29, RELAT_1:143;
[:DQ, C:]\[:A\/DQ,C\/{}:]={}; then
A2: [:DQ, C:] c= [:A,C:] by Th29; reconsider PP=P as
Relation of dom P, rng P by RELAT_1:7; [:B,C:] c= [:B,C:]; then
reconsider RR1=[:B,C:] as Relation of B, C; reconsider QQ=PP*RR1 as
Relation of dom P, C;
[:dom Q,rng Q:] c= [:dom Q, C:] & Q c= [:dom Q,rng Q:]
by RELAT_1:7, ZFMISC_1:95; then Q c= [:dom Q, C:];
hence Q c= [:A,C:] by A2;
end;
Lm61: P*[:B,C:] = [:P"B,C:]
proof
set A=P"B, R1=[:B,C:], R2=[:A,C:], Q=P*R1, LH=Q, RH=R2;
now
let z be object; assume
z in RH; then consider x,y being object such that
A1: x in A & y in C & z=[x,y] by ZFMISC_1:def 2;
consider x1 being object such that
A2: [x,x1] in P & x1 in B by RELAT_1:def 14, A1;
[x1,y] in [:B,C:] by A1, A2, ZFMISC_1:def 2;
hence z in LH by A1, A2, RELAT_1:def 8;
end; then RH c= LH & LH c= RH by Lm60;
hence thesis;
end;
Lm62: y<>{} & y c= Y implies [:X,y:]*[:Y,Z:] = [:X,Z:]
proof
assume y<>{}; then reconsider yy=y as non empty set;
set P=[:X,yy:], Q=[:Y,Z:]; assume y c= Y; then
reconsider z=rng P as Subset of Y by XBOOLE_1:1;
P"(Y \/ z) \+\ dom P = {} & dom P \+\ X={}; then
P"Y=dom P & dom P = X by Th29;
hence thesis by Lm61;
end;
Lm63: P*[:rng P, X:] = [: dom P, X:]
proof P*[:rng P, X:]=[:P"rng P,X:] by Lm61;hence thesis by RELAT_1:134;end;
Lm64: rng f=dom f implies f is onto Function of dom f, dom f
proof
set D=dom f, C=rng f; reconsider ff=f as Element of Funcs(D,C) by
FUNCT_2:def 2; assume A1: C=D; then reconsider fff=ff as
Function of D, D by FUNCT_2:66; fff is onto D-valued
by FUNCT_2:def 3, A1; hence thesis;
end;
Lm65: f is involutive implies f*f c= id dom f
proof
assume f is involutive; then reconsider ff=f as involutive Function;
set g=ff*ff, df=dom ff, dg=dom g, I=id df;
now
let x; assume
A1: x in dg;
then
A2: x in df by RELAT_1:25,TARSKI:def 3;
thus x in dom I by RELAT_1:25, TARSKI:def 3, A1;
thus I.x=x by
FUNCT_1:18,A2 .= f.(f.x) by A2,PARTIT_2:def 2 .=g.x by FUNCT_1:13,A2;
end;
hence thesis by Th51;
end;
Lm66: X/\id(proj1 X/\proj2 X) = X/\id(proj1 X)
proof
set D=proj1 X, C=proj2 X, i=id(D/\C), I=id D, R=X/\I, r=X/\i;
X/\i=X/\(I/\id(proj2 X)) & X/\I/\id proj2 X \+\ X/\(I/\id proj2 X)={}
by SYSREL:14; then
reconsider r as Subset of R by Th29;
now ::#R c= r
let z be object; assume
A1: z in R;
consider x,y being object such that
A2: z=[x,y] by RELAT_1:def 1, A1;
A3: x in D & y in C by A1, A2, XTUPLE_0:def 12, def 13;
A4: x=y by A2, A1, RELAT_1:def 10; then x in D/\C
by A3, XBOOLE_0:def 4; then [x,y] in i
by A4, RELAT_1:def 10; hence z in r by A1, A2, XBOOLE_0:def 4;
end;
then R c= r; hence thesis;
end;
Lm67: id X|Y=id(X/\Y)
proof
A1: dom id (X\Y)=X\Y & dom id (X/\Y)=X/\Y
& (X\Y)/\(Y/\Y)={} & X/\Y c= Y; then
A2: dom id (X\Y) misses Y & dom id (X/\Y) c= Y;
reconsider i=id (X/\Y) as Y-defined Function
by RELAT_1:def 18, A1;
X=X/\Y\/(X\Y); then id X=id(X/\Y) \/ id (X\Y) by SYSREL:14; then
id X|Y = id (X/\Y)|Y \/ (id(X\Y)|Y) by Th56; then id X|Y =
id(X/\Y)|Y \/ {} by A2, RELAT_1:152 .= i null Y .= i; hence thesis;
end;
Lm68: rng f1 /\ rng f2 = {} & b1<>b2 & rng f1 c= dom f2 & rng f2 c= dom f1
implies [:rng f1,{b2}:]\/[:rng f2,{b1}:] c=
((f1\/f2) >*> ([:rng f1,{b2}:]\/[:rng f2,{b1}:])) >*> ((b1,b2)-->(b2,b1))
proof
set A1=dom f1, A2=dom f2, g1=[:rng f1,{b2}:], g2=[:rng f2,{b1}:],
h1=b1.-->b2, h2=b2.-->b1, h=(b1,b2)-->(b2,b1), f=f1\/f2, g=g1\/g2;
assume
rng f1 /\ rng f2 = {}; then reconsider e= rng f1 /\ rng f2 as empty set;
A1: dom g1 /\ rng f2 = dom g1 /\ e .= {};
A2: dom g2 /\ rng f1 = dom g2 /\ e .= {};
A3: rng [:A1,{b2}:] /\{b2}/\{b1} \+\ (rng [:A1,{b2}:] /\({b2}/\{b1}))={};
rng [:A1,{b2}:] /\{b2} \+\ rng [:A1,{b2}:]={}; then
A4: rng [:A1,{b2}:] /\ {b1}=rng [:A1,{b2}:] /\ {b2}/\{b1} by Th29 .=
rng [:A1,{b2}:] /\ ({b1}/\{b2}) by A3, Th29; f*g=f >*> g1 \/ (f >*>g2)
by RELAT_1:32 .= f1 >*> g1 \/ (f2 >*> g1) \/ (f >*> g2) by SYSREL:6 .=
f1 >*> g1 \/ (f2 >*> g1) \/ ((f1 >*> g2) \/ (f2 >*> g2)) by SYSREL:6
.= f1>*>g1 \/ (f2 >*> g1) \/ ({} \/ (f2 >*> g2))
by A2, XBOOLE_0:def 7, RELAT_1:44 .=
f1 >*> g1 \/ {} \/ {} \/ (f2 >*> g2) by A1, XBOOLE_0:def 7, RELAT_1:44
.= [:A1,{b2}:] \/ (f2 >*> g2) by Lm63 .=
[:A1,{b2}:] \/ [:A2,{b1}:] by Lm63; then
A5: f * g >*> (h1\/h2) =
[:A1,{b2}:] >*> (h1\/h2) \/ ([:A2,{b1}:] >*> (h1\/h2)) by SYSREL:6 .=
[:A1,{b2}:] >*> h1 \/ ([:A1,{b2}:] >*> h2) \/
([:A2,{b1}:] >*> (h1\/h2)) by RELAT_1:32 .=
[:A1,{b2}:] >*> h1 \/ ([:A1,{b2}:] >*> h2) \/
(([:A2,{b1}:] >*> h1) \/ ([:A2,{b1}:] >*> h2)) by RELAT_1:32;
assume
A6: b1<>b2; then
A7: {b1}/\{b2}={} by XBOOLE_0:def 7, ZFMISC_1:11; then
{} = rng[:A1,{b2}:] /\ dom h1 by A4; then
A8: f * g >*> (h1\/h2) = {}\/ ([:A1,{b2}:] >*> h2) \/
([:A2,{b1}:] >*> h1 \/ ([:A2,{b1}:] >*> h2))
by RELAT_1:44, A5, XBOOLE_0:def 7;
A9: rng [:A2,{b1}:]/\({b1}/\{b2}) \+\ (rng [:A2,{b1}:] /\ {b1} /\{b2}) = {};
rng [:A2,{b1}:] /\ {b1} \+\ rng [:A2,{b1}:] ={}; then
rng [:A2,{b1}:] /\ {b2} = rng [:A2,{b1}:] /\ {b1} /\ {b2} by Th29 .=
rng [:A2,{b1}:] /\ ({b1}/\{b2}) by A9,Th29; then
rng [:A2,{b1}:] /\ dom h2 = {} by A7; then
[:A2,{b1}:] >*>h2 = {} by RELAT_1:44, XBOOLE_0:def 7; then
A10: f*g >*> (h1\/h2) =
[:A1,{b2}:] >*> h2 \/ [:(A2 --> b1) " {b1},{b2}:] by Lm61, A8 .=
[:A1,{b2}:] >*> h2 \/ [:A2,{b2}:] by FUNCOP_1:15 .=
[:(A1 --> b2)"{b2}, {b1}:] \/ [:A2,{b2}:] by Lm61 .=
[:A1,{b1}:] \/ (A2-->b2) by FUNCOP_1:15; assume
rng f1 c= A2; then reconsider B1=rng f1 as Subset of A2; assume
rng f2 c= A1; then reconsider B2=rng f2 as Subset of A1;
[:B1,{b2}:] \ [:A2 null B1,{b2} \/ {}:] = {} &
[:B2,{b1}:] \ [:A1 null B2,{b1} \/ {}:] = {}; then
A11: B1-->b2 c= A2-->b2 & B2-->b1 c= A1-->b1 by Th29; h =
[:{b1}\{b2},{b2}:] \/ h2 by
ZFMISC_1:102
.= h1 \/ h2 by A6, ZFMISC_1:11, XBOOLE_1:83;
hence thesis by A11, A10, XBOOLE_1:13;
end;
Lm69: a in {a1,f.a1} & f is involutive & a1 in dom f implies
{a,f.a}={a1,f.a1}
proof
assume
A1: a in {a1,f.a1} & f is involutive & a1 in dom f;
per cases;
suppose a=a1; hence thesis; end;
suppose a<>a1; then a=f.a1 by A1, TARSKI:def 2;
hence {a,f.a}={a1,f.a1} by A1, PARTIT_2:def 2;
end;
end;
Lm70: ((a in {a1,f.a1} or f.a in {a1,f.a1}) &
f is involutive & a in dom f & a1 in dom f) implies {a,f.a}={a1,f.a1}
proof
set X1={a1,f.a1}, X={a,f.a}; assume
A1: (a in X1 or f.a in X1) & f is involutive & a in dom f & a1 in dom f;
assume
A2: not thesis; then
{a1,f.a1} ={f.a, f.(f.a)} by Lm69, A1 .=
{f.a,a} by A1, PARTIT_2:def 2; hence contradiction by A2;
end;
Lm71: X c= f implies dom (f\X)=dom f\proj1 X
proof
assume X c= f; then reconsider g=X as Function-like Relation-like
Subset of f; set dg=dom g, df=dom f; f|dg=g by GRFUNC_1:23;
hence thesis by RELAT_1:177;
end;
Lm72: X<>{} implies the set of all x where x is Element of X = X
proof
assume X<>{}; then reconsider XX=X as non empty set;
defpred P[set] means not contradiction;
A1: for x st x in XX holds P[x];
set Y={x where x is Element of XX: P[x]};
XX=Y from FraenkelEq(A1); hence thesis;
end;
Lm73: [[a1,a2],[b1,b2]] in [:f,g:] iff ([a1,b1] in f & [a2,b2] in g)
proof
set a=[a1,a2], b=[b1,b2], F=[:f,g:];
thus [a,b] in F implies [a1,b1] in f & [a2,b2] in g
proof assume
A1: [a,b] in F; then reconsider F as non empty Function;
set D=dom F, C=rng F;
F <> {}; then reconsider ff=f, gg=g as non empty Function; set df=dom ff,
dg=dom gg, rf=rng ff, rg=rng gg;
reconsider ff as Function of df, rf by FUNCT_2:1;
reconsider gg as Function of dg, rg by FUNCT_2:1;
A2: a in D & b=[:ff,gg:].(a1,a2) by FUNCT_1:1, A1;
reconsider aa=a as Element of D by FUNCT_1:1, A1;
reconsider aaa=aa as Element of [:df,dg:] by FUNCT_3:def 8;
A3: {aaa`1}\df={} & {aaa`2}\dg={} & a`1=a1 & a`2=a2;
reconsider a1 as Element of df by A3;
reconsider a2 as Element of dg by A3;
b=[ff.a1, gg.a2] & [ff.a1,gg.a2]`1=ff.a1 & b`1=b1 &
[ff.a1,gg.a2]`2=gg.a2 & b`2=b2 by A2, FUNCT_3:75;
hence thesis by FUNCT_1:def 2;
end;
assume
A4: [a1, b1] in f & [a2,b2] in g; then
reconsider ff=f, gg=g as non empty Function; set df=dom f, dg=dom g;
a1 in df & b1=ff.a1 & a2 in dg & b2=gg.a2 by FUNCT_1:1, A4; then
[b1,b2] = F.(a1,a2) by FUNCT_3:def 8 .= F.[a1,a2]; then
F.[a1,a2]=[b1,b2] & [a1,a2] in dom F by FUNCT_1:def 2;
hence thesis by FUNCT_1:def 2;
end;
Lm74: X=Y iff for x st x in X\/Y holds (x in X iff x in Y)
proof
set Z=X\/Y; defpred W[object] means $1 in X iff $1 in Y;
thus X=Y implies for x st x in Z holds W[x];
assume
A1: for x st x in Z holds W[x];
now
let x be object;
per cases;
suppose x in Z; hence W[x] by A1;
end;
suppose not x in Z;
hence W[x] by XBOOLE_0:def 3;
end;
end;
hence thesis by TARSKI:2;
end;
Lm75: x in [:f,g:] implies x=[[x`1`1,x`1`2],[x`2`1,x`2`2]]
proof
set F=[:f,g:], y=x`1, z=x`2, x1=y`1, x2=y`2, x3=z`1, x4=z`2;
assume
A1: x in F; then reconsider F as non empty Function;
F<>{}; then reconsider ff=f as non empty Function;
F<>{}; then reconsider gg=g as non empty Function;
reconsider F=[:ff,gg:] as non empty Function by A1;
reconsider xx=x as Element of F by A1;
reconsider y=xx`1, z=xx`2 as pair object;
y=[y`1,y`2] & z=[z`1,z`2] & xx=[xx`1,xx`2];
hence thesis;
end;
Lm76: [:f1,f2:]/\[:g1,g2:]=[:(f1/\g1) qua Function, (f2/\g2) qua Function:]
proof
set H1=f1/\g1, H2=f2/\g2, F=[:f1,f2:], G=[:g1,g2:], lh=F/\G;
reconsider H1, H2 as Function; set rh=[:H1,H2:];
now
let x; set y=x`1, z=x`2, x1=y`1, x2=y`2, x3=z`1, x4=z`2, xx=[[x1,x2],[x3,x4]];
xx in lh iff xx in F & xx in G by XBOOLE_0:def 4; then xx in lh iff
([x1,x3] in f1 & [x1,x3] in g1 & [x2,x4] in f2 & [x2,x4] in g2) by Lm73; then
xx in lh iff ([x1,x3] in f1/\g1 & [x2,x4] in f2/\g2) by XBOOLE_0:def 4; then
A1: xx in lh iff xx in rh by Lm73;
assume x in lh \/ rh;
thus x in lh iff x in rh by A1, Lm75;
end;
hence thesis by Lm74;
end;
begin ::#oneone
definition
let P;
attr P is oneone means :Def34: P~ is Function-like;
end;
registration
cluster one-to-one -> oneone for Function;
coherence;
cluster oneone -> one-to-one for Function;
coherence
proof
let f be Function; set D=dom f; assume f is oneone; then reconsider
g=f~ as Function;
now
let x1, x2 be object; assume x1 in D & x2 in D & f.x1=f.x2; then
[x1,f.x1] in f & [x2,f.x1] in f by FUNCT_1:def 2; then
[f.x1,x1] in g & [f.x1,x2] in g by RELAT_1:def 7; hence
x1=x2 by FUNCT_1:def 1;
end;
hence thesis by FUNCT_1:def 4;
end;
end;
registration
cluster oneone for one-to-one Function;
existence proof take the one-to-one Function; thus thesis; end;
end;
registration
let P be oneone Relation;
cluster P~ -> Function-like;
coherence by Def34;
end;
registration
cluster non empty one-to-one for Function;
existence proof take id(the non empty set); thus thesis; end;
let P be oneone Relation;
cluster -> oneone for Subset of P;
coherence proof
let Q be Subset of P; Q~ c= P~ by SYSREL:11; hence thesis; end;
end;
begin ::# fixpoints
definition
let R be set;
func fixpoints R -> set equals proj1 (R /\ id (proj1 R));
coherence;
func fixpoints1 R -> set equals proj1 (R /\ id (proj1 R /\ proj2 R));
coherence;
end;
registration
let X; let R be Subset of id X;
reduce R~ to R;
reducibility
proof
set RR=id(X/\dom R), I=id X; A1: R=I|(dom R) by GRFUNC_1:23 .= RR
by Lm67; thus thesis by A1;
end;
end;
Lm77: fixpoints1 R = fixpoints1 (R~)
proof
set Q=R~, dq=dom Q, dr=dom R, rq=rng Q, rr=rng R,
iq=id(dq/\rq), ir=id(dr/\rr), r=R/\ir, q=Q/\iq;
reconsider r as Subset of ir;
dq=rr & rq=dr by RELAT_1:20; then
q=
Q/\(ir ~) .= r~ by RELAT_1:22 .= r; hence thesis;
end;
registration
let R;
cluster fixpoints1 (R~) \+\ fixpoints1 R -> empty;
coherence by Lm77, Th29;
end;
registration
let f be one-to-one Function;
cluster fixpoints1 (f") \+\ fixpoints1 f -> empty;
coherence proof f"=f~ by FUNCT_1:def 5; hence thesis; end;
end;
registration
let R be set;
identify fixpoints R with fixpoints1 R;
compatibility by Lm66;
identify fixpoints1 R with fixpoints R;
compatibility;
end;
Lm78:
for x being object holds x in fixpoints f iff x is_a_fixpoint_of f
proof let x be object;
set FP=fixpoints f, D=dom f, I=id D; reconsider g=f /\ I as Function;
set y=g.x; defpred P[object] means $1 is_a_fixpoint_of f;
FP\D = {} & FP \ dom I = {}; then
A1: FP c= D & FP c= dom I by Th29;
thus x in FP implies P[x]
proof
assume
A2: x in FP;
[x, y] in g by A2, FUNCT_1:def 2; then
y=f.x & y=I.x by FUNCT_1:def 2, A1, A2; then
f.x=x by FUNCT_1:17, A1, A2; hence P[x] by ABIAN:def 3, A1, A2;
end;
assume
A3: P[x]; then
A4: x in D & x in dom I & x=f.x by ABIAN:def 3;
x=f.x & x=I.x by A3, ABIAN:def 3, FUNCT_1:18; then
[x,x] in f & [x,x] in I by A4, FUNCT_1:def 2;
then [x,x] in g by XBOOLE_0:def 4; hence x in FP by XTUPLE_0:def 12;
end;
registration
let X;
reduce fixpoints (id X) to X;
reducibility; ::# WHY DOES THIS WORK?!
end;
Lm79: fixpoints [:f,g:] = [:fixpoints f, fixpoints g:]
proof
set h=[:f,g:], F=fixpoints f, G=fixpoints g, LH=fixpoints h, RH=[:F,G:],
df=dom f, dg=dom g; h/\ id dom h = h /\ id [:df,dg:] by FUNCT_3:def 8 .=
h/\[:id df, id dg:] by FUNCT_3:69 .= [:f/\id df, g/\id dg:] by Lm76;
hence LH =
RH by FUNCT_3:def 8;
end;
registration
let X be non empty set;
cluster id X -> with_fixpoint;
coherence
proof
set I=id X, x=the Element of X; x in fixpoints I;
hence thesis by ABIAN:def 5, Lm78;
end;
end;
registration
let X be non empty set;
cluster with_fixpoint non empty symmetric for Permutation of X;
existence proof take id X; thus thesis; end;
end;
registration
cluster with_fixpoint non empty symmetric for Function;
existence
proof
take the with_fixpoint non empty symmetric
Permutation of (the non empty set); thus thesis; end;
end;
registration
let f be with_fixpoint Function;
cluster dom f -> non empty;
coherence
proof
consider x being object such that
A1: x is_a_fixpoint_of f by ABIAN:def 5;
thus thesis by A1, ABIAN:def 3;
end;
end;
registration
cluster empty -> without_fixpoints for Function;
coherence proof dom {}={}; hence thesis; end;
end;
registration
cluster without_fixpoints empty for Function;
existence proof take {}; thus thesis; end;
end;
registration
let f be with_fixpoint Function;
cluster fixpoints f -> non empty;
coherence
proof
consider x being object such that
A1: x is_a_fixpoint_of f by ABIAN:def 5;
thus thesis by A1, Lm78;
end;
end;
registration
let f be without_fixpoints Function;
cluster fixpoints f -> empty;
coherence
by Lm78,ABIAN:def 5;
end;
begin ::# constanT
definition
let X;
attr X is constanT means :Def37: proj2 X is trivial;
end;
registration
cluster empty -> constanT for set;
coherence;
end;
registration
cluster empty constanT for Function;
existence proof take {}; thus thesis; end;
end;
registration
cluster constant -> constanT for Function;
coherence;
cluster constanT -> constant for Function;
coherence;
end;
Lm80: X is non empty trivial & P is X-valued implies
P is constant Function
proof
assume X is non empty trivial; then reconsider T=X as non empty trivial set;
consider t being Element of T such that
A1: T={t} by SUBSET_1:46; set d=dom P, r=rng P; reconsider f=[:d,{t}:] as
Function; assume P is X-valued; then reconsider r as Subset of {t}
by A1; [:d,r:] \ [:d\/{},{t} null r:]={}; then
P c= [:d,r:] & [:d,r:] c= f by RELAT_1:7, Th29;
then reconsider fP=P as Function-like Subset of f by XBOOLE_1:1;
rng fP \ rng f={} &
rng f\{t}={}; then rng fP c= rng f & rng f c= {t} by Th29;
hence thesis;
end;
registration
let x be trivial set;
cluster x-valued -> Function-like for Relation;
coherence
proof
let P;
per cases;
suppose
A1: x={}; assume P is x-valued;
hence thesis by A1;
end;
suppose
A2: not x={}; assume P is x-valued;
hence thesis by Lm80, A2;
end;
end;
end;
registration
let x be trivial set;
cluster x-valued -> constant for Function;
coherence;
end;
registration
let P; let Q be constanT Relation;
cluster P*Q -> constanT;
coherence proof set p2=rng P, q2=rng Q, R=P*Q, r2=rng R;
r2 c= q2 & q2 is trivial by RELAT_1:26, Def37;
hence thesis;
end;
end;
registration
cluster constanT -> Function-like for set;
coherence
proof
let X be set; set X2=proj2 X; assume
A1: X is constanT;
now
let x,y1,y2 be object; set a1=[x,y1], a2=[x,y2]; assume a1 in X & a2 in X;
then
y1 in X2 & y2 in X2 by XTUPLE_0:def 13; hence y1=y2
by A1, ZFMISC_1:def 10;
end; hence thesis by FUNCT_1:def 1;
end;
end;
registration
let P; let c be constanT Relation;
cluster P >*> c -> Function-like;
coherence;
end;
registration
let X,Y; let x be trivial set;
cluster [:X,Y:] >*> [:Y,x:] -> Function-like;
coherence;
end;
theorem x in fixpoints f iff x is_a_fixpoint_of f by Lm78; ::# Th69:
theorem a in {a1,f.a1} & f is involutive & a1 in dom f implies
{a,f.a}={a1,f.a1} by Lm69;
theorem ((a in {a1,f.a1} or f.a in {a1,f.a1}) & f is involutive &
a in dom f & a1 in dom f) implies {a,f.a}={a1,f.a1} by Lm70;
theorem f is involutive implies f*f c= id dom f by Lm65; ::# Th72
theorem y<>{} & y c= Y implies [:X,y:]*[:Y,Z:] = [:X,Z:] by Lm62;
theorem X<>{} implies the set of all x where x is Element of X = X
by Lm72; ::# Th74:
theorem rng f=dom f implies f is onto Function of dom f, dom f by Lm64;
theorem fixpoints [:f,g:] = [:fixpoints f, fixpoints g:] by Lm79; ::#Th76
theorem ::#Th77:
rng f1 /\ rng f2 = {} & b1<>b2 & rng f1 c= dom f2 & rng f2 c= dom f1
implies [:rng f1,{b2}:]\/[:rng f2,{b1}:] c=
((f1\/f2) >*> ([:rng f1,{b2}:]\/[:rng f2,{b1}:])) >*> ((b1,b2)-->(b2,b1))
by Lm68;
theorem X c= f implies dom (f\X)=dom f\proj1 X by Lm71; ::#Th78