:: Miscellaneous Facts about Functions
:: by Grzegorz Bancerek and Andrzej Trybulec
::
:: Received January 12, 1996
:: Copyright (c) 1996-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 NUMBERS, SUBSET_1, FUNCT_1, RELAT_1, TARSKI, XBOOLE_0, FUNCOP_1,
PBOOLE, ZFMISC_1, FUNCT_4, FINSEQ_1, ARYTM_3, CARD_1, NAT_1, XXREAL_0,
FINSET_1, SETFAM_1, FINSEQ_2, ORDINAL4, MCART_1, PARTFUN1, REWRITE1,
FUNCT_2, ARYTM_1, RFINSEQ, CLASSES1, FUNCT_7, VALUED_1, ORDINAL1;
notations TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, XTUPLE_0, SUBSET_1, CARD_1,
WELLORD2, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, SETFAM_1, PBOOLE,
DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, BINOP_1, FINSET_1, PARTFUN1,
FUNCOP_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FUNCT_4, CLASSES1, RFINSEQ, NAT_D,
REWRITE1, VALUED_1;
constructors SETFAM_1, PARTFUN1, WELLORD2, BINOP_1, DOMAIN_1, FUNCT_4,
XXREAL_0, NAT_1, INT_1, PBOOLE, RFINSEQ, NAT_D, REWRITE1, RELAT_2,
REAL_1, CLASSES1, RELSET_1, VALUED_1, FINSEQ_2, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1,
FUNCOP_1, FUNCT_4, XREAL_0, NAT_1, INT_1, CARD_1, FINSEQ_1, FUNCT_2,
RELSET_1, XXREAL_0, XTUPLE_0, FINSEQ_3;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1;
equalities TARSKI, RELAT_1, FUNCOP_1, BINOP_1, FINSEQ_2, FUNCT_4, ORDINAL1;
expansions TARSKI, XBOOLE_0, FUNCT_1, FUNCOP_1;
theorems FINSEQ_1, RELAT_1, TARSKI, AXIOMS, ZFMISC_1, INT_1, FUNCT_1,
FINSEQ_2, FUNCT_4, SUBSET_1, FINSET_1, CARD_1, NAT_1, FUNCT_2, FUNCOP_1,
SETFAM_1, FINSEQ_3, ENUMSET1, REWRITE1, FINSEQ_4, RELSET_1, XBOOLE_0,
XBOOLE_1, PARTFUN1, GRFUNC_1, XREAL_1, XXREAL_0, ORDINAL1, RFINSEQ,
FINSEQ_5, NAT_D, WELLORD2, VALUED_1, XTUPLE_0;
schemes NAT_1, DOMAIN_1, CLASSES1, FRAENKEL, FINSEQ_1, RECDEF_1, FUNCT_2;
begin :: Preliminaries
reserve a,x,y for object, A,B for set,
l,m,n for Nat;
theorem
for f being Function, X being set st rng f c= X holds (id X)*f = f
proof
let f be Function, X be set;
assume rng f c= X;
then reconsider g = f as Function of dom f, X by FUNCT_2:2;
(id X)*g = g by FUNCT_2:17;
hence thesis;
end;
theorem
for X being set, Y being non empty set, f being Function of X,Y st f
is one-to-one for B being Subset of X, C being Subset of Y st C c= f.:B holds f
"C c= B
proof
let X be set, Y be non empty set, f be Function of X,Y such that
A1: f is one-to-one;
let B be Subset of X, C be Subset of Y;
assume C c= f.:B;
then
A2: f"C c= f"(f.:B) by RELAT_1:143;
f"(f.:B) c= B by A1,FUNCT_1:82;
hence thesis by A2;
end;
theorem Th3:
for X,Y be non empty set, f being Function of X,Y st f is
one-to-one for x being Element of X, A being Subset of X st f.x in f.:A holds x
in A
proof
let X,Y be non empty set, f be Function of X,Y such that
A1: f is one-to-one;
let x be Element of X, A be Subset of X;
assume f.x in f.:A;
then ex y be Element of X st y in A & f.y = f.x by FUNCT_2:65;
hence thesis by A1,FUNCT_2:19;
end;
theorem Th4:
for X,Y be non empty set, f being Function of X,Y st f is
one-to-one for x being Element of X, A being Subset of X, B being Subset of Y
st f.x in f.:A \ B holds x in A \ f"B
proof
let X,Y be non empty set, f be Function of X,Y such that
A1: f is one-to-one;
let x be Element of X, A be Subset of X, B be Subset of Y;
assume
A2: f.x in f.:A \ B;
A3: now
assume x in f"B;
then f.x in B by FUNCT_1:def 7;
hence contradiction by A2,XBOOLE_0:def 5;
end;
f.x in f.:A by A2,XBOOLE_0:def 5;
then x in A by A1,Th3;
hence thesis by A3,XBOOLE_0:def 5;
end;
theorem
for X,Y be non empty set, f being Function of X,Y st f is one-to-one
for y being Element of Y, A being Subset of X, B being Subset of Y st y in f.:A
\ B holds f".y in A \ f"B
proof
let X,Y be non empty set, f be Function of X,Y such that
A1: f is one-to-one;
let y be Element of Y, A be Subset of X, B be Subset of Y;
assume
A2: y in f.:A \ B;
then
A3: y in f.:A by XBOOLE_0:def 5;
A4: f.:A c= rng f by RELAT_1:111;
then f".y in dom f by A1,A3,FUNCT_1:32;
then reconsider x = f".y as Element of X;
y = f.x by A1,A3,A4,FUNCT_1:35;
hence thesis by A1,A2,Th4;
end;
theorem Th6:
for f being Function, a being set st a in dom f holds f|{a} = a
.--> f.a
proof
let f be Function, a be set;
assume a in dom f;
hence f|{a} = {[a,f.a]} by GRFUNC_1:28
.= a .--> f.a by ZFMISC_1:29;
end;
registration
let x,y be object;
cluster x .--> y -> non empty;
coherence;
end;
registration
let x,y,a,b be object;
cluster (x,y) --> (a,b) -> non empty;
coherence;
end;
theorem Th7:
for I being set, M being ManySortedSet of I for i being set st i
in I holds i.--> (M.i) = M|{i}
proof
let I be set, M be ManySortedSet of I, i be set;
assume i in I;
then i in dom M by PARTFUN1:def 2;
hence thesis by Th6;
end;
theorem
for I,J being set, M being ManySortedSet of [:I,J:] for i,j being set
st i in I & j in J holds (i,j):-> (M.(i,j)) = M|([:{i},{j}:] qua set)
proof
let I,J be set, M be ManySortedSet of [:I,J:];
let i,j be set;
assume i in I & j in J;
then
A1: [i,j] in [:I,J:] by ZFMISC_1:87;
thus (i,j):-> (M.(i,j)) = [i,j].--> (M.[i,j])
.= M|({[i,j]} qua set) by A1,Th7
.= M|([:{i},{j}:] qua set) by ZFMISC_1:29;
end;
theorem Th9:
for f,g,h being Function st rng h c= dom f holds f*(g +* h) = (f
*g) +* (f*h)
proof
let f,g,h be Function such that
A1: rng h c= dom f;
A2: dom h c= dom(g+*h) by FUNCT_4:10;
A3: dom g c= dom(g+*h) by FUNCT_4:10;
A4: dom(f*(g +* h)) = dom(f*g) \/ dom(f*h)
proof
thus dom(f*(g +* h)) c= dom(f*g) \/ dom(f*h)
proof
let x be object;
assume
A5: x in dom(f*(g +* h));
then
A6: (g +* h).x in dom f by FUNCT_1:11;
x in dom(g +* h) by A5,FUNCT_1:11;
then
A7: x in dom g \/ dom h by FUNCT_4:def 1;
per cases;
suppose
A8: x in dom h;
then h.x in dom f by A6,FUNCT_4:13;
then x in dom(f*h) by A8,FUNCT_1:11;
hence thesis by XBOOLE_0:def 3;
end;
suppose
not x in dom h;
then g.x in dom f & x in dom g by A7,A6,FUNCT_4:11,XBOOLE_0:def 3;
then x in dom(f*g) by FUNCT_1:11;
hence thesis by XBOOLE_0:def 3;
end;
end;
let x be object;
assume
A9: x in dom(f*g) \/ dom(f*h);
per cases;
suppose
A10: x in dom(f*h);
then
A11: h.x in dom f by FUNCT_1:11;
A12: x in dom h by A10,FUNCT_1:11;
then (g +* h).x = h.x by FUNCT_4:13;
hence thesis by A2,A12,A11,FUNCT_1:11;
end;
suppose
A13: not x in dom(f*h);
x in dom h implies h.x in dom f
proof
assume x in dom h;
then h.x in rng h by FUNCT_1:3;
hence thesis by A1;
end;
then not x in dom h by A13,FUNCT_1:11;
then
A14: (g +* h).x = g.x by FUNCT_4:11;
x in dom(f*g) by A9,A13,XBOOLE_0:def 3;
then g.x in dom f & x in dom g by FUNCT_1:11;
hence thesis by A3,A14,FUNCT_1:11;
end;
end;
now
let x be object;
assume
A15: x in dom(f*g) \/ dom(f*h);
thus x in dom(f*h) implies (f*(g +* h)).x = (f*h).x
proof
assume x in dom(f*h);
then
A16: x in dom h by FUNCT_1:11;
hence (f*(g +* h)).x = f.((g +* h).x) by A2,FUNCT_1:13
.= f.(h.x) by A16,FUNCT_4:13
.= (f*h).x by A16,FUNCT_1:13;
end;
assume
A17: not x in dom(f*h);
x in dom h implies h.x in dom f
proof
assume x in dom h;
then h.x in rng h by FUNCT_1:3;
hence thesis by A1;
end;
then
A18: not x in dom h by A17,FUNCT_1:11;
x in dom(f*g) by A15,A17,XBOOLE_0:def 3;
then
A19: x in dom g by FUNCT_1:11;
hence (f*(g +* h)).x = f.((g +* h).x) by A3,FUNCT_1:13
.= f.(g.x) by A18,FUNCT_4:11
.= (f*g).x by A19,FUNCT_1:13;
end;
hence thesis by A4,FUNCT_4:def 1;
end;
theorem Th10:
for f,g,h being Function holds (g +* h)*f = (g*f) +* (h*f)
proof
let f,g,h be Function;
A1: dom((g +* h)*f) = dom(g*f) \/ dom(h*f)
proof
thus dom((g +* h)*f) c= dom(g*f) \/ dom(h*f)
proof
let x be object;
assume
A2: x in dom((g +* h)*f);
then f.x in dom(g +* h) by FUNCT_1:11;
then f.x in dom g \/ dom h by FUNCT_4:def 1;
then
A3: f.x in dom g or f.x in dom h by XBOOLE_0:def 3;
x in dom f by A2,FUNCT_1:11;
then x in dom(g*f) or x in dom(h*f) by A3,FUNCT_1:11;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume x in dom(g*f) \/ dom(h*f);
then
A4: x in dom(g*f) or x in dom(h*f) by XBOOLE_0:def 3;
then f.x in dom g or f.x in dom h by FUNCT_1:11;
then f.x in dom g \/ dom h by XBOOLE_0:def 3;
then
A5: f.x in dom(g +* h) by FUNCT_4:def 1;
x in dom f by A4,FUNCT_1:11;
hence thesis by A5,FUNCT_1:11;
end;
now
let x be object;
assume x in dom(g*f) \/ dom(h*f);
then x in dom(g*f) or x in dom(h*f) by XBOOLE_0:def 3;
then
A6: x in dom f by FUNCT_1:11;
hereby
assume
A7: x in dom(h*f);
then
A8: f.x in dom h by FUNCT_1:11;
thus ((g +* h)*f).x = (g +* h).(f.x) by A6,FUNCT_1:13
.= h.(f.x) by A8,FUNCT_4:13
.= (h*f).x by A7,FUNCT_1:12;
end;
assume not x in dom(h*f);
then
A9: not f.x in dom h by A6,FUNCT_1:11;
thus ((g +* h)*f).x = (g +* h).(f.x) by A6,FUNCT_1:13
.= g.(f.x) by A9,FUNCT_4:11
.= (g*f).x by A6,FUNCT_1:13;
end;
hence thesis by A1,FUNCT_4:def 1;
end;
theorem
for f,g,h being Function st rng f misses dom g holds (h +* g)*f = h*f
proof
let f,g,h be Function;
assume
A1: rng f misses dom g;
thus (h +* g)*f = (h*f) +* (g*f) by Th10
.= h*f +* {} by A1,RELAT_1:44
.= h*f;
end;
theorem Th12:
for A,B be set, y be set st A meets rng(id B +* (A --> y)) holds
y in A
proof
let A,B be set, y be set;
assume A meets rng(id B +* (A --> y));
then consider x being object such that
A1: x in A and
A2: x in rng(id B +* (A --> y)) by XBOOLE_0:3;
consider z being object such that
A3: z in dom(id B +* (A --> y)) and
A4: (id B +* (A --> y)).z = x by A2,FUNCT_1:def 3;
A5: z in dom id B \/ dom(A --> y) by A3,FUNCT_4:def 1;
per cases;
suppose
A6: z in dom(A --> y);
then y = (A --> y).z by FUNCOP_1:7
.= x by A4,A6,FUNCT_4:13;
hence thesis by A1;
end;
suppose
A7: not z in dom(A --> y);
then
A8: z in dom id B by A5,XBOOLE_0:def 3;
x = (id B).z by A4,A7,FUNCT_4:11
.= z by A8,FUNCT_1:18;
hence thesis by A1,A7;
end;
end;
theorem
for x,y be set, A be set st x <> y holds not x in rng(id A +* (x .-->
y))
proof
let x,y be set, A be set;
assume x <> y;
then not y in {x} by TARSKI:def 1;
then {x} misses rng(id A +* ({x} --> y)) by Th12;
hence thesis by ZFMISC_1:48;
end;
theorem
for X being set, a being set, f being Function st dom f = X \/ {a}
holds f = f|X +* (a .--> f.a)
proof
let X be set, a be set, f be Function;
assume
A1: dom f = X \/ {a};
a in {a} by TARSKI:def 1;
then
A2: a in dom f by A1,XBOOLE_0:def 3;
thus f = f|X +* f|{a} by A1,FUNCT_4:70
.= f|X +* (a .--> f.a) by A2,Th6;
end;
theorem
for f being Function, X,y,z being set holds (f+*(X-->y))+*(X-->z) = f
+*(X-->z)
proof
let f be Function, X,y,z be set;
A1: dom (X-->z) = X;
A2: dom (X-->y) = X;
then dom (f+*(X-->y)) = dom f \/ X by FUNCT_4:def 1;
then
A3: dom ((f+*(X-->y))+*(X-->z)) = (dom f \/ X) \/ X by A1,FUNCT_4:def 1
.= dom f \/ (X \/ X) by XBOOLE_1:4
.= dom f \/ X;
A4: now
let x be object;
assume x in dom f \/ X;
per cases;
suppose
A5: x in X;
then ((f+*(X-->y))+*(X-->z)).x = (X-->z).x by A1,FUNCT_4:13;
hence ((f+*(X-->y))+*(X-->z)).x = (f+*(X-->z)).x by A1,A5,FUNCT_4:13;
end;
suppose
A6: not x in X;
then ((f+*(X-->y))+*(X-->z)).x = (f+*(X-->y)).x by A1,FUNCT_4:11;
then ((f+*(X-->y))+*(X-->z)).x = f.x by A2,A6,FUNCT_4:11;
hence ((f+*(X-->y))+*(X-->z)).x = (f+*(X-->z)).x by A1,A6,FUNCT_4:11;
end;
end;
dom (f+*(X-->z)) = dom f \/ X by A1,FUNCT_4:def 1;
hence thesis by A3,A4;
end;
theorem
INT <> INT*
proof
now
A1: {} in 1 by CARD_1:49,TARSKI:def 1;
assume 1 in INT*;
then ex x,y being object st {} = [x,y] by A1,RELAT_1:def 1;
hence contradiction;
end;
hence thesis by INT_1:def 2;
end;
theorem
{}* = {{}}
proof
thus {}* c= {{}}
proof
let x be object;
assume x in {}*;
then reconsider f = x as FinSequence of {} by FINSEQ_1:def 11;
now
assume x <> {};
then ex x st x in dom f;
hence contradiction;
end;
hence thesis by ZFMISC_1:31;
end;
let x be object;
assume x in {{}};
then
A1: x = {} by TARSKI:def 1;
rng {} = {};
then x is FinSequence of {} by A1,FINSEQ_1:def 4;
hence thesis by FINSEQ_1:def 11;
end;
theorem Th18:
for x being object holds <*x*> in A* iff x in A
proof let x be object;
rng <*x*> = {x} by FINSEQ_1:38;
then {x} c= A iff <*x*> is FinSequence of A by FINSEQ_1:def 4;
hence thesis by FINSEQ_1:def 11,ZFMISC_1:31;
end;
theorem
A* c= B* implies A c= B
proof
assume
A1: A* c= B*;
let x be object;
assume x in A;
then <*x*> in A* by Th18;
hence thesis by A1,Th18;
end;
theorem
for A being Subset of NAT st for n,m st n in A & m < n holds m in A
holds A is Cardinal
proof
let A be Subset of NAT such that
A1: for n,m st n in A & m < n holds m in A;
per cases;
suppose
A = {};
hence thesis;
end;
suppose that
A2: A <> {} and
A3: ex m being Nat st for n being Nat st n in A holds n <= m;
defpred P[set] means $1 in A;
consider M being Nat such that
A4: for n being Nat st P[n] holds n <= M by A3;
ex m being Element of NAT st P[m] by A2,SUBSET_1:4;
then
A5: ex m being Nat st P[m];
consider m being Nat such that
A6: P[m] and
A7: for n being Nat st P[n] holds n <= m from NAT_1:sch 6(A4,A5);
A = { l where l is Nat : l < m+1 }
proof
thus A c= { l where l is Nat : l < m+1 }
proof
let x be object;
assume
A8: x in A;
then reconsider l = x as Nat;
l <= m by A7,A8;
then l < m+1 by NAT_1:13;
hence thesis;
end;
let x be object;
assume x in { l where l is Nat : l < m+1 };
then consider l being Nat such that
A9: x = l and
A10: l < m+1;
reconsider l as Nat;
l <= m by A10,NAT_1:13;
then l < m or l = m by XXREAL_0:1;
hence thesis by A1,A6,A9;
end;
hence thesis by AXIOMS:4;
end;
suppose
A11: for m being Nat ex n being Nat st n in A & n > m;
NAT c= A
proof
let x be object;
assume x in NAT;
then reconsider m = x as Nat;
ex n being Nat st n in A & n > m by A11;
hence thesis by A1;
end;
hence thesis by XBOOLE_0:def 10;
end;
end;
theorem
for A being finite set, X being non empty Subset-Family of A ex C
being Element of X st for B being Element of X holds B c= C implies B = C
proof
let A be finite set, X be non empty Subset-Family of A;
reconsider D = COMPLEMENT X as non empty Subset-Family of A by SETFAM_1:32;
consider x being set such that
A1: x in D and
A2: for B being set st B in D holds x c= B implies B = x by FINSET_1:6;
reconsider x as Subset of A by A1;
reconsider C = x` as Element of X by A1,SETFAM_1:def 7;
take C;
let B be Element of X such that
A3: B c= C;
B`` = B;
then B` in D by SETFAM_1:def 7;
then B` = x by A2,A3,SUBSET_1:16;
hence thesis;
end;
theorem Th22:
for p,q being FinSequence st len p = len q+1
for i being Nat holds i in dom q iff i in dom p & i+1 in dom p
proof
let p,q be FinSequence;
assume
A1: len p = len q+1;
let i be Nat;
hereby
assume
A2: i in dom q;
then
A3: i >= 1 by FINSEQ_3:25;
A4: i <= len q by A2,FINSEQ_3:25;
len q <= len p by A1,NAT_1:11;
then
A5: i+1 >= 1 & i <= len p by A4,NAT_1:11,XXREAL_0:2;
i+1 <= len p by A1,A4,XREAL_1:6;
hence i in dom p & i+1 in dom p by A3,A5,FINSEQ_3:25;
end;
assume that
A6: i in dom p and
A7: i+1 in dom p;
i+1 <= len p by A7,FINSEQ_3:25;
then
A8: i <= len q by A1,XREAL_1:6;
i >= 1 by A6,FINSEQ_3:25;
hence thesis by A8,FINSEQ_3:25;
end;
registration
cluster Function-yielding non empty non-empty for FinSequence;
existence
proof
take p = <*<*0 qua set*>*>;
A1: dom p = {1} & p.1 = <*0*> by FINSEQ_1:2,38;
thus p is Function-yielding;
thus p is non empty;
let x be object;
assume x in dom p;
hence thesis by A1,TARSKI:def 1;
end;
end;
registration
cluster empty -> Function-yielding for Function;
coherence;
end;
registration
let n be Nat, f be Function;
cluster n |-> f -> Function-yielding;
coherence;
end;
registration
let p,q be Function-yielding FinSequence;
cluster p^q -> Function-yielding;
coherence
proof
let x be object;
assume
A1: x in dom (p^q);
then reconsider i = x as Nat;
per cases;
suppose
i in dom p;
then p.i = (p^q).i by FINSEQ_1:def 7;
hence thesis;
end;
suppose
not i in dom p;
then consider j being Nat such that
A2: j in dom q & i = len p+j by A1,FINSEQ_1:25;
q.j = (p^q).i by A2,FINSEQ_1:def 7;
hence thesis;
end;
end;
end;
theorem Th23:
for p,q being FinSequence st p^q is Function-yielding holds p is
Function-yielding & q is Function-yielding
proof
let p,q be FinSequence;
assume
A1: for x being object st x in dom (p^q) holds (p^q).x is Function;
hereby
let x be object;
assume
A2: x in dom p;
then (p^q).x = p.x by FINSEQ_1:def 7;
hence p.x is Function by A1,A2,FINSEQ_3:22;
end;
let x be object;
assume
A3: x in dom q;
then reconsider i = x as Nat;
(p^q).(len p+i) = q.x by A3,FINSEQ_1:def 7;
hence thesis by A1,A3,FINSEQ_1:28;
end;
begin :: Some useful schemes
scheme
Kappa2D{ X,Y,Z()->non empty set,F(Element of X(),Element of Y())->object}:
ex f being Function of [:X(),Y():], Z() st
for x being Element of X(), y being Element of Y() holds f.(x,y)=F(x,y)
provided
A1: for x being Element of X(), y being Element of Y() holds F(x,y) in Z
()
proof
deffunc G(Element of [:X(),Y():]) = F($1`1,$1`2);
A2: for p being Element of [:X(),Y():] holds G(p) in Z() by A1;
consider f being Function of [:X(),Y():], Z() such that
A3: for p being Element of [:X(),Y():] holds f.p = G(p) from FUNCT_2:sch
8(A2);
take f;
let x be Element of X(), y be Element of Y();
[x,y]`1 = x & [x,y]`2 = y;
hence thesis by A3;
end;
scheme
FinMono{ A() -> set, D() -> non empty set, F,G(object) -> object }:
{ F(d) where d
is Element of D() : G(d) in A() } is finite
provided
A1: A() is finite and
A2: for d1,d2 being Element of D() st G(d1) = G(d2) holds d1 = d2
proof
per cases;
suppose
A3: A() = {};
now
set a =the Element of { F(d) where d is Element of D() : G(d) in A () };
assume { F(d) where d is Element of D() : G(d) in A() } <> {};
then a in { F(d) where d is Element of D() : G(d) in A() };
then ex d being Element of D() st a = F(d) & G(d) in A();
hence contradiction by A3;
end;
hence thesis;
end;
suppose
A() <> {};
then reconsider D = A() as non empty set;
defpred R[set] means ex d being Element of D() st $1 = G(d);
set B = { d where d is Element of D() : G(d) in D}, C = { a where a is
Element of D: R[a]};
A4: { F(d) where d is Element of D() : G(d) in A() } = { F(d) where d is
Element of D(): d in B}
proof
thus { F(d) where d is Element of D() : G(d) in A() } c= { F(d) where d
is Element of D(): d in B}
proof
let x be object;
assume x in { F(d) where d is Element of D() : G(d) in A() };
then consider d9 being Element of D() such that
A5: x = F(d9) and
A6: G(d9) in A();
d9 in B by A6;
hence thesis by A5;
end;
let x be object;
assume x in { F(d) where d is Element of D(): d in B};
then consider d1 being Element of D() such that
A7: x = F(d1) and
A8: d1 in B;
ex d3 being Element of D() st d3 = d1 & G(d3) in D by A8;
hence thesis by A7;
end;
A9: C,B are_equipotent
proof
take Z = the set of all [G(d),d] where d is Element of D();
hereby
let x be object;
assume x in C;
then consider a being Element of D such that
A10: a = x and
A11: ex d being Element of D() st a = G(d);
consider d being Element of D() such that
A12: a = G(d) by A11;
reconsider d as object;
take d;
thus d in B & [x,d] in Z by A10,A12;
end;
hereby
let y be object;
assume y in B;
then consider d being Element of D() such that
A13: d = y & G(d) in D;
reconsider x = G(d) as object;
take x;
thus x in C & [x,y] in Z by A13;
end;
let x,y,z,u be object;
assume [x,y] in Z;
then consider d1 being Element of D() such that
A14: [x,y] = [G(d1),d1];
assume [z,u] in Z;
then consider d2 being Element of D() such that
A15: [z,u] = [G(d2),d2];
A16: z = G(d2) & u = d2 by A15,XTUPLE_0:1;
x = G(d1) & y = d1 by A14,XTUPLE_0:1;
hence thesis by A2,A16;
end;
C is Subset of D from DOMAIN_1:sch 7;
then C is finite by A1,FINSET_1:1;
then
A17: B is finite by A9,CARD_1:38;
{ F(d) where d is Element of D(): d in B} is finite from FRAENKEL:sch
21(A17);
hence thesis by A4;
end;
end;
scheme
CardMono{ A() -> set, D() -> non empty set, G(object) -> object }:
A(),{ d where d is Element of D() : G(d) in A() } are_equipotent
provided
A1: for x being set st x in A() ex d being Element of D() st x = G(d) and
A2: for d1,d2 being Element of D() st G(d1) = G(d2) holds d1 = d2
proof
set D = { d where d is Element of D() : G(d) in A() };
per cases;
suppose
A3: A() = {};
now
set a =the Element of D;
assume D <> {};
then a in D;
then ex d being Element of D() st a = d & G(d) in A();
hence contradiction by A3;
end;
hence thesis by A3;
end;
suppose
A() <> {};
then reconsider A = A() as non empty set;
A,D are_equipotent
proof
take Z = the set of all [G(d),d] where d is Element of D();
hereby
let x be object;
assume
A4: x in A;
then consider d being Element of D() such that
A5: x = G(d) by A1;
reconsider d as object;
take d;
thus d in D by A4,A5;
thus [x,d] in Z by A5;
end;
hereby
let y be object;
assume y in D;
then consider d being Element of D() such that
A6: d = y & G(d) in A;
reconsider x = G(d) as object;
take x;
thus x in A & [x,y] in Z by A6;
end;
let x,y,z,u be object;
assume [x,y] in Z;
then consider d1 being Element of D() such that
A7: [x,y] = [G(d1),d1];
assume [z,u] in Z;
then consider d2 being Element of D() such that
A8: [z,u] = [G(d2),d2];
A9: z = G(d2) & u = d2 by A8,XTUPLE_0:1;
x = G(d1) & y = d1 by A7,XTUPLE_0:1;
hence thesis by A2,A9;
end;
hence thesis;
end;
end;
scheme
CardMono9{ A() -> set, D() -> non empty set, G(object) -> object }:
A(),{ G(d) where d is Element of D() : d in A() } are_equipotent
provided
A1: A() c= D() and
A2: for d1,d2 being Element of D() st G(d1) = G(d2) holds d1 = d2;
per cases;
suppose
A3: A() = {};
now
set a =the Element of { G(d) where d is Element of D() : d in A() };
assume { G(d) where d is Element of D() : d in A() } <> {};
then a in { G(d) where d is Element of D() : d in A() };
then ex d being Element of D() st a = G(d) & d in A();
hence contradiction by A3;
end;
hence thesis by A3;
end;
suppose
A() <> {};
then reconsider A = A() as non empty set;
set D = { G(d) where d is Element of D() : d in A };
A,D are_equipotent
proof
take Z = the set of all [d,G(d)] where d is Element of D();
hereby
let x be object;
assume
A4: x in A;
then reconsider d = x as Element of D() by A1;
reconsider y = G(d) as object;
take y;
thus y in D by A4;
thus [x,y] in Z;
end;
hereby
let y be object;
assume y in D;
then consider d being Element of D() such that
A5: G(d) = y & d in A;
reconsider d as object;
take d;
thus d in A & [d,y] in Z by A5;
end;
let x,y,z,u be object;
assume [x,y] in Z;
then consider d1 being Element of D() such that
A6: [x,y] = [d1,G(d1)];
assume [z,u] in Z;
then consider d2 being Element of D() such that
A7: [z,u] = [d2,G(d2)];
A8: z = d2 & u = G(d2) by A7,XTUPLE_0:1;
x = d1 & y = G(d1) by A6,XTUPLE_0:1;
hence thesis by A2,A8;
end;
hence thesis;
end;
end;
scheme
FuncSeqInd {P[object]}: for p being Function-yielding FinSequence holds P[p]
provided
A1: P[ {} ] and
A2: for p being Function-yielding FinSequence st P[p] for f being
Function holds P[p^<*f*>]
proof
defpred R[FinSequence] means $1 is Function-yielding implies P[ $1];
A3: for p being FinSequence, x being object st R[p] holds R[p^<*x*>]
proof
let p be FinSequence, x be object such that
A4: p is Function-yielding implies P[p] and
A5: p^<*x*> is Function-yielding;
A6: <*x*>.1 = x;
p is Function-yielding & <*x*> is Function-yielding by A5,Th23;
hence thesis by A2,A4,A6;
end;
A7: R[{}] by A1;
for p being FinSequence holds R[p] from FINSEQ_1:sch 3(A7,A3);
hence thesis;
end;
begin :: Some auxiliary concepts
definition
::$CD
let f,g be Function;
let A be set;
pred f,g equal_outside A means
f|(dom f \ A) = g|(dom g \ A);
end;
::$CT
theorem
for f be Function, A be set holds f,f equal_outside A;
theorem Th25:
for f,g be Function, A be set st f,g equal_outside A holds g,f
equal_outside A;
theorem
for f,g,h be Function, A be set st f,g equal_outside A & g,h
equal_outside A holds f,h equal_outside A;
theorem Th27:
for f,g be Function, A be set st f,g equal_outside A holds dom f
\ A = dom g \ A
proof
let f,g be Function, A be set;
assume
A1: f|(dom f \ A) = g|(dom g \ A);
thus dom f \ A = dom f /\ (dom f \ A) by XBOOLE_1:28
.= dom(f|(dom f \ A)) by RELAT_1:61
.= dom g /\ (dom g \ A) by A1,RELAT_1:61
.= dom g \ A by XBOOLE_1:28;
end;
theorem Th28:
for f,g being Function, A be set st dom g c= A holds f, f +* g
equal_outside A
proof
let f,g be Function, A be set;
assume
A1: dom g c= A;
A2: dom(f +* g) \ A = (dom f \/ dom g) \ A by FUNCT_4:def 1
.= dom f \ A \/ (dom g \ A) by XBOOLE_1:42
.= dom f \ A \/ {} by A1,XBOOLE_1:37
.= dom f \ A;
dom f \ A misses A by XBOOLE_1:79;
then dom f \ A misses dom g by A1,XBOOLE_1:63;
hence f|(dom f \ A) = (f +* g)|(dom(f +* g) \ A) by A2,FUNCT_4:72;
end;
definition
let f be Function, i, x be object;
func f+*(i,x) -> Function equals
:Def2:
f+*(i.-->x) if i in dom f otherwise
f;
correctness;
end;
theorem Th29:
for f be Function, d,i be object holds dom(f+*(i,d)) = dom f
proof
let f be Function, x,i be object;
per cases;
suppose
A1: i in dom f;
then
A2: {i} c= dom f by ZFMISC_1:31;
thus dom(f+*(i,x)) = dom(f+*(i.-->x)) by A1,Def2
.= dom f \/ dom(i.-->x) by FUNCT_4:def 1
.= dom f \/ {i}
.= dom f by A2,XBOOLE_1:12;
end;
suppose
not i in dom f;
hence thesis by Def2;
end;
end;
registration
let f be empty Function, i, x be object;
cluster f+*(i,x) -> empty;
coherence
proof
dom f is empty;
then dom(f+*(i,x)) is empty by Th29;
hence thesis;
end;
end;
registration
let f be non empty Function, i, x be object;
cluster f+*(i,x) -> non empty;
coherence
proof
dom f is non empty;
then dom(f+*(i,x)) is non empty by Th29;
hence thesis;
end;
end;
theorem Th30:
for f be Function, d,i be object st i in dom f holds (f+*(i,d)).i = d
proof
let f be Function, d,i be object;
A1: i in dom(i.-->d) by TARSKI:def 1;
assume i in dom f;
hence (f+*(i,d)).i = (f+*(i.-->d)).i by Def2
.= (i.-->d).i by A1,FUNCT_4:13
.= d by FUNCOP_1:72;
end;
theorem Th31:
for f be Function, d,i,j be object st i <> j holds (f+*(i,d)).j = f.j
proof
let f be Function, d,i,j be object such that
A1: i <> j;
A2: not j in dom(i.-->d) by A1,TARSKI:def 1;
per cases;
suppose
i in dom f;
hence (f+*(i,d)).j = (f+*(i.-->d)).j by Def2
.= f.j by A2,FUNCT_4:11;
end;
suppose
not i in dom f;
hence thesis by Def2;
end;
end;
theorem
for f be Function, d,e,i,j be set st i <> j holds f+*(i,d)+*(j,e) = f
+*(j,e)+*(i,d)
proof
let f be Function, d,e,i,j be set such that
A1: i <> j;
per cases;
suppose that
A2: i in dom f and
A3: j in dom f;
A4: i in dom(f+*(j,e)) by A2,Th29;
A5: dom(i.-->d) = {i} & dom(j.-->e) = {j};
j in dom(f+*(i,d)) by A3,Th29;
hence f+*(i,d)+*(j,e) = f+*(i,d)+*(j.-->e) by Def2
.= f+*(i.-->d)+*(j.-->e) by A2,Def2
.= f+*((i.-->d)+*(j.-->e)) by FUNCT_4:14
.= f+*((j.-->e)+*(i.-->d)) by A1,A5,FUNCT_4:35,ZFMISC_1:11
.= f+*(j.-->e)+*(i.-->d) by FUNCT_4:14
.= f+*(j,e)+*(i.-->d) by A3,Def2
.= f+*(j,e)+*(i,d) by A4,Def2;
end;
suppose that
i in dom f and
A6: not j in dom f;
not j in dom(f+*(i,d)) by A6,Th29;
hence f+*(i,d)+*(j,e) = f+*(i,d) by Def2
.= f+*(j,e)+*(i,d) by A6,Def2;
end;
suppose that
A7: not i in dom f and
j in dom f;
A8: not i in dom(f+*(j,e)) by A7,Th29;
thus f+*(i,d)+*(j,e) = f+*(j,e) by A7,Def2
.= f+*(j,e)+*(i,d) by A8,Def2;
end;
suppose that
A9: not i in dom f and
A10: not j in dom f;
A11: not i in dom(f+*(j,e)) by A9,Th29;
not j in dom(f+*(i,d)) by A10,Th29;
hence f+*(i,d)+*(j,e) = f+*(i,d) by Def2
.= f by A9,Def2
.= f+*(j,e) by A10,Def2
.= f+*(j,e)+*(i,d) by A11,Def2;
end;
end;
theorem
for f be Function, d,e,i be set holds f+*(i,d)+*(i,e) = f+*(i,e)
proof
let f be Function, d,e,i be set;
A1: dom(i.-->d) = {i}
.= dom(i.-->e);
per cases;
suppose
A2: i in dom f;
then i in dom(f+*(i,d)) by Th29;
hence f+*(i,d)+*(i,e) = f+*(i,d)+*(i.-->e) by Def2
.= f+*(i.-->d)+*(i.-->e) by A2,Def2
.= f+*((i.-->d)+*(i.-->e)) by FUNCT_4:14
.= f+*(i.-->e) by A1,FUNCT_4:19
.= f+*(i,e) by A2,Def2;
end;
suppose
not i in dom f;
hence thesis by Def2;
end;
end;
theorem Th34:
for f be Function, i be set holds f+*(i,f.i) = f
proof
let f be Function, i be set;
per cases;
suppose
A1: i in dom f;
then
A2: i.-->f.i = f|{i} by Th6;
thus f+*(i,f.i) = f +*(i.-->f.i) by A1,Def2
.= f by A2,FUNCT_4:75;
end;
suppose
not i in dom f;
hence thesis by Def2;
end;
end;
registration
let f be FinSequence, i,x be object;
cluster f+*(i,x) -> FinSequence-like;
coherence
proof
dom(f+*(i,x)) = dom f by Th29
.= Seg len f by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 2;
end;
end;
definition
let D be set, f be FinSequence of D, i be Nat, d be Element of D;
redefine func f+*(i,d) -> FinSequence of D; :: redefines +* (FUNCT_7, definition)
coherence
proof
per cases;
suppose
A1: i in dom f;
then f.i in rng f by FUNCT_1:def 3;
then {d} c= D by ZFMISC_1:31;
then
A2: rng f \/ rng(i.-->d) = rng f \/ {d} & rng f \/ {d} c= D by FUNCOP_1:8
,XBOOLE_1:8;
f+*(i,d) = f+*(i.-->d) by A1,Def2;
then rng(f+*(i,d)) c= rng f \/ rng(i.-->d) by FUNCT_4:17;
then rng(f+*(i,d)) c= D by A2;
hence thesis by FINSEQ_1:def 4;
end;
suppose
not i in dom f;
hence thesis by Def2;
end;
end;
end;
theorem
for D be non empty set, f be FinSequence of D, d be Element of D, i be
Nat st i in dom f holds (f+*(i,d))/.i = d
proof
let D be non empty set, f be FinSequence of D, d be Element of D, i be
Nat;
assume
A1: i in dom f;
then i in dom(f+*(i,d)) by Th29;
hence (f+*(i,d))/.i = (f+*(i,d)).i by PARTFUN1:def 6
.= d by A1,Th30;
end;
theorem
for D be non empty set, f be FinSequence of D, d be Element of D, i,j
be Nat st i <> j & j in dom f holds (f+*(i,d))/.j = f/.j
proof
let D be non empty set, f be FinSequence of D, d be Element of D, i,j be
Nat such that
A1: i <> j and
A2: j in dom f;
j in dom(f+*(i,d)) by A2,Th29;
hence (f+*(i,d))/.j = (f+*(i,d)).j by PARTFUN1:def 6
.= f.j by A1,Th31
.= f/.j by A2,PARTFUN1:def 6;
end;
theorem
for D be non empty set, f be FinSequence of D, d,e be Element of D, i
be Nat holds f+*(i,f/.i) = f
proof
let D be non empty set, f be FinSequence of D, d,e be Element of D, i be
Nat;
per cases;
suppose
i in dom f;
hence f+*(i,f/.i) = f+*(i,f.i) by PARTFUN1:def 6
.= f by Th34;
end;
suppose
not i in dom f;
hence thesis by Def2;
end;
end;
begin :: On the composition of a finite sequence of functions
definition
let X be set;
let p be Function-yielding FinSequence;
func compose(p,X) -> Function means
: Def3:
ex f being ManySortedFunction of
NAT st it = f.len p & f.0 = id X & for i being Nat st i+1 in dom p
for g,h being Function st g = f.i & h = p.(i+1) holds f.(i+1) = h*g;
uniqueness
proof
let g1,g2 be Function;
given f1 being ManySortedFunction of NAT such that
A1: g1 = f1.len p and
A2: f1.0 = id X and
A3: for i being Nat st i+1 in dom p for g,h being Function
st g = f1.i & h = p.(i+1) holds f1.(i+1) = h*g;
given f2 being ManySortedFunction of NAT such that
A4: g2 = f2.len p and
A5: f2.0 = id X and
A6: for i being Nat st i+1 in dom p for g,h being Function
st g = f2.i & h = p.(i+1) holds f2.(i+1) = h*g;
defpred R[Nat] means $1 <= len p implies f1.$1 = f2.$1 & f1.$1
is Function;
A7: for i being Nat st R[i] holds R[i+1]
proof
let i be Nat such that
A8: i <= len p implies f1.i = f2.i & f1.i is Function and
A9: i+1 <= len p;
reconsider h = p.(i+1) as Function;
reconsider g = f1.i as Function;
i+1 >= 1 by NAT_1:11;
then
A10: i+1 in dom p by A9,FINSEQ_3:25;
then f1.(i+1) = h*g by A3;
hence thesis by A6,A8,A9,A10,NAT_1:13;
end;
A11: R[ 0 ] by A2,A5;
for i being Nat holds R[i] from NAT_1:sch 2(A11,A7);
hence thesis by A1,A4;
end;
correctness
proof
reconsider e = 0 as Function;
defpred P[Nat,set,set] means not $2 is Function & $3 = e or $2
is Function & for g,h being Function st g = $2 & h = p.($1+1) holds $3 = h*g;
A12: for n being Nat for x being set ex y being set st P[n,x,y]
proof
let n be Nat, x be set;
reconsider h = p.(n+1) as Function;
per cases;
suppose
x is Function;
then reconsider g = x as Function;
take h*g;
thus thesis;
end;
suppose
A13: x is not Function;
take 0;
thus thesis by A13;
end;
end;
consider f being Function such that
A14: dom f = NAT & f.0 = id X and
A15: for n being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:
sch 1(A12);
defpred P[Nat] means f.$1 is Function;
A16: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat;
reconsider h = p.(i+1) as Function;
assume f.i is Function;
then reconsider g = f.i as Function;
f.(i+1) = h*g by A15;
hence thesis;
end;
A17: P[ 0] by A14;
A18: for i being Nat holds P[i] from NAT_1:sch 2(A17,A16);
then reconsider F = f.len p as Function;
f is Function-yielding
by A14,A18;
then reconsider f as ManySortedFunction of NAT by A14,PARTFUN1:def 2
,RELAT_1:def 18;
take F;
take f;
thus F = f.len p & f.0 = id X by A14;
let i be Nat;
thus thesis by A15;
end;
end;
definition
let p be Function-yielding FinSequence;
let x be object;
func apply(p,x) -> FinSequence means
:Def4:
len it = len p+1 & it.1 = x &
for i being Nat, f being Function st i in dom p & f = p.i holds it.(
i+1) = f.(it.i);
existence
proof
defpred P[Nat,set,set] means ex f being Function st f = p.$1 &
$3 = f.$2;
A1: for i being Nat st 1 <= i & i < len p+1 for x being set ex
y being set st P[i,x,y]
proof
let i be Nat;
assume 1 <= i;
assume
i < len p+1;
reconsider f = p.i as Function;
let x be set;
take f.x, f;
thus thesis;
end;
consider q being FinSequence such that
A2: len q = len p+1 &( q.1 = x or len p+1 = 0) and
A3: for i being Nat st 1 <= i & i < len p+1 holds P[i,q.i,q
.(i+1)] from RECDEF_1:sch 3(A1);
take q;
thus len q = len p+1 & q.1 = x by A2;
let i be Nat, f be Function;
assume
A4: i in dom p;
then i <= len p by FINSEQ_3:25;
then
A5: i < len p+1 by NAT_1:13;
i >= 1 by A4,FINSEQ_3:25;
then ex f being Function st f = p.i & q.(i+1) = f.(q.i) by A3,A5;
hence thesis;
end;
correctness
proof
let q1, q2 be FinSequence such that
A6: len q1 = len p+1 and
A7: q1.1 = x and
A8: for i being Nat, f being Function st i in dom p & f =
p.i holds q1.(i+1) = f.(q1.i) and
A9: len q2 = len p+1 and
A10: q2.1 = x and
A11: for i being Nat, f being Function st i in dom p & f =
p.i holds q2.(i+1) = f.(q2.i);
defpred P[Nat] means $1 in dom q1 implies q1.$1 = q2.$1;
A12: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A13: i in dom q1 implies q1.i = q2.i and
A14: i+1 in dom q1;
i+1 <= len q1 by A14,FINSEQ_3:25;
then
A15: i <= len p by A6,XREAL_1:6;
per cases;
suppose
i = 0;
hence thesis by A7,A10;
end;
suppose
A16: i > 0;
reconsider f = p.i as Function;
i >= 0+1 by A16,NAT_1:13;
then
A17: i in dom p by A15,FINSEQ_3:25;
hence q1.(i+1) = f.(q2.i) by A6,A8,A13,Th22
.= q2.(i+1) by A11,A17;
end;
end;
A18: P[ 0] by FINSEQ_3:25;
A19: for i being Nat holds P[i] from NAT_1:sch 2(A18,A12);
dom q1 = dom q2 by A6,A9,FINSEQ_3:29;
hence thesis by A19;
end;
end;
reserve X,Y for set, x for object,
p,q for Function-yielding FinSequence,
f,g,h for Function;
theorem Th38:
compose({},X) = id X
proof
ex f being ManySortedFunction of NAT st compose({},X) = f.0 & f.0 = id X
& for i being Nat st i+1 in dom {} for g,h being Function st g = f.i
& h = {} .(i+1) holds f.(i+1) = h*g by Def3,CARD_1:27;
hence thesis;
end;
theorem Th39:
apply({},x) = <*x*>
proof
len apply({},x) = 0+1 & apply({},x).1 = x by Def4,CARD_1:27;
hence thesis by FINSEQ_1:40;
end;
theorem Th40:
compose(p^<*f*>,X) = f*compose(p,X)
proof
A1: f = (p^<*f*>).(len p+1) by FINSEQ_1:42;
len <*f*> = 1 by FINSEQ_1:40;
then
A2: len (p^<*f*>) = len p+1 by FINSEQ_1:22;
consider ff being ManySortedFunction of NAT such that
A3: compose(p^<*f*>,X) = ff.len (p^<*f*>) and
A4: ff.0 = id X and
A5: for i being Nat st i+1 in dom (p^<*f*>) for g,h being
Function st g = ff.i & h = (p^<*f*>).(i+1) holds ff.(i+1) = h*g by Def3;
reconsider g = ff.len p as Function;
A6: dom p c= dom(p^<*f*>) by FINSEQ_1:26;
now
let i be Nat;
assume
A7: i+1 in dom p;
let g,h be Function;
assume that
A8: g = ff.i and
A9: h = p.(i+1);
h = (p^<*f*>).(i+1) by A7,A9,FINSEQ_1:def 7;
hence ff.(i+1) = h*g by A5,A6,A7,A8;
end;
then
A10: g = compose(p,X) by A4,Def3;
1 in Seg 1 & dom <*f*> = Seg 1 by FINSEQ_1:2,38,TARSKI:def 1;
hence thesis by A3,A5,A10,A2,A1,FINSEQ_1:28;
end;
theorem Th41:
apply(p^<*f*>,x) = apply(p,x)^<*f.(apply(p,x).(len p+1))*>
proof
defpred P[Nat] means $1 in dom apply(p,x) implies apply(p^<*f*>,x).$1 =
apply(p,x).$1;
A1: len apply(p,x) = len p+1 by Def4;
A2: apply(p,x).1 = x by Def4;
A3: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A4: i in dom apply(p,x) implies apply(p^<*f*>,x).i = apply(p,x).i and
A5: i+1 in dom apply(p,x);
A6: i+1 <= len apply(p,x) by A5,FINSEQ_3:25;
then
A7: i <= len apply(p,x) by NAT_1:13;
A8: i <= len p by A1,A6,XREAL_1:6;
per cases;
suppose
i = 0;
hence thesis by A2,Def4;
end;
suppose
A9: i > 0;
reconsider g = p.i as Function;
A10: i >= 0+1 by A9,NAT_1:13;
then
A11: i in dom p by A8,FINSEQ_3:25;
then dom p c= dom (p^<*f*>) & g = (p^<*f*>).i by FINSEQ_1:26,def 7;
then apply(p^<*f*>,x).(i+1) = g.(apply(p^<*f*>,x).i) by A11,Def4;
hence thesis by A4,A7,A10,A11,Def4,FINSEQ_3:25;
end;
end;
A12: P[ 0] by FINSEQ_3:25;
A13: for i being Nat holds P[i] from NAT_1:sch 2(A12,A3);
len <*f*> = 1 by FINSEQ_1:40;
then
A14: len (p^<*f*>) = len p+1 by FINSEQ_1:22;
A15: len p+1 >= 1 by NAT_1:11;
then
A16: (p^<*f*>).(len p+1) = f & len p+1 in dom (p^<*f*>) by A14,FINSEQ_1:42
,FINSEQ_3:25;
A17: len p+1 in dom apply(p,x) by A1,A15,FINSEQ_3:25;
A18: now
let i be Nat;
assume i in dom <*f.(apply(p,x).(len p+1))*>;
then i in Seg 1 by FINSEQ_1:38;
then
A19: i = 1 by FINSEQ_1:2,TARSKI:def 1;
then
f.(apply(p^<*f*>,x).(len p+i)) = apply(p^<*f*>,x).((len apply(p,x)) +
i) & apply(p^<*f*>,x).(len p+i) = apply(p,x).(len p+i) by A1,A16,A17,A13
,Def4;
hence
apply(p^<*f*>,x).((len apply(p,x))+i) = <*f.(apply(p,x).(len p+1))*>.
i by A19;
end;
len apply(p^<*f*>,x) = len (p^<*f*>)+1 by Def4;
then len <*f.(apply(p,x).(len p+1))*> = 1 & dom apply(p^<*f*>,x) = Seg (len
apply (p,x)+1) by A1,A14,FINSEQ_1:40,def 3;
hence thesis by A13,A18,FINSEQ_1:def 7;
end;
theorem
compose(<*f*>^p,X) = compose(p,f.:X)*(f|X)
proof
defpred R[Function-yielding FinSequence] means compose(<*f*>^$1,X) = compose
($1,f.:X)*(f|X);
A1: for p being Function-yielding FinSequence st R[p] for f being Function
holds R[p^<*f*>]
proof
let p be Function-yielding FinSequence such that
A2: compose(<*f*>^p,X) = compose(p,f.:X)*(f|X);
let g be Function;
thus compose(<*f*>^(p^<*g*>),X) = compose(<*f*>^p^<*g*>,X) by FINSEQ_1:32
.= g*compose(<*f*>^p,X) by Th40
.= g*compose(p,f.:X)*(f|X) by A2,RELAT_1:36
.= compose(p^<*g*>,f.:X)*(f|X) by Th40;
end;
<*f*>^{} = <*f*> & {}^<*f*> = <*f*> by FINSEQ_1:34;
then compose(<*f*>^{},X) = f*compose({},X) by Th40
.= f*id X by Th38
.= f|X by RELAT_1:65
.= (id rng (f|X))*(f|X) by RELAT_1:54
.= (id (f.:X))*(f|X) by RELAT_1:115
.= compose({},f.:X)*(f|X) by Th38;
then
A3: R[{}];
for p holds R[p] from FuncSeqInd(A3,A1);
hence thesis;
end;
theorem
apply(<*f*>^p,x) = <*x*>^apply(p,f.x)
proof
defpred P[Function-yielding FinSequence] means apply(<*f*>^$1,x) = <*x*>^
apply($1,f.x);
A1: len {} = 0;
A2: for p being Function-yielding FinSequence st P[p] for f being Function
holds P[p^<*f*>]
proof
let p such that
A3: apply(<*f*>^p,x) = <*x*>^apply(p,f.x);
let g be Function;
set p9 = <*f*>^p;
A4: len apply(p,f.x) = len p+1 by Def4;
len <*f*> = 1 by FINSEQ_1:40;
then
A5: len p9 = len p+1 by FINSEQ_1:22;
then len p9 >= 1 by NAT_1:11;
then len <*x*> = 1 & len p9 in dom apply(p,f.x) by A4,A5,FINSEQ_1:40
,FINSEQ_3:25;
then
A6: apply(p9,x).(1+len p9) = apply(p,f.x).(len p+1) by A3,A5,FINSEQ_1:def 7;
apply(p9^<*g*>,x) = apply(p9,x)^<*g.(apply(p9,x).(len p9+1))*> by Th41;
hence apply(<*f*>^(p^<*g*>),x) = <*x*>^apply(p,f.x)^<*g.(apply(p,f.x).(len
p+1))*> by A3,A6,FINSEQ_1:32
.= <*x*>^(apply(p,f.x)^<*g.(apply(p,f.x).(len p+1))*>) by FINSEQ_1:32
.= <*x*>^apply(p^<*g*>,f.x) by Th41;
end;
<*f*>^{} = <*f*> & {}^<*f*> = <*f*> by FINSEQ_1:34;
then apply(<*f*>^{},x) = apply({},x)^<*f.(apply({},x).(0+1))*> by A1,Th41
.= <*x*>^<*f.(apply({},x).1)*> by Th39
.= <*x*>^<*f.(<*x*>.1)*> by Th39
.= <*x*>^<*f.x*>
.= <*x*>^apply({},f.x) by Th39;
then
A7: P[{}];
for p holds P[p] from FuncSeqInd(A7,A2);
hence thesis;
end;
theorem Th44:
compose(<*f*>,X) = f*id X
proof
<*f*> = {}^<*f*> by FINSEQ_1:34;
hence compose(<*f*>,X) = f*compose({},X) by Th40
.= f*id X by Th38;
end;
theorem
dom f c= X implies compose(<*f*>,X) = f
proof
compose(<*f*>,X) = f*id X by Th44;
hence thesis by RELAT_1:51;
end;
theorem Th46:
apply(<*f*>,x) = <*x,f.x*>
proof
A1: <*x*>.(0+1) = x;
A2: apply({},x) = <*x*> & len {} = 0 by Th39;
thus apply(<*f*>,x) = apply({}^<*f*>,x) by FINSEQ_1:34
.= <*x*>^<*f.x*> by A2,A1,Th41
.= <*x,f.x*> by FINSEQ_1:def 9;
end;
theorem
rng compose(p,X) c= Y implies compose(p^q,X) = compose(q,Y)*compose(p,
X )
proof
assume
A1: rng compose(p,X) c= Y;
defpred P[Function-yielding FinSequence] means compose(p^$1,X) = compose($1,
Y)*compose(p,X);
A2: for p being Function-yielding FinSequence st P[p] for f being Function
holds P[p^<*f*>]
proof
let q such that
A3: compose(p^q,X) = compose(q,Y)*compose(p,X);
let f;
thus compose(p^(q^<*f*>),X) = compose(p^q^<*f*>,X) by FINSEQ_1:32
.= f*compose(p^q,X) by Th40
.= f*compose(q,Y)*compose(p,X) by A3,RELAT_1:36
.= compose(q^<*f*>,Y)*compose(p,X) by Th40;
end;
compose(p^{},X) = compose(p,X) by FINSEQ_1:34
.= (id Y)*compose(p,X) by A1,RELAT_1:53
.= compose({},Y)*compose(p,X) by Th38;
then
A4: P[{}];
for q holds P[q] from FuncSeqInd(A4,A2);
hence thesis;
end;
theorem Th48:
apply(p^q,x).(len (p^q)+1) = apply(q,apply(p,x).(len p+1)).(len
q+1)
proof
defpred P[Function-yielding FinSequence] means apply(p^$1,x).(len (p^$1)+1)
= apply($1,apply(p,x).(len p+1)).(len $1+1);
A1: for p being Function-yielding FinSequence st P[p] for f being Function
holds P[p^<*f*>]
proof
set y = apply(p,x).(len p+1);
let q such that
A2: apply(p^q,x).(len (p^q)+1) = apply(q,apply(p,x).(len p+1)).(len q+
1);
let f be Function;
A3: len <*f*> = 1 by FINSEQ_1:40;
then
A4: len (p^q^<*f*>) = len (p^q)+1 by FINSEQ_1:22;
A5: len (q^<*f*>) = len q+1 by A3,FINSEQ_1:22;
A6: apply(q^<*f*>,y) = apply(q,y)^<*f.(apply(q,y).(len q+1))*> & len
apply(q,y) = len q+1 by Def4,Th41;
A7: len apply(p^q,x) = len (p^q)+1 by Def4;
p^(q^<*f*>) = p^q^<*f*> & apply(p^q^<*f*>,x) = apply(p^q,x)^<*f.(apply
(p^q,x ).(len (p^q)+1))*> by Th41,FINSEQ_1:32;
hence
apply(p^(q^<*f*>),x).(len (p^(q^<*f*>))+1) = f.(apply(p^q,x).(len (p^
q)+1)) by A7,A4,FINSEQ_1:42
.= apply(q^<*f*>,apply(p,x).(len p+1)).(len (q^<*f*>)+1) by A2,A6,A5,
FINSEQ_1:42;
end;
apply({},apply(p,x).(len p+1)) = <*apply(p,x).(len p+1)*> & p^{} = p by Th39,
FINSEQ_1:34;
then
A8: P[{}];
for q holds P[q] from FuncSeqInd(A8,A1);
hence thesis;
end;
theorem
apply(p^q,x) = apply(p,x)$^apply(q,apply(p,x).(len p+1))
proof
defpred P[Function-yielding FinSequence] means apply(p^$1,x) = apply(p,x)$^
apply($1,apply(p,x).(len p+1));
A1: len apply(p,x) = len p+1 by Def4;
then consider r being FinSequence, y being object such that
A2: apply(p,x) = r^<*y*> by CARD_1:27,FINSEQ_1:46;
A3: for p being Function-yielding FinSequence st P[p] for f being Function
holds P[p^<*f*>]
proof
let q such that
A4: apply(p^q,x) = apply(p,x)$^apply(q,apply(p,x).(len p+1));
A5: apply(p^q,x).(len (p^q)+1) = apply(q,apply(p,x).(len p+1)).(len q+1)
by Th48;
let f;
A6: len apply(q,apply(p,x).(len p+1)) = len q+1 by Def4;
A7: len apply(q^<*f*>,apply(p,x).(len p+1)) = len(q^<*f*>)+1 by Def4;
thus apply(p^(q^<*f*>),x) = apply(p^q^<*f*>,x) by FINSEQ_1:32
.= apply(p^q,x)^<*f.(apply(p^q,x).(len (p^q)+1))*> by Th41
.= r^apply(q,apply(p,x).(len p+1))^<*f.(apply(p^q,x).(len (p^q)+1))*>
by A2,A4,A6,CARD_1:27,REWRITE1:2
.= r^(apply(q,apply(p,x).(len p+1))^<*f.(apply(p^q,x).(len (p^q)+1))*>
) by FINSEQ_1:32
.= r^apply(q^<*f*>,apply(p,x).(len p+1)) by A5,Th41
.= apply(p,x)$^apply(q^<*f*>,apply(p,x).(len p+1))
by A2,A7,CARD_1:27,REWRITE1:2;
end;
len <*y*> = 1 by FINSEQ_1:40;
then len p+1 = len r+1 by A1,A2,FINSEQ_1:22;
then
A8: apply(p,x).(len p+1) = y by A2,FINSEQ_1:42;
apply(p^{},x) = apply(p,x) by FINSEQ_1:34
.= apply(p,x)$^<*apply(p,x).(len p+1)*> by A2,A8,REWRITE1:2
.= apply(p,x)$^apply({},apply(p,x).(len p+1)) by Th39;
then
A9: P[{}];
for q holds P[q] from FuncSeqInd(A9,A3);
hence thesis;
end;
theorem Th50:
compose(<*f,g*>,X) = g*f*id X
proof
<*f,g*> = <*f*>^<*g*> by FINSEQ_1:def 9;
hence compose(<*f,g*>,X) = g*compose(<*f*>,X) by Th40
.= g*(f*id X) by Th44
.= g*f*id X by RELAT_1:36;
end;
theorem
dom f c= X or dom(g*f) c= X implies compose(<*f,g*>,X) = g*f
proof
compose(<*f,g*>,X) = g*f*id X & g*f*id X = g*(f*id X) by Th50,RELAT_1:36;
hence thesis by RELAT_1:51;
end;
theorem Th52:
apply(<*f,g*>,x) = <*x,f.x,g.(f.x)*>
proof
A1: apply(<*f*>,x) = <*x,f.x*> & len <*f*> = 1 by Th46,FINSEQ_1:40;
thus apply(<*f,g*>,x) = apply(<*f*>^<*g*>,x) by FINSEQ_1:def 9
.= <*x,f.x*>^<*g.(<*x,f.x*>.(1+1))*> by A1,Th41
.= <*x,f.x*>^<*g.(f.x)*>
.= <*x,f.x,g.(f.x)*> by FINSEQ_1:43;
end;
theorem Th53:
compose(<*f,g,h*>,X) = h*g*f*id X
proof
<*f,g,h*> = <*f,g*>^<*h*> by FINSEQ_1:43;
hence compose(<*f,g,h*>,X) = h*compose(<*f,g*>,X) by Th40
.= h*(g*f*id X) by Th50
.= h*(g*f)*id X by RELAT_1:36
.= h*g*f*id X by RELAT_1:36;
end;
theorem
dom f c= X or dom(g*f) c= X or dom(h*g*f) c= X implies compose(<*f,g,h
*>,X) = h*g*f
proof
A1: h*g*(f*id X) = h*(g*(f*id X)) & g*(f*id X) = g*f*id X by RELAT_1:36;
A2: h*(g*f) = h*g*f by RELAT_1:36;
compose(<*f,g,h*>,X) = h*g*f*id X & h*g*f*id X = h*g*(f*id X) by Th53,
RELAT_1:36;
hence thesis by A1,A2,RELAT_1:51;
end;
theorem
apply(<*f,g,h*>,x) = <*x*>^<*f.x,g.(f.x),h.(g.(f.x))*>
proof
A1: apply(<*f,g*>,x) = <*x,f.x,g.(f.x)*> & len <*f,g*> = 2 by Th52,FINSEQ_1:44;
thus apply(<*f,g,h*>,x) = apply(<*f,g*>^<*h*>,x) by FINSEQ_1:43
.= <*x,f.x,g.(f.x)*>^<*h.(<*x,f.x,g.(f.x)*>.(2+1))*> by A1,Th41
.= <*x,f.x,g.(f.x)*>^<*h.(g.(f.x))*>
.= <*x*>^<*f.x,g.(f.x)*>^<*h.(g.(f.x))*> by FINSEQ_1:43
.= <*x*>^(<*f.x,g.(f.x)*>^<*h.(g.(f.x))*>) by FINSEQ_1:32
.= <*x*>^<*f.x,g.(f.x),h.(g.(f.x))*> by FINSEQ_1:43;
end;
definition
let F be FinSequence;
func firstdom F -> set means
: Def5:
it is empty if F is empty otherwise it = proj1
(F.1);
correctness;
func lastrng F -> set means
: Def6:
it is empty if F is empty otherwise it = proj2
(F.len F);
correctness;
end;
theorem Th56:
firstdom {} = {} & lastrng {} = {} by Def5,Def6;
theorem Th57:
for p being FinSequence holds firstdom (<*f*>^p) = dom f &
lastrng (p^<*f*>) = rng f
proof
let p be FinSequence;
thus firstdom (<*f*>^p) = proj1((<*f*>^p).1) by Def5
.= dom f by FINSEQ_1:41;
len <*f*> = 1 by FINSEQ_1:40;
then len (p^<*f*>) = len p+1 by FINSEQ_1:22;
hence lastrng (p^<*f*>) = proj2((p^<*f*>).(len p+1)) by Def6
.= rng f by FINSEQ_1:42;
end;
theorem Th58:
for p being Function-yielding FinSequence st p <> {} holds rng
compose(p,X) c= lastrng p
proof
defpred P[Function-yielding FinSequence] means $1 <> {} implies rng compose(
$1,X) c= lastrng $1;
A1: for p being Function-yielding FinSequence st P[p] for f being Function
holds P[p^<*f*>]
proof
let q;
assume q <> {} implies rng compose(q,X) c= lastrng q;
let f;
assume q^<*f*> <> {};
compose(q^<*f*>,X) = f*compose(q,X) by Th40;
then rng compose(q^<*f*>,X) c= rng f by RELAT_1:26;
hence thesis by Th57;
end;
A2: P[{}];
thus for p holds P[p] from FuncSeqInd(A2,A1);
end;
definition
let IT be FinSequence;
attr IT is FuncSeq-like means
: Def7:
ex p being FinSequence st len p = len
IT+1 & for i being Nat st i in dom IT holds IT.i in Funcs(p.i, p.(i+
1));
end;
theorem Th59:
for p,q being FinSequence st p^q is FuncSeq-like holds p is
FuncSeq-like & q is FuncSeq-like
proof
let p,q be FinSequence;
given pq being FinSequence such that
A1: len pq = len (p^q)+1 and
A2: for i being Nat st i in dom (p^q) holds (p^q).i in Funcs(
pq.i, pq.(i+1));
reconsider p1 = pq|Seg (len p+1), p2 = pq|Seg len p as FinSequence by
FINSEQ_1:15;
A3: len (p^q) = len p+len q by FINSEQ_1:22;
then
A4: len p <= len (p^q) by NAT_1:11;
len (p^q) <= len pq by A1,NAT_1:11;
then len p <= len pq by A4,XXREAL_0:2;
then
A5: len p2 = len p by FINSEQ_1:17;
hereby
take p1;
len p <= len (p^q) by A3,NAT_1:11;
then len p+1 <= len pq by A1,XREAL_1:6;
hence
A6: len p1 = len p+1 by FINSEQ_1:17;
let i be Nat;
assume
A7: i in dom p;
then (p^q).i = p.i by FINSEQ_1:def 7;
then
A8: p.i in Funcs(pq.i, pq.(i+1)) by A2,A7,FINSEQ_3:22;
i in dom p1 by A6,A7,Th22;
then
A9: pq.i = p1.i by FUNCT_1:47;
i+1 in dom p1 by A6,A7,Th22;
hence p.i in Funcs(p1.i, p1.(i+1)) by A8,A9,FUNCT_1:47;
end;
consider q2 being FinSequence such that
A10: pq = p2^q2 by FINSEQ_1:80;
take q2;
len pq = len p2+len q2 by A10,FINSEQ_1:22;
hence len q2 = len q+1 by A1,A3,A5;
let x be Nat;
assume
A11: x in dom q;
then (p^q).(len p+x) = q.x by FINSEQ_1:def 7;
then
A12: q.x in Funcs(pq.(len p+x), pq.(len p+x+1)) by A2,A11,FINSEQ_1:28;
A13: len p+(len q+1) = len p+len q2 by A1,A3,A10,A5,FINSEQ_1:22;
then x+1 in dom q2 by A11,Th22;
then
A14: q2.(x+1) = pq.(len p+(x+1)) by A10,A5,FINSEQ_1:def 7;
x in dom q2 by A13,A11,Th22;
hence thesis by A10,A5,A12,A14,FINSEQ_1:def 7;
end;
registration
cluster FuncSeq-like -> Function-yielding for FinSequence;
coherence
proof
let q be FinSequence;
given p being FinSequence such that
len p = len q+1 and
A1: for i being Nat st i in dom q holds q.i in Funcs(p.i, p
.(i+1));
let i be object;
assume
A2: i in dom q;
then reconsider i as Nat;
q.i in Funcs(p.i, p.(i+1)) by A1,A2;
hence thesis;
end;
end;
registration
cluster empty -> FuncSeq-like for FinSequence;
coherence
proof
let p be FinSequence;
assume
A1: p is empty;
take q = <*{}*>;
thus len q = len p+1 by A1,FINSEQ_1:40;
thus thesis by A1;
end;
end;
registration
let f be Function;
cluster <*f*> -> FuncSeq-like;
coherence
proof
take q = <*dom f, rng f*>;
set p = <*f*>;
thus len q = 1+1 by FINSEQ_1:44
.= len p+1 by FINSEQ_1:40;
let i be Nat;
assume i in dom p;
then i in {1} by FINSEQ_1:2,38;
then
A1: i = 1 by TARSKI:def 1;
then
A2: q.(i+1) = rng f;
p.i = f & q.i = dom f by A1;
hence thesis by A2,FUNCT_2:def 2;
end;
end;
registration
cluster FuncSeq-like non empty non-empty for FinSequence;
existence
proof
set f =the non empty Function;
take p = <*f*>;
thus p is FuncSeq-like;
thus p is non empty;
let x be object;
assume x in dom p;
then x in {1} by FINSEQ_1:2,38;
then x = 1 by TARSKI:def 1;
hence thesis;
end;
end;
definition
mode FuncSequence is FuncSeq-like FinSequence;
end;
theorem Th60:
for p being FuncSequence st p <> {} holds dom compose(p,X) = (
firstdom p) /\ X
proof
defpred P[Function-yielding FinSequence] means $1 is FuncSequence & $1 <> {}
implies dom compose($1,X) = (firstdom $1) /\ X;
A1: for p being Function-yielding FinSequence st P[p] for f being Function
holds P[p^<*f*>]
proof
let q;
assume
A2: q is FuncSequence & q <> {} implies dom compose(q,X) = (firstdom q
) /\ X;
let f;
assume that
A3: q^<*f*> is FuncSequence and
q^<*f*> <> {};
A4: compose(q^<*f*>,X) = f*compose(q,X) by Th40;
per cases;
suppose
q = {};
then
A5: q^<*f*> = <*f*> by FINSEQ_1:34;
then
A6: compose(q^<*f*>,X) = f*id X by Th44;
<*f*>^{} = <*f*> by FINSEQ_1:34;
then firstdom(q^<*f*>) = dom f by A5,Th57;
hence thesis by A6,FUNCT_1:19;
end;
suppose
A7: q <> {};
then consider y being object, s being FinSequence such that
A8: q = <*y*>^s and
A9: len q = len s+1 by REWRITE1:5;
reconsider y as set by TARSKI:1;
q.1 = y by A8,FINSEQ_1:41;
then
A10: firstdom q = proj1 y by A8,Def5;
A11: len q >= 1 by A9,NAT_1:11;
then len q in dom q by FINSEQ_3:25;
then
A12: (q^<*f*>).len q = q.len q by FINSEQ_1:def 7;
A13: rng compose(q,X) c= lastrng q by A7,Th58;
consider p being FinSequence such that
len p = len (q^<*f*>)+1 and
A14: for i being Nat st i in dom (q^<*f*>) holds (q^<*f*>
).i in Funcs(p.i, p.(i+1)) by A3,Def7;
consider r being FinSequence, x being object such that
A15: q = r^<*x*> by A7,FINSEQ_1:46;
len <*f*> = 1 by FINSEQ_1:40;
then
A16: len (q^<*f*>) = len q+1 by FINSEQ_1:22;
then len q <= len (q^<*f*>) by NAT_1:11;
then len q in dom (q^<*f*>) by A11,FINSEQ_3:25;
then
A17: (q^<*f*>).len q in Funcs(p.len q, p.(len q+1)) by A14;
len <*x*> = 1 by FINSEQ_1:40;
then len q = len r+1 by A15,FINSEQ_1:22;
then q.len q = x by A15,FINSEQ_1:42;
then consider g being Function such that
A18: x = g and
dom g = p.len q and
A19: rng g c= p.(len q+1) by A17,A12,FUNCT_2:def 2;
A20: (<*y*>^(s^<*f*>)).1 = y by FINSEQ_1:41;
len q+1 >= 1 by NAT_1:11;
then len q+1 in dom (q^<*f*>) by A16,FINSEQ_3:25;
then
A21: (q^<*f*>).(len q+1) in Funcs(p.(len q+1), p.(len q+1+1)) by A14;
(q^<*f*>).(len q+1) = f by FINSEQ_1:42;
then
A22: ex g being Function st f = g & dom g = p.(len q+1) & rng g c= p.(
len q+1+1) by A21,FUNCT_2:def 2;
q^<*f*> = <*y*>^(s^<*f*>) by A8,FINSEQ_1:32;
then
A23: firstdom (q^<*f*>) = proj1 y by A20,Def5;
lastrng q = rng g by A15,A18,Th57;
hence thesis by A2,A3,A4,A7,A23,A10,A19,A22,A13,Th59,RELAT_1:27
,XBOOLE_1:1;
end;
end;
A24: P[{}];
for p being Function-yielding FinSequence holds P[p] from FuncSeqInd(
A24,A1);
hence thesis;
end;
theorem Th61:
for p being FuncSequence holds dom compose(p,firstdom p) =
firstdom p
proof
let p be FuncSequence;
per cases;
suppose
p = {};
then compose(p,firstdom p) = id firstdom p by Th38;
hence thesis;
end;
suppose
p <> {};
then dom compose(p,firstdom p) = (firstdom p) /\ firstdom p by Th60;
hence thesis;
end;
end;
theorem
for p being FuncSequence, f being Function st rng f c= firstdom p
holds <*f*>^p is FuncSequence
proof
let p be FuncSequence, f be Function such that
A1: rng f c= firstdom p;
consider q being FinSequence such that
A2: len q = len p+1 and
A3: for i being Nat st i in dom p holds p.i in Funcs(q.i, q.(
i+1)) by Def7;
set r = <*dom f*>^q;
A4: len <*dom f*> = 1 by FINSEQ_1:40;
A5: len <*f*> = 1 by FINSEQ_1:40;
then
A6: len (<*f*>^p) = len p+1 by FINSEQ_1:22;
A7: now
assume
A8: p <> {};
then len p >= 0+1 by NAT_1:13;
then 1 in dom p by FINSEQ_3:25;
then p.1 in Funcs(q.1, q.(1+1)) by A3;
then ex g being Function st p.1 = g & dom g = q.1 & rng g c= q.2 by
FUNCT_2:def 2;
hence rng f c= q.1 by A1,A8,Def5;
end;
<*f*>^p is FuncSeq-like
proof
take r;
1 <= len q by A2,NAT_1:11;
then
A9: 1 in dom q by FINSEQ_3:25;
thus len r = len (<*f*>^p)+1 by A2,A4,A6,FINSEQ_1:22;
let i be Nat;
assume
A10: i in dom (<*f*>^p);
then
A11: i >= 1 by FINSEQ_3:25;
A12: rng f c= q.1 by A1,A7,Th56;
A13: i <= len p+1 by A6,A10,FINSEQ_3:25;
per cases;
suppose
A14: i = 1;
then
A15: r.i = dom f & (<*f*>^p).i = f by FINSEQ_1:41;
r.(i+1) = q.1 by A4,A9,A14,FINSEQ_1:def 7;
hence thesis by A12,A15,FUNCT_2:def 2;
end;
suppose
i <> 1;
then i > 1 by A11,XXREAL_0:1;
then i >= 1+1 by NAT_1:13;
then consider j being Nat such that
A16: i = 1+1+j by NAT_1:10;
A17: i = j+1+1 by A16;
then j+1 >= 1 & j+1 <= len p by A13,NAT_1:11,XREAL_1:6;
then
A18: j+1 in dom p by FINSEQ_3:25;
then
A19: p.(j+1) = (<*f*>^p).i by A5,A17,FINSEQ_1:def 7;
A20: j+1+1 in dom q by A2,A18,Th22;
A21: p.(j+1) in Funcs(q.(j+1),q.(j+1+1)) by A3,A18;
j+1 in dom q by A2,A18,Th22;
then r.i = q.(j+1) by A4,A16,A21,FINSEQ_1:def 7;
hence thesis by A4,A16,A21,A20,A19,FINSEQ_1:def 7;
end;
end;
hence thesis;
end;
theorem
for p being FuncSequence, f being Function st lastrng p c= dom f holds
p^<*f*> is FuncSequence
proof
let p be FuncSequence, f be Function such that
A1: lastrng p c= dom f;
consider q being FinSequence such that
A2: len q = len p+1 and
A3: for i being Nat st i in dom p holds p.i in Funcs(q.i, q.(
i+1)) by Def7;
consider q9 being FinSequence, x being object such that
A4: q = q9^<*x*> by A2,CARD_1:27,FINSEQ_1:46;
A5: now
assume
A6: len p in dom p;
then p.len p in Funcs(q.len p, q.(len p+1)) by A3;
then consider g being Function such that
A7: p.len p = g and
A8: dom g = q.len p and
rng g c= q.(len p+1) by FUNCT_2:def 2;
lastrng p = rng g by A6,A7,Def6,RELAT_1:38;
hence p.len p in Funcs(q.len p,dom f) by A1,A7,A8,FUNCT_2:def 2;
end;
A9: <*dom f,rng f*>.1 = dom f;
A10: <*dom f,rng f*>.2 = rng f;
len <*f*> = 1 by FINSEQ_1:40;
then
A11: len (p^<*f*>) = len p+1 by FINSEQ_1:22;
set r = q9^<*dom f,rng f*>;
len <*dom f,rng f*> = 2 by FINSEQ_1:44;
then
A12: len r = len q9+(1+1) by FINSEQ_1:22;
A13: dom <*dom f,rng f*> = Seg 2 by FINSEQ_1:89;
then
A14: 1 in dom <*dom f,rng f*> by FINSEQ_1:2,TARSKI:def 2;
len <*x*> = 1 by FINSEQ_1:40;
then
A15: len q = len q9+1 by A4,FINSEQ_1:22;
A16: 2 in dom <*dom f,rng f*> by A13,FINSEQ_1:2,TARSKI:def 2;
p^<*f*> is FuncSeq-like
proof
take r;
thus len r = len (p^<*f*>)+1 by A2,A15,A11,A12;
let i be Nat;
assume
A17: i in dom (p^<*f*>);
then
A18: i >= 1 by FINSEQ_3:25;
i <= len p+1 by A11,A17,FINSEQ_3:25;
then
A19: i = len p+1 or len p >= i by NAT_1:8;
per cases by A19,XXREAL_0:1;
suppose
A20: i = len p+1;
then
A21: r.i = dom f & (p^<*f*>).i = f by A2,A15,A14,A9,FINSEQ_1:42,def 7;
r.(i+1) = rng f by A2,A15,A12,A16,A10,A20,FINSEQ_1:def 7;
hence thesis by A21,FUNCT_2:def 2;
end;
suppose
A22: i = len p;
then i in dom q9 by A2,A15,A18,FINSEQ_3:25;
then
A23: r.i = q9.i & q9.i = q.i by A4,FINSEQ_1:def 7;
len p in dom p & r.(i+1) = dom f by A2,A15,A14,A9,A18,A22,FINSEQ_1:def 7
,FINSEQ_3:25;
hence thesis by A5,A22,A23,FINSEQ_1:def 7;
end;
suppose
A24: i < len p;
then i in dom q9 by A2,A15,A18,FINSEQ_3:25;
then
A25: q.i = q9.i & q9.i = r.i by A4,FINSEQ_1:def 7;
A26: i+1 >= 1 by NAT_1:11;
i in dom p by A18,A24,FINSEQ_3:25;
then
A27: p.i in Funcs(q.i, q.(i+1)) & p.i = (p^<*f*>).i by A3,FINSEQ_1:def 7;
i+1 <= len p by A24,NAT_1:13;
then
A28: i+1 in dom q9 by A2,A15,A26,FINSEQ_3:25;
then q.(i+1) = q9.(i+1) by A4,FINSEQ_1:def 7;
hence thesis by A28,A25,A27,FINSEQ_1:def 7;
end;
end;
hence thesis;
end;
theorem
for p being FuncSequence st x in firstdom p & x in X holds apply(p,x).
(len p+1) = compose(p,X).x
proof
defpred P[Function-yielding FinSequence] means $1 is FuncSequence & x in
firstdom $1 & x in X implies apply($1,x).(len $1+1) = compose($1,X).x;
A1: for p being Function-yielding FinSequence st P[p] for f being Function
holds P[p^<*f*>]
proof
A2: dom id X = X;
let p such that
A3: p is FuncSequence & x in firstdom p & x in X implies apply(p,x).(
len p+1) = compose(p,X).x;
let f;
assume that
A4: p^<*f*> is FuncSequence and
A5: x in firstdom (p^<*f*>) and
A6: x in X;
A7: p is FuncSequence by A4,Th59;
(id X).x = x by A6,FUNCT_1:17;
then
A8: (f*id X).x = f.x by A6,A2,FUNCT_1:13;
A9: len <*f*> = 1 by FINSEQ_1:40;
A10: compose(p^<*f*>,X) = f*compose(p,X) by Th40;
A11: apply(<*f*>,x) = <*x,f.x*> & compose(<*f*>,X) = f*id X by Th44,Th46;
A12: apply(p^<*f*>,x) = apply(p,x)^<*f.(apply(p,x).(len p+1))*> by Th41;
per cases;
suppose
p = {};
then p^<*f*> = <*f*> by FINSEQ_1:34;
hence thesis by A9,A11,A8;
end;
suppose
A13: p <> {};
then
A14: dom compose(p,X) = (firstdom p) /\ X by A7,Th60;
A15: firstdom (p^<*f*>) = proj1((p^<*f*>).1) by Def5;
A16: firstdom p = proj1 (p.1) by A13,Def5;
len p >= 0+1 by A13,NAT_1:13;
then
A17: 1 in dom p by FINSEQ_3:25;
then p.1 = (p^<*f*>).1 by FINSEQ_1:def 7;
then
A18: x in (firstdom p) /\ X by A5,A6,A16,A15,XBOOLE_0:def 4;
len apply(p,x) = len p+1 & len (p^<*f*>) = len p+1 by A9,Def4,FINSEQ_1:22
;
hence
apply(p^<*f*>,x).(len (p^<*f*>)+1) = f.(compose(p,X).x) by A3,A4,A5,A6
,A12,A16,A15,A17,Th59,FINSEQ_1:42,def 7
.= compose(p^<*f*>,X).x by A10,A14,A18,FUNCT_1:13;
end;
end;
A19: P[{}] by Def5;
for p holds P[p] from FuncSeqInd(A19,A1);
hence thesis;
end;
definition
let X,Y be set such that
A1: Y is empty implies X is empty;
mode FuncSequence of X,Y -> FuncSequence means
: Def8:
firstdom it = X &
lastrng it c= Y;
existence
proof
set f =the Function of X,Y;
take p = <*f*>;
A2: p^{} = p & {}^p = p by FINSEQ_1:34;
dom f = X & rng f c= Y by A1,FUNCT_2:def 1;
hence thesis by A2,Th57;
end;
end;
definition
let Y be non empty set, X be set;
let F be FuncSequence of X,Y;
redefine func compose(F,X) -> Function of X,Y; :: redefines compose (FUNCT_7, definition)
coherence
proof
A1: firstdom F = X by Def8;
now
assume F = {};
then X = {} & compose(F,X) = id X by A1,Def5,Th38;
hence rng compose(F,X) = {};
end;
then
A2: rng compose(F,X) c= lastrng F by Th58;
lastrng F c= Y by Def8;
then
A3: rng compose(F,X) c= Y by A2;
dom compose(F,X) = X by A1,Th61;
hence thesis by A3,FUNCT_2:def 1,RELSET_1:4;
end;
end;
definition
let q be non-empty non empty FinSequence;
mode FuncSequence of q -> FinSequence means
:Def9:
len it+1 = len q & for i
being Nat st i in dom it holds it.i in Funcs(q.i,q.(i+1));
existence
proof
defpred P[object,object] means
ex i being Nat st i = $1 & $2 in Funcs(q.i,q.(i+1));
consider n being Nat such that
A1: len q = n+1 by NAT_1:6;
reconsider n as Element of NAT by ORDINAL1:def 12;
A2: for x being object st x in Seg n ex y being object st P[x,y]
proof
let x be object;
assume
A3: x in Seg n;
then reconsider i = x as Nat;
A4: i <= n by A3,FINSEQ_1:1;
then i+1 >= 1 & i+1 <= n+1 by NAT_1:11,XREAL_1:6;
then
A5: i+1 in dom q by A1,FINSEQ_3:25;
n <= n+1 by NAT_1:11;
then
A6: i <= n+1 by A4,XXREAL_0:2;
i >= 1 by A3,FINSEQ_1:1;
then i in dom q by A1,A6,FINSEQ_3:25;
then reconsider X = q.i, Y = q.(i+1) as non empty set by A5;
set y =the Function of X,Y;
take y,i;
thus thesis by FUNCT_2:8;
end;
consider f being Function such that
A7: dom f = Seg n and
A8: for x being object st x in Seg n holds P[x,f.x] from CLASSES1:sch 1(A2);
reconsider f as FinSequence by A7,FINSEQ_1:def 2;
take f;
thus len f+1 = len q by A1,A7,FINSEQ_1:def 3;
let i be Nat;
assume i in dom f;
then
ex j being Nat st j = i & f.i in Funcs(q.j,q.(j+1)) by A7,A8;
hence thesis;
end;
end;
registration
let q be non-empty non empty FinSequence;
cluster -> FuncSeq-like non-empty for FuncSequence of q;
coherence
proof
let p be FuncSequence of q;
thus p is FuncSeq-like
proof
take q;
thus thesis by Def9;
end;
let x be object;
assume
A1: x in dom p;
then reconsider i = x as Nat;
len q = len p+1 by Def9;
then i in dom q & i+1 in dom q by A1,Th22;
then reconsider X = q.i, Y = q.(i+1) as non empty set;
p.i in Funcs(X,Y) by A1,Def9;
then ex f st p.x = f & dom f = X & rng f c= Y by FUNCT_2:def 2;
hence thesis;
end;
end;
theorem Th65:
for q being non-empty non empty FinSequence, p being
FuncSequence of q st p <> {} holds firstdom p = q.1 & lastrng p c= q.len q
proof
let q be non-empty non empty FinSequence;
let p be FuncSequence of q;
assume
A1: p <> {};
then 1 in dom p by FINSEQ_5:6;
then p.1 in Funcs(q.1,q.(1+1)) by Def9;
then ex f being Function st p.1 = f & dom f = q.1 & rng f c= q.2 by
FUNCT_2:def 2;
hence firstdom p = q.1 by A1,Def5;
len p in dom p by A1,FINSEQ_5:6;
then p.len p in Funcs(q.len p,q.(len p+1)) by Def9;
then
A2: ex g being Function st p.len p = g & dom g = q.len p & rng g c= q.(len p+
1) by FUNCT_2:def 2;
len p+1 = len q by Def9;
hence thesis by A1,A2,Def6;
end;
theorem
for q being non-empty non empty FinSequence, p being FuncSequence of q
holds dom compose(p,q.1) = q.1 & rng compose(p,q.1) c= q.len q
proof
let q be non-empty non empty FinSequence;
let p be FuncSequence of q;
per cases;
suppose
A1: p = {};
A2: len q = len p+1 by Def9;
compose(p,q.1) = id (q.1) & len p = 0 by A1,Th38;
hence thesis by A2;
end;
suppose
A3: p <> {};
then
A4: lastrng p c= q.len q by Th65;
firstdom p = q.1 & rng compose(p,q.1) c= lastrng p by A3,Th58,Th65;
hence thesis by A4,Th61;
end;
end;
:: Moved from FUNCT_4
registration
let X be set;
let f be sequence of bool [:X,X:];
let n be Nat;
cluster f.n -> Relation-like;
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
f.n is Element of bool [:X,X:];
hence thesis;
end;
end;
Lm1: for f being Function of X,X holds rng f c= dom f
proof
let f be Function of X,X;
dom f = X by FUNCT_2:52;
hence thesis;
end;
Lm2: for f being Relation for n being Nat
for p1,p2 being sequence of bool [:field f,field f:] st
p1.0 = id(field f) &
(for k being Nat holds p1.(k+1) = f*p1.k) &
p2.0 = id(field f) & (for k being Nat holds p2.(k+1) = f*p2.k)
holds p1 = p2
proof
let f be Relation;
let n be Nat;
let p1,p2 be sequence of bool [:field f,field f:] such that
A1: p1.0 = id(field f) and
A2: for k being Nat holds p1.(k+1) = f * p1.k and
A3: p2.0 = id(field f) and
A4: for k being Nat holds p2.(k+1) = f * p2.k;
defpred P[Nat,Relation,set] means $3 = f*$2;
A5: for k being Nat holds P[k,p1.k,p1.(k+1)] by A2;
set FX = bool [:field f,field f:];
reconsider ID = id(field f) as Element of FX;
A6: p2.0 = ID by A3;
A7: for k being Nat for x,y1,y2 being Element of FX st P[k,x,y1] & P[k,x,y2]
holds y1 = y2;
A8: for k being Nat holds P[k,p2.k,p2.(k+1)] by A4;
A9: p1.0 = ID by A1;
p1 = p2 from NAT_1:sch 14(A9,A5,A6,A8,A7);
hence thesis;
end;
definition
let f be Relation;
let n be Nat;
func iter (f,n) -> Relation means
:Def10:
ex p being sequence of bool [:field f,field f:] st
it = p.n & p.0 = id(field f) &
for k being Nat holds p.(k+1) = f*(p.k);
existence
proof
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
defpred P[Nat,Relation,set] means $3 = f * $2;
set FX = bool [:field f,field f:];
reconsider ID = id(field f) as Element of FX;
A1: for n being Nat for x being Element of FX ex y being
Element of FX st P[n,x,y]
proof
dom f c= field f & rng f c= field f by XBOOLE_1:7;
then reconsider h = f as Relation of field f, field f by RELSET_1:4;
let n be Nat;
let x be Element of FX;
reconsider g = x as Relation of field f,field f;
h * g is Element of FX;
hence thesis;
end;
consider p being sequence of FX such that
A2: p.0 = ID & for n being Nat holds P[n,p.n,p.(n+1)] from
RECDEF_1:sch 2(A1);
p.n9 is Relation of field f,field f;
hence thesis by A2;
end;
uniqueness by Lm2;
end;
registration
let f be Function;
let n be Nat;
cluster iter (f,n) -> Function-like;
coherence
proof
consider p being sequence of bool [:field f,field f:] such that
A1: p.n = iter(f,n) & p.0 = id(field f) and
A2: for k being Nat holds p.(k+1) = f*p.k by Def10;
defpred P[Nat] means p.$1 is Function;
A3: P[0] by A1;
A4: for m being Nat holds P[m] implies P[m+1]
proof let m be Nat;
assume P[m]; then
reconsider g = p.m as Function;
p.(m+1) = g*f by A2;
hence thesis;
end;
for m being Nat holds P[m] from NAT_1:sch 2(A3,A4);
hence thesis by A1;
end;
end;
reserve m,n,k for Nat, R for Relation;
Lm3: id(field R)*R = R & R*id(field R) = R by RELAT_1:51,53,XBOOLE_1:7;
theorem Th67:
iter (R,0) = id(field R)
proof
ex p being sequence of bool [:field R,field R:] st iter
(R,0) = p.0 & p.0 = id(field R) & for k being Nat holds p.(k+1) = R*p.k
by Def10;
hence thesis;
end;
Lm4: rng R c= dom R implies iter (R,0) = id(dom R)
proof
assume rng R c= dom R;
then field R = dom R by XBOOLE_1:12;
hence thesis by Th67;
end;
theorem Th68:
for n be Nat holds iter(R,n+1) = R*iter(R,n)
proof
let n be Nat;
consider p being sequence of bool [:field R,field R:] such
that
A1: p.(n+1) = iter(R,n+1) & p.0 = id(field R) and
A2: for k being Nat holds p.(k+1) = R*p.k by Def10;
p.(n+1) = R*p.n by A2;
hence thesis by A1,A2,Def10;
end;
theorem Th69:
iter(R,1) = R
proof
thus iter(R,1) = iter(R,0+1)
.= R*iter(R,0) by Th68
.= R*id(field R) by Th67
.= R by Lm3;
end;
theorem Th70:
for n being Nat holds iter(R,n+1) = iter(R,n)*R
proof
let n be Nat;
defpred P[Nat] means iter(R,$1+1) = iter(R,$1)*R;
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A2: iter(R,k+1) = iter(R,k)*R;
thus iter(R,k+1)*R = R*iter(R,k)*R by Th68
.= R*(iter(R,k)*R) by RELAT_1:36
.= iter(R,k+1+1) by A2,Th68;
end;
iter(R,0+1) = R by Th69
.= id(field R)*R by Lm3
.= iter(R,0)*R by Th67;
then
A3: P[ 0];
for k be Nat holds P[k] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th71:
dom iter(R,n) c= field R & rng iter(R,n) c= field R
proof
defpred P[Nat] means dom iter(R,$1) c= field R & rng iter(
R,$1) c= field R;
A1: P[k] implies P[k+1]
proof
iter(R,k+1) = iter(R,k)*R by Th70;
then
A2: dom iter(R,k+1) c= dom iter(R,k) by RELAT_1:25;
iter(R,k+1) = R*iter(R,k) by Th68;
then
A3: rng iter(R,k+1) c= rng iter(R,k) by RELAT_1:26;
assume dom iter(R,k) c= field R & rng iter(R,k) c= field R;
hence thesis by A2,A3,XBOOLE_1:1;
end;
iter(R,0) = id(field R) by Th67;
then
A4: P[ 0];
P[k] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
theorem
n <> 0 implies dom iter(R,n) c= dom R & rng iter(R,n) c= rng R
proof
defpred P[Nat] means dom iter(R,$1+1) c= dom R & rng iter(R,$1+1) c= rng R;
assume n <> 0;
then
A1: ex k be Nat st n = k+1 by NAT_1:6;
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume that
dom iter(R,k+1) c= dom R and
rng iter(R,k+1) c= rng R;
iter(R,k+1+1) = R*iter(R,k+1) & iter(R,k+1+1) = iter(R,k+1)*R by Th68,Th70;
hence thesis by RELAT_1:25,26;
end;
A3: P[ 0] by Th69;
for k be Nat holds P[k] from NAT_1:sch 2(A3,A2);
hence thesis by A1;
end;
theorem Th73:
for n being Nat st rng R c= dom R holds dom iter(R,n) = dom R &
rng iter(R,n) c= dom R
proof
let n be Nat;
defpred P[Nat] means dom iter(R,$1) = dom R & rng iter(R,$1) c= dom R;
A1: for k being Nat holds P[k] implies P[k+1]
proof
let k be Nat;
assume
A2: dom iter(R,k) = dom R & rng iter(R,k) c= dom R;
iter(R,k+1) = R*iter(R,k) by Th68;
then
A3: rng iter(R,k+1) c= rng iter(R,k) by RELAT_1:26;
iter(R,k+1) = iter(R,k)*R by Th70;
hence thesis by A2,A3,RELAT_1:27,XBOOLE_1:1;
end;
assume rng R c= dom R;
then iter(R,0) = id dom R by Lm4;
then
A4: P[ 0];
for k being Nat holds P[k] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
theorem Th74:
id(field R)*iter(R,n) = iter(R,n)
proof
dom iter(R,n) c= field R by Th71;
hence thesis by RELAT_1:51;
end;
theorem
iter(R,n)*id(field R) = iter(R,n)
proof
rng iter(R,n) c= field R by Th71;
hence thesis by RELAT_1:53;
end;
theorem Th76:
iter(R,m)*iter(R,n) = iter(R,n+m)
proof
defpred P[Nat] means iter(R,$1)*iter(R,n) = iter(R,n+$1);
A1: P[k] implies P[k+1]
proof
assume
A2: iter(R,k)*iter(R,n) = iter(R,n+k);
thus iter(R,k+1)*iter(R,n) = R*iter(R,k)*iter(R,n) by Th68
.= R*(iter(R,k)*iter(R,n)) by RELAT_1:36
.= iter(R,n+k+1) by A2,Th68
.= iter(R,n+(k+1));
end;
iter(R,0)*iter(R,n) = id(field R)*iter(R,n) by Th67
.= iter(R,n+0) by Th74;
then
A3: P[ 0];
P[k] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
Lm5: iter(iter(R,m),k) = iter(R,m*k) implies iter(iter(R,m),k+1) = iter(R,m*(k
+1))
proof
assume
A1: iter(iter(R,m),k) = iter(R,m*k);
thus iter(iter(R,m),k+1) = iter(R,m)*iter(iter(R,m),k) by Th68
.= iter(R,m*k + m*1) by A1,Th76
.= iter(R,m*(k+1));
end;
theorem
n <> 0 implies iter(iter(R,m),n) = iter(R,m*n)
proof
defpred P[Nat] means iter(iter(R,m),$1+1) = iter(R,m*($1+1));
A1: P[k] implies P[k+1] by Lm5;
A2: P[ 0] by Th69;
A3: P[k] from NAT_1:sch 2(A2,A1);
assume n <> 0;
then consider k be Nat such that
A4: n = k+1 by NAT_1:6;
reconsider k as Nat;
n=k+1 by A4;
hence thesis by A3;
end;
theorem Th78:
rng R c= dom R implies iter(iter(R,m),n) = iter(R,m*n)
proof
defpred P[Nat] means iter(iter(R,m),$1) = iter(R,m*$1);
assume
A1: rng R c= dom R;
then dom iter(R,m) = dom R by Th73;
then field iter(R,m) = dom R by A1,Th73,XBOOLE_1:12;
then iter(iter(R,m),0) = id(dom R) by Th67
.= id(field R) by A1,XBOOLE_1:12
.= iter(R,m*0) by Th67;
then
A2: P[ 0];
A3: P[k] implies P[k+1] by Lm5;
P[k] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem
iter({},n) = {}
proof
defpred P[Nat] means iter({},$1) = {};
A1: P[k] implies P[k+1]
proof
assume iter({},k) = {};
thus iter({},k+1) = iter({},k)*{} by Th68
.= {};
end;
iter({},0) = id (field {}) by Th67
.= {};
then
A2: P[0 ];
P[k] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem
iter(id(X),n) = id(X)
proof
defpred P[Nat] means iter(id(X),$1) = id(X);
A1: P[k] implies P[k+1]
proof
assume
A2: P[k];
thus iter(id(X),k+1) = iter(id(X),k)*id(X) by Th68
.= id(X) by A2,FUNCT_2:17;
end;
id(field id X) = id X;
then
A3: P[ 0] by Th67;
P[k] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem
rng R misses dom R implies iter(R,2) = {}
proof
assume
A1: rng R misses dom R;
thus iter(R,2) = iter(R,1+1)
.= iter(R,1)*R by Th70
.= R*R by Th69
.= {} by A1,RELAT_1:44;
end;
theorem
for n being Nat for f being Function of X,X holds iter(f,n) is
Function of X,X
proof
let n be Nat;
let f be Function of X,X;
A1: X = {} implies X = {};
then
A2: dom f = X by FUNCT_2:def 1;
A3: rng f c= X;
then dom iter(f,n) = X & rng iter(f,n) c= X by A2,Th73;
then reconsider R = iter(f,n) as Relation of X,X by RELSET_1:4;
dom R = X by A2,A3,Th73;
hence thesis by A1,FUNCT_2:def 1;
end;
theorem
for f being Function of X,X holds iter(f,0) = id X
proof
let f be Function of X,X;
iter(f,0) = id(field f) & field f = dom f by Lm1,Th67,XBOOLE_1:12;
hence thesis by FUNCT_2:52;
end;
theorem
for f being Function of X,X holds iter(iter(f,m),n) = iter(f,m*n)
proof
let f be Function of X,X;
rng f c= dom f by Lm1;
hence thesis by Th78;
end;
theorem
for f being PartFunc of X,X holds iter(f,n) is PartFunc of X,X
proof
let f be PartFunc of X,X;
A1: field f = dom f \/ rng f;
rng iter(f,n) c= field f by Th71;
then
A2: rng iter(f,n) c= X by A1,XBOOLE_1:1;
dom iter(f,n) c= field f by Th71;
then dom iter(f,n) c= X by A1,XBOOLE_1:1;
hence thesis by A2,RELSET_1:4;
end;
theorem
n <> 0 & a in X & f = X --> a implies iter(f,n) = f
proof
assume that
A1: n <> 0 and
A2: a in X and
A3: f = X --> a;
defpred P[Nat] means iter(f,$1+1) = f;
A4: now
A5: dom f = X by A3;
let k such that
A6: P[k];
A7: now
let x be object;
assume
A8: x in dom f;
then
A9: f.x = a by A3,FUNCOP_1:7;
thus iter(f,k+1+1).x = (f*f).x by A6,Th70
.= f.(f.x) by A8,FUNCT_1:13
.= f.x by A2,A3,A9,FUNCOP_1:7;
end;
rng f = {a} by A2,A3,FUNCOP_1:8;
then rng f c= dom f by A2,A5,ZFMISC_1:31;
then dom iter(f,k+1+1) = dom f by Th73;
hence P[k+1] by A7,FUNCT_1:2;
end;
A10: P[ 0] by Th69;
A11: P[k] from NAT_1:sch 2(A10,A4);
consider k be Nat such that
A12: n = k+1 by A1,NAT_1:6;
reconsider k as Nat;
n = k + 1 by A12;
hence thesis by A11;
end;
theorem
for f being Function, n being Nat holds iter(f,n) = compose
(n|->f,field f)
proof
let f be Function;
defpred P[Nat] means iter(f,$1) = compose($1|->f,field f);
A1: now
let n be Nat;
assume P[n];
then iter(f,n+1) = f*compose(n|->f,field f) by Th70
.= compose((n|->f)^<*f*>,field f) by Th40
.= compose((n+1)|->f,field f) by FINSEQ_2:60;
hence P[n+1];
end;
iter(f,0) = id (field f) by Th67
.= compose({},field f) by Th38
.= compose(0|->f,field f);
then
A2: P[ 0];
thus for n being Nat holds P[n] from NAT_1:sch 2(A2, A1);
end;
begin :: Addenda
:: from SCMFSA6A, 2006.03.14, A.T.
theorem
for f,g being Function, x,y being set st g c= f & not x in dom g holds
g c= f+*(x,y)
proof
let f,g be Function, x,y be set such that
A1: g c= f and
A2: not x in dom g;
A3: now
let z be object;
assume
A4: z in dom g;
hence g.z = f.z by A1,GRFUNC_1:2
.= (f+*(x,y)).z by A2,A4,Th31;
end;
dom g c= dom f by A1,GRFUNC_1:2;
then dom g c= dom(f+*(x,y)) by Th29;
hence thesis by A3,GRFUNC_1:2;
end;
theorem
for f,g being Function, A being set st f|A = g|A & f,g equal_outside A
holds f = g
proof
let f,g be Function, A be set such that
A1: f|A = g|A & f,g equal_outside A;
thus f = f|(dom f \/ A) by RELAT_1:68,XBOOLE_1:7
.= f|(dom f \ A \/ A) by XBOOLE_1:39
.= f|(dom f \ A) \/ f|A by RELAT_1:78
.= g|(dom g \ A) \/ g|A by A1
.= g|(dom g \ A \/ A) by RELAT_1:78
.= g|(dom g \/ A) by XBOOLE_1:39
.= g by RELAT_1:68,XBOOLE_1:7;
end;
theorem
for f being Function, a,b,A being set st a in A holds f,f+*(a,b)
equal_outside A
proof
let f be Function, a,b,A be set;
per cases;
suppose
A1: a in dom f;
assume a in A;
then {a} c= A by ZFMISC_1:31;
then
A2: dom(a.-->b) c= A;
f+*(a,b) = f+*(a.-->b) by A1,Def2;
hence thesis by A2,Th28;
end;
suppose
not a in dom f;
then f+*(a,b) = f by Def2;
hence thesis;
end;
end;
theorem Th91:
for f being Function, a,b being object,
A being set holds a in A or (f+*(a,b))
|A = f|A
proof
let f be Function, a,b be object, A be set;
per cases;
suppose
A1: a in dom f;
assume not a in A;
then {a} misses A by ZFMISC_1:50;
then
A2: dom (a.-->b) misses A;
thus (f+*(a,b))|A = (f +* (a.-->b))|A by A1,Def2
.= f|A by A2,FUNCT_4:72;
end;
suppose
not a in dom f;
hence thesis by Def2;
end;
end;
theorem
for f,g being Function, a,b be object,
A being set st f|A = g|A holds (f+*(a,b))|
A = (g+*(a,b))|A
proof
let f,g be Function, a,b be object, A be set such that
A1: f|A = g|A;
per cases;
suppose that
A2: a in A and
A3: a in dom g;
now
assume not a in dom f;
then not a in dom f /\ A by XBOOLE_0:def 4;
then not a in dom(g|A) by A1,RELAT_1:61;
then not a in dom g /\ A by RELAT_1:61;
hence contradiction by A2,A3,XBOOLE_0:def 4;
end;
hence (f+*(a,b))|A = (f +* (a.-->b))|A by Def2
.= g|A +* (a.-->b)|A by A1,FUNCT_4:71
.= (g +* (a.-->b))|A by FUNCT_4:71
.= (g+*(a,b))|A by A3,Def2;
end;
suppose that
A4: a in A and
A5: not a in dom g;
now
assume a in dom f;
then a in dom f /\ A by A4,XBOOLE_0:def 4;
then a in dom(g|A) by A1,RELAT_1:61;
then a in dom g /\ A by RELAT_1:61;
hence contradiction by A5,XBOOLE_0:def 4;
end;
hence (f+*(a,b))|A = g|A by A1,Def2
.= (g+*(a,b))|A by A5,Def2;
end;
suppose
A6: not a in A;
hence (f+*(a,b))|A = f|A by Th91
.= (g+*(a,b))|A by A1,A6,Th91;
end;
end;
:: from YELLOW14, 2006.03.14, A.T.
theorem Th93:
for f being Function, a, b being object holds (f +* (a .--> b)).a =
b
proof
let f be Function, a, b be object;
a in dom (a .--> b) by TARSKI:def 1;
hence (f +* (a .--> b)).a = (a .--> b).a by FUNCT_4:13
.= b by FUNCOP_1:72;
end;
:: from SCMFSA6A, 2006.03.14, A.T.
theorem
for a, b being set holds <*a*> +* (1,b) = <*b*>
proof
let a, b be set;
A1: dom <*b*> = {1} by FINSEQ_1:2,def 8;
A2: dom <*a*> = {1} by FINSEQ_1:2,def 8;
then 1 in dom <*a*> by TARSKI:def 1;
then
A3: <*a*> +* (1,b) = <*a*> +* (1 .--> b) by Def2;
A4: for x being object st x in {1} holds (<*a*> +* (1,b)).x = <*b*>.x
proof
let x be object;
assume x in {1};
then
A5: x = 1 by TARSKI:def 1;
hence (<*a*> +* (1,b)).x = b by A3,Th93
.= <*b*>.x by A5;
end;
dom (<*a*> +* (1,b)) = dom <*a*> \/ dom (1 .--> b) by A3,FUNCT_4:def 1
.= {1} \/ {1} by A2
.= {1};
hence thesis by A1,A4;
end;
:: from SCMFSA8C, 2006.03.15
theorem
for f be Function, x be set st x in dom f holds f +* (x .--> f.x) = f
proof
let f be Function;
let x be set;
assume x in dom f;
hence f +* (x .--> f.x) = f +*(x,f.x) by Def2
.= f by Th34;
end;
:: from JORDAN2B, 2007.03.18, A.T.
reserve i,j for Nat;
theorem Th96:
for w being FinSequence,r being object,i being natural Number
holds len (w+*(i,r))=len w
proof
let w be FinSequence,r be object,i be natural Number;
dom ( w+*(i,r))=dom w by Th29;
then Seg len ( w+*(i,r))=dom w by FINSEQ_1:def 3
.=Seg len w by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:6;
end;
theorem
for D being non empty set, w being FinSequence of D, r being Element
of D st i in dom w holds w+*(i,r)=(w|(i-'1))^<*r*>^(w/^i)
proof
let D be non empty set, w be FinSequence of D, r be Element of D;
assume
A1: i in dom w;
then
A2: 1<=i by FINSEQ_3:25;
A3: i<=len w by A1,FINSEQ_3:25;
A4: len ((w|(i-'1))^<*r*>^(w/^i)) =len ((w|(i-'1))^<*r*>)+len(w/^i) by
FINSEQ_1:22
.=len (w|(i-'1))+len<*r*>+len(w/^i) by FINSEQ_1:22
.=len (w|(i-'1))+1+len(w/^i) by FINSEQ_1:39
.=(i-'1)+1+len(w/^i) by A3,FINSEQ_1:59,NAT_D:44
.=(i-'1)+1+(len w-i) by A3,RFINSEQ:def 1
.=(i-1)+1+(len w-i) by A2,XREAL_1:233;
for j be Nat st 1<=j & j<=len (w+*(i,r)) holds (w+*(i,r)).j=((w|(i-'1))^
<*r*>^(w/^i)).j
proof
A5: len (w|(i-'1)) =(i-'1) by A3,FINSEQ_1:59,NAT_D:44
.=(i-1) by A2,XREAL_1:233;
let j be Nat;
assume that
A6: 1<=j and
A7: j<=len (w+*(i,r));
A8: len ((w|(i-'1))^<*r*>) =len (w|(i-'1))+len<*r*> by FINSEQ_1:22
.=len (w|(i-'1))+1 by FINSEQ_1:39
.=(i-'1)+1 by A3,FINSEQ_1:59,NAT_D:44
.=(i-1)+1 by A2,XREAL_1:233
.=i;
A9: len (w+*(i,r))=len (w) by Th96;
now
per cases by XXREAL_0:1;
case
A10: i<j;
then i+1<=j by NAT_1:13;
then
A11: i+1-i<=j-i by XREAL_1:9;
then
A12: 1<=j-'i by NAT_D:39;
A13: j-i<=len w-i by A7,A9,XREAL_1:9;
A14: i<=len w by A1,FINSEQ_3:25;
len (w/^i)=len w -'i by RFINSEQ:29
.=len w -i by A14,XREAL_1:233;
then j-'i<=len (w/^i) by A11,A13,NAT_D:39;
then
A15: j-'i in dom (w/^i) by A12,FINSEQ_3:25;
j<=len ((w|(i-'1))^<*r*>^(w/^i)) by A4,A7,Th96;
then
((w|(i-'1))^<*r*>^(w/^i)).j =(w/^i).(j-len ((w|(i-'1))^<*r*>)) by A8
,A10,FINSEQ_1:24
.=(w/^i).(j-'i) by A8,A10,XREAL_1:233
.=w.(j-'i+i) by A14,A15,RFINSEQ:def 1
.=w.j by A10,XREAL_1:235;
hence thesis by A10,Th31;
end;
case
A16: j=i;
A17: i=len (w|(i-'1))+1 by A5;
((w|(i-'1))^<*r*>^(w/^i)).j =((w|(i-'1))^<*r*>).i by A6,A8,A16,
FINSEQ_1:64
.=r by A17,FINSEQ_1:42;
hence thesis by A1,A16,Th30;
end;
case
A18: j<i;
then j+1<=i by NAT_1:13;
then
A19: j+1-1<=i-1 by XREAL_1:9;
then
A20: j<=i-'1 by A2,XREAL_1:233;
((w|(i-'1))^<*r*>^(w/^i)).j =((w|(i-'1))^<*r*>).j by A6,A8,A18,
FINSEQ_1:64
.=(w|(i-'1)).j by A6,A5,A19,FINSEQ_1:64
.= w.j by A20,FINSEQ_3:112;
hence thesis by A18,Th31;
end;
end;
hence thesis;
end;
hence thesis by A4,Th96,FINSEQ_1:14;
end;
:: comp. FINSEQ_7, 2007.03.18, A.T.
reserve F for Function,
e,x,y,z for object;
definition
let F;
let x,y be object;
func Swap(F,x,y) -> set equals
:Def11:
F+*(x,F.y)+*(y,F.x) if x in dom F & y in dom
F otherwise F;
correctness;
end;
registration
let F;
let x,y be object;
cluster Swap(F,x,y) -> Relation-like Function-like;
coherence
proof
per cases;
suppose
x in dom F & y in dom F;
then Swap(F,x,y) = F+*(x,F.y)+*(y,F.x) by Def11;
hence thesis;
end;
suppose
not(x in dom F & y in dom F);
hence thesis by Def11;
end;
end;
end;
theorem Th98:
for x,y being object holds dom Swap(F,x,y) = dom F
proof let x,y be object;
per cases;
suppose
x in dom F & y in dom F;
hence dom Swap(F,x,y) = dom(F+*(x,F.y)+*(y,F.x)) by Def11
.= dom(F+*(x,F.y)) by Th29
.= dom F by Th29;
end;
suppose
not(x in dom F & y in dom F);
hence thesis by Def11;
end;
end;
theorem Th99:
for x,y being object holds rng(F+*(x,y)) c= rng F \/ {y}
proof let x,y be object;
A1: rng(x.-->y) = {y} by FUNCOP_1:8;
per cases;
suppose
x in dom F;
then F+*(x,y) = F+*(x.-->y) by Def2;
hence thesis by A1,FUNCT_4:17;
end;
suppose
not x in dom F;
then F+*(x,y) = F by Def2;
hence thesis by XBOOLE_1:7;
end;
end;
theorem Th100:
for x,y being object holds rng F c= rng(F+*(x,y)) \/ {F.x}
proof let x,y be object;
let z be object;
assume z in rng F;
then consider e being object such that
A1: e in dom F and
A2: z = F.e by FUNCT_1:def 3;
A3: dom F = dom(F+*(x,y)) by Th29;
per cases;
suppose
e = x;
then z in {F.x} by A2,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
e <> x;
then (F+*(x,y)).e = F.e by Th31;
then z in rng(F+*(x,y)) by A1,A2,A3,FUNCT_1:3;
hence thesis by XBOOLE_0:def 3;
end;
end;
theorem Th101:
x in dom F implies y in rng(F+*(x,y))
proof
assume x in dom F;
then x in dom (F+*(x,y)) & (F+*(x,y)).x = y by Th29,Th30;
hence thesis by FUNCT_1:3;
end;
theorem
for x,y being object holds rng Swap(F,x,y) = rng F
proof let x,y be object;
per cases;
suppose that
A1: x in dom F and
A2: y in dom F;
F.x in rng F by A1,FUNCT_1:3;
then F.x in rng F \/ {F.y} by XBOOLE_0:def 3;
then rng F \/ {F.y} \/ {F.x} = rng F \/ {F.y} by ZFMISC_1:40
.= rng F by A2,FUNCT_1:3,ZFMISC_1:40;
then
A3: rng(F+*(x,F.y)) \/ {F.x} c= rng F by Th99,XBOOLE_1:9;
A4: (F+*(x,F.y)).y = F.y
proof
per cases;
suppose
x <> y;
hence thesis by Th31;
end;
suppose
x = y;
hence thesis by A1,Th30;
end;
end;
A5: rng F c= rng(F+*(x,F.y)) \/ {F.x} by Th100;
A6: Swap(F,x,y) = F+*(x,F.y)+*(y,F.x) by A1,A2,Def11;
then rng Swap(F,x,y) c= rng(F+*(x,F.y)) \/ {F.x} by Th99;
then
A7: rng Swap(F,x,y) c= rng F by A3;
A8: y in dom(F+*(x,F.y)) by A2,Th29;
A9: F.y in rng Swap(F,x,y)
proof
per cases;
suppose
F.x = F.y;
hence thesis by A6,A8,Th101;
end;
suppose
A10: F.x <> F.y;
A11: dom Swap(F,x,y) = dom F by Th98;
Swap(F,x,y).x = F+*(x,F.y).x by A6,A10,Th31
.= F.y by A1,Th30;
hence thesis by A1,A11,FUNCT_1:3;
end;
end;
F.x in rng Swap(F,x,y) by A6,A8,Th101;
then F.x in rng Swap(F,x,y) \/ {F.y} by XBOOLE_0:def 3;
then rng Swap(F,x,y) \/ {F.y} \/ {F.x} = rng Swap(F,x,y) \/ {F.y} by
ZFMISC_1:40
.= rng Swap(F,x,y) by A9,ZFMISC_1:40;
then rng(F+*(x,F.y)) \/ {F.x} c= rng Swap(F,x,y) by A6,A4,Th100,XBOOLE_1:9;
then rng F c= rng Swap(F,x,y) by A5;
hence thesis by A7;
end;
suppose
not(x in dom F & y in dom F);
hence thesis by Def11;
end;
end;
:: from SCMFSA_7, 2007.07.22, A.T.
scheme
{ A() -> set, D() -> non empty set, G(object) -> object }:
A(),{ G(d) where d is Element of D() : d in A() } are_equipotent
provided
A1: A() c= D() and
A2: for d1,d2 being Element of D() st d1 in A() & d2 in A() & G(d1) = G(
d2) holds d1 = d2
proof
per cases;
suppose
A() <> {};
then reconsider D = A() as non empty set;
set X = { G(d) where d is Element of D : d in A() };
set Y = { G(d) where d is Element of D() : d in A() };
A3: now
let x be object;
hereby
assume x in X;
then ex d being Element of D st G(d) = x & d in A();
hence x in Y by A1;
end;
hereby
assume x in Y;
then ex d being Element of D() st G(d) = x & d in A();
hence x in X;
end;
end;
A4: now
let d1,d2 be Element of D;
reconsider d = d1, dd = d2 as Element of D() by A1;
assume G(d1) = G(d2);
then d = dd by A2;
hence d1 = d2;
end;
A5: A() c= D;
A(),X are_equipotent from CardMono9(A5,A4);
hence thesis by A3,TARSKI:2;
end;
suppose
A6: A() = {};
now
set a =the Element of { G(d) where d is Element of D() : d in A() };
assume { G(d) where d is Element of D() : d in A() } <> {};
then a in { G(d) where d is Element of D() : d in A() };
then ex d being Element of D() st a = G(d) & d in A();
hence contradiction by A6;
end;
hence thesis by A6;
end;
end;
:: from SCMFSA6A, 2007.07.23, A.T.
theorem
for f,g,h being Function, A being set holds f, g equal_outside A
implies f +* h, g +* h equal_outside A
proof
let f,g,h be Function;
let A be set;
A1: dom ((f +* h) | (dom (f +* h) \ A)) = dom (f +* h) \ A by RELAT_1:156
.= (dom f \/ dom h) \ A by FUNCT_4:def 1
.= (dom f \ A) \/ (dom h \ A) by XBOOLE_1:42;
assume f,g equal_outside A;
then
A2: f|(dom f \ A) = g|(dom g \ A);
then
A3: dom f \ A = dom (g|(dom g \ A)) by RELAT_1:156
.= dom g \ A by RELAT_1:156;
then
A4: dom ((f +* h) | (dom (f +* h) \ A)) = (dom g \/ dom h) \ A by A1,
XBOOLE_1:42
.= dom (g +* h) \ A by FUNCT_4:def 1
.= dom ((g +* h) | (dom (g +* h) \ A)) by RELAT_1:156;
now
let x be object;
assume
A5: x in dom ((f +* h) | (dom (f +* h) \ A));
then
A6: x in dom f \ A or x in dom h \ A by A1,XBOOLE_0:def 3;
per cases;
suppose
A7: x in dom h \ A;
thus ((f +* h) | (dom (f +* h) \ A)).x = (f +* h).x by A5,FUNCT_1:47
.= h.x by A7,FUNCT_4:13
.= (g +* h).x by A7,FUNCT_4:13
.= ((g +* h) | (dom (g +* h) \ A)).x by A4,A5,FUNCT_1:47;
end;
suppose
A8: not x in dom h \ A;
not x in A by A6,XBOOLE_0:def 5;
then
A9: not x in dom h by A8,XBOOLE_0:def 5;
A10: x in dom f \ A by A1,A5,A8,XBOOLE_0:def 3;
thus ((f +* h) | (dom (f +* h) \ A)).x = (f +* h).x by A5,FUNCT_1:47
.= f.x by A9,FUNCT_4:11
.= (g | (dom g \ A)).x by A2,A6,A8,FUNCT_1:49
.= g.x by A3,A10,FUNCT_1:49
.= (g +* h).x by A9,FUNCT_4:11
.= ((g +* h) | (dom (g +* h) \ A)).x by A4,A5,FUNCT_1:47;
end;
end;
then (f +* h) | (dom (f +* h) \ A) = (g +* h) | (dom (g +* h) \ A) by A4;
hence thesis;
end;
theorem
for f,g,h being Function, A being set holds f, g equal_outside A
implies h +* f, h +* g equal_outside A
proof
let f,g,h be Function;
let A be set;
assume f,g equal_outside A;
then
A1: f | (dom f \ A) = g | (dom g \ A);
then
A2: dom f \ A = dom (g | (dom g \ A)) by RELAT_1:156
.= dom g \ A by RELAT_1:156;
A3: dom ((h +* f) | (dom (h +* f) \ A)) = dom (h +* f) \ A by RELAT_1:156
.= (dom h \/ dom f) \ A by FUNCT_4:def 1
.= (dom h \ A) \/ (dom f \ A) by XBOOLE_1:42;
then
A4: dom ((h +* f) | (dom (h +* f) \ A)) = (dom h \/ dom g) \ A by A2,
XBOOLE_1:42
.= dom (h +* g) \ A by FUNCT_4:def 1
.= dom ((h +* g) | (dom (h +* g) \ A)) by RELAT_1:156;
now
let x be object;
assume
A5: x in dom ((h +* f) | (dom (h +* f) \ A));
then
A6: x in dom h \ A or x in dom f \ A by A3,XBOOLE_0:def 3;
per cases;
suppose
A7: x in dom f \ A;
thus ((h +* f) | (dom (h +* f) \ A)).x = (h +* f).x by A5,FUNCT_1:47
.= f.x by A7,FUNCT_4:13
.= (g | (dom g \ A)).x by A1,A7,FUNCT_1:49
.= g.x by A2,A7,FUNCT_1:49
.= (h +* g).x by A2,A7,FUNCT_4:13
.= ((h +* g) | (dom (h +* g) \ A)).x by A4,A5,FUNCT_1:47;
end;
suppose
A8: not x in dom f \ A;
A9: not x in A by A6,XBOOLE_0:def 5;
then
A10: not x in dom f by A8,XBOOLE_0:def 5;
A11: not x in dom g by A2,A8,A9,XBOOLE_0:def 5;
thus ((h +* f) | (dom (h +* f) \ A)).x = (h +* f).x by A5,FUNCT_1:47
.= h.x by A10,FUNCT_4:11
.= (h +* g).x by A11,FUNCT_4:11
.= ((h +* g) | (dom (h +* g) \ A)).x by A4,A5,FUNCT_1:47;
end;
end;
then (h +* f) | (dom (h +* f) \ A) = (h +* g) | (dom (h +* g) \ A) by A4;
hence thesis;
end;
theorem
for f,g,h being Function holds f +* h = g +* h iff f,g equal_outside
dom h
proof
let f,g,h be Function;
thus f +* h = g +* h implies f,g equal_outside dom h
proof
assume f +* h = g +* h;
then
A1: f +* h,g equal_outside dom h by Th25,Th28;
f, f +* h equal_outside dom h by Th28;
hence thesis by A1;
end;
assume
A2: f,g equal_outside dom h;
then
A3: dom f \ dom h = dom g \ dom h by Th27;
A4: for x being object st x in dom (f +* h) holds (f +* h).x = (g +* h).x
proof
let x be object;
assume
A5: x in dom (f +* h);
per cases;
suppose
A6: x in dom h;
hence (f +* h).x = h.x by FUNCT_4:13
.= (g +* h).x by A6,FUNCT_4:13;
end;
suppose
A7: not x in dom h;
dom (f +* h) = dom f \/ dom h by FUNCT_4:def 1;
then x in dom f by A5,A7,XBOOLE_0:def 3;
then
A8: x in dom f \ dom h by A7,XBOOLE_0:def 5;
A9: f|(dom f \ dom h) = g|(dom g \ dom h) by A2;
thus (f +* h).x = f.x by A7,FUNCT_4:11
.= g|(dom g \ dom h).x by A9,A8,FUNCT_1:49
.= g.x by A3,A8,FUNCT_1:49
.= (g +* h).x by A7,FUNCT_4:11;
end;
end;
dom (f +* h) = dom f \/ dom h by FUNCT_4:def 1
.= (dom g \ dom h) \/ dom h by A3,XBOOLE_1:39
.= dom g \/ dom h by XBOOLE_1:39
.= dom (g +* h) by FUNCT_4:def 1;
hence thesis by A4;
end;
:: from SF_MASTR, 2007.07.25, A.T.
theorem Th106:
for x, y, a being object, f being Function st f.x = f.y holds f.a
= (f*((id dom f)+*(x,y))).a
proof
let x, y, a be object, f be Function;
assume
A1: f.x = f.y;
set g1 = (id dom f)+*(x,y);
A2: dom id dom f = dom f;
per cases;
suppose
not x in dom f;
then id dom f = g1 by Def2;
hence thesis by RELAT_1:52;
end;
suppose
A3: x in dom f;
A4: dom g1 = dom f by A2,Th29;
A5: g1.x = y by A2,A3,Th30;
thus f.a = (f*((id dom f)+*(x,y))).a
proof
per cases;
suppose
A6: a in dom f;
now
assume a <> x;
then g1.a = (id dom f).a by Th31
.= a by A6,FUNCT_1:18;
hence thesis by A4,A6,FUNCT_1:13;
end;
hence thesis by A1,A3,A5,A4,FUNCT_1:13;
end;
suppose
A7: not a in dom f;
dom (f*g1) c= dom g1 by RELAT_1:25;
then not a in dom (f*g1) by A4,A7;
then (f*g1).a = {} by FUNCT_1:def 2;
hence thesis by A7,FUNCT_1:def 2;
end;
end;
end;
end;
theorem
for x, y being set, f being Function st x in dom f implies y in dom f
& f.x = f.y holds f = f*((id dom f)+*(x,y))
proof
let x, y be set, f be Function;
assume
A1: x in dom f implies y in dom f & f.x = f.y;
set g1 = (id dom f)+*(x,y);
set g = f*g1;
A2: dom id dom f = dom f;
per cases;
suppose
not x in dom f;
then id dom f = g1 by Def2;
hence thesis by RELAT_1:52;
end;
suppose
A3: x in dom f;
A4: dom g1 = dom f by A2,Th29;
now
rng g1 c= dom f
proof
let b be object;
assume b in rng g1;
then consider a being object such that
A5: a in dom g1 and
A6: b = g1.a by FUNCT_1:def 3;
per cases;
suppose
a = x;
hence thesis by A1,A2,A3,A6,Th30;
end;
suppose
a <> x;
then (id dom f).a = g1.a by Th31;
hence thesis by A4,A5,A6,FUNCT_1:18;
end;
end;
hence dom f = dom g by A4,RELAT_1:27;
let a be object;
assume a in dom f;
thus f.a = g.a by A1,A3,Th106;
end;
hence thesis;
end;
end;
::$CT
:: from SFMASTR3, 2007.07.26, A.T.
theorem Th109:
for X being set, p being Permutation of X, x, y being Element
of X holds p+*(x, p.y)+*(y, p.x) is Permutation of X
proof
let X be set, p be Permutation of X, x, y be Element of X;
set p1 = p+*(x, p.y);
set p2 = p1+*(y, p.x);
A1: dom p2 = dom p1 by Th29;
A2: dom p1 = dom p by Th29;
A3: X = {} implies X = {};
then
A4: dom p = X by FUNCT_2:def 1;
per cases;
suppose
X is empty;
then p2 = {};
hence thesis by A3;
end;
suppose
A5: X is non empty;
A6: rng p = X by FUNCT_2:def 3;
then
A7: p.x in X by A4,A5,FUNCT_1:def 3;
thus p+*(x, p.y)+*(y, p.x) is Permutation of X
proof
per cases;
suppose
A8: x = y;
then p2 = p1 by Th34
.= p by A8,Th34;
hence thesis;
end;
suppose
A9: x <> y;
then
A10: p2.x = p1.x by Th31
.= p.y by A4,A5,Th30;
A11: now
let z be set such that
z in X and
A12: z <> x and
A13: z <> y;
thus p2.z = p1.z by A13,Th31
.= p.z by A12,Th31;
end;
A14: p2.y = p.x by A2,A4,A5,Th30;
A15: now
let pz be object;
hereby
assume pz in rng p2;
then consider z being object such that
A16: z in dom p2 and
A17: pz = p2.z by FUNCT_1:def 3;
A18: p.z in X by A1,A2,A6,A16,FUNCT_1:def 3;
per cases;
suppose
z = x;
hence pz in X by A4,A5,A6,A10,A17,FUNCT_1:def 3;
end;
suppose
z = y;
hence pz in X by A2,A4,A7,A17,Th30;
end;
suppose
z <> x & z <> y;
hence pz in X by A1,A2,A11,A16,A17,A18;
end;
end;
assume pz in X;
then consider z being object such that
A19: z in dom p and
A20: pz = p.z by A6,FUNCT_1:def 3;
per cases;
suppose
z = x;
hence pz in rng p2 by A1,A2,A4,A14,A19,A20,FUNCT_1:def 3;
end;
suppose
z = y;
hence pz in rng p2 by A1,A2,A4,A10,A19,A20,FUNCT_1:def 3;
end;
suppose
z <> x & z <> y;
then p2.z = p.z by A11,A19;
hence pz in rng p2 by A1,A2,A19,A20,FUNCT_1:def 3;
end;
end;
then rng p2 = X by TARSKI:2;
then reconsider p2 as Function of X, X by A1,A2,A4,A5,FUNCT_2:def 1
,RELSET_1:4;
now
let z1, z2 be object such that
A21: z1 in X and
A22: z2 in X and
A23: p2.z1 = p2.z2 and
A24: z1 <> z2;
per cases;
suppose
z1 = x & z2 = y;
hence contradiction by A5,A9,A10,A14,A23,FUNCT_2:19;
end;
suppose
z1 = y & z2 = x;
hence contradiction by A5,A9,A10,A14,A23,FUNCT_2:19;
end;
suppose
A25: z1 = x & z2 <> y;
then p2.z2 = p.z2 by A11,A22,A24;
hence contradiction by A10,A22,A23,A25,FUNCT_2:19;
end;
suppose
A26: z1 <> x & z2 = y;
then p2.z1 = p.z1 by A11,A21,A24;
hence contradiction by A14,A21,A23,A26,FUNCT_2:19;
end;
suppose
A27: z1 = y & z2 <> x;
then p2.z2 = p.z2 by A11,A22,A24;
hence contradiction by A14,A22,A23,A27,FUNCT_2:19;
end;
suppose
A28: z1 <> y & z2 = x;
then p2.z1 = p.z1 by A11,A21,A24;
hence contradiction by A10,A21,A23,A28,FUNCT_2:19;
end;
suppose
z1 <> y & z2 <> x & z1 <> x & z2 <> y;
then p2.z1 = p.z1 & p2.z2 = p.z2 by A11,A21,A22;
hence contradiction by A21,A22,A23,A24,FUNCT_2:19;
end;
end;
then
A29: p2 is one-to-one by A5,FUNCT_2:19;
rng p2 = X by A15,TARSKI:2;
then p2 is onto by FUNCT_2:def 3;
hence thesis by A29;
end;
end;
end;
end;
theorem
for f being Function, x, y being set st x in dom f & y in dom f ex p
being Permutation of dom f st f+*(x, f.y)+*(y, f.x) = f*p
proof
let f be Function, x, y be set such that
A1: x in dom f and
A2: y in dom f;
set i = id dom f;
i.x = x & i.y = y by A1,A2,FUNCT_1:18;
then reconsider p = i+*(x,y)+*(y,x) as Permutation of dom f by A1,A2,Th109;
set pk = i+*(x, y);
set fr = f*p;
set fk = f+*(x, f.y);
take p;
set fl = fk+*(y, f.x);
A3: dom i = dom f;
A4: dom fk = dom fl by Th29;
A5: dom p = dom pk by Th29;
A6: dom pk = dom i by Th29;
A7: dom f = dom fk by Th29;
now
thus dom f = dom fl by A4,Th29;
rng p = dom f by FUNCT_2:def 3;
hence dom f = dom fr by A5,A6,RELAT_1:27;
let z be object such that
A8: z in dom f;
per cases;
suppose
A9: x <> y;
thus fl.z = fr.z
proof
per cases;
suppose
A10: z = x;
hence fl.z = fk.z by A9,Th31
.= f.y by A8,A10,Th30
.= f.(pk.x) by A1,A3,Th30
.= f.(p.x) by A9,Th31
.= fr.z by A5,A6,A8,A10,FUNCT_1:13;
end;
suppose
A11: z = y;
hence fl.z = f.x by A7,A8,Th30
.= f.(p.y) by A2,A6,Th30
.= fr.z by A5,A6,A8,A11,FUNCT_1:13;
end;
suppose
A12: z <> x & z <> y;
then
A13: p.z = pk.z by Th31
.= i.z by A12,Th31
.= z by A8,FUNCT_1:18;
thus fl.z = fk.z by A12,Th31
.= f.(p.z) by A12,A13,Th31
.= fr.z by A5,A6,A8,FUNCT_1:13;
end;
end;
end;
suppose
A14: x = y;
A15: x = i.x by A1,FUNCT_1:17;
fk = f & i = i+*(x, i.y) by A14,Th34;
hence fl.z = fr.z by A14,A15,RELAT_1:52;
end;
end;
hence thesis;
end;
:: from SCMISORT, 2007.07.26, A.T.
theorem
for f be Function,d,r be set st d in dom f holds dom f=dom (f+*(d.-->r
))
proof
let f be Function,d,r be set;
assume
A1: d in dom f;
thus dom f=dom (f+*(d,r)) by Th29
.=dom (f+*(d.-->r)) by A1,Def2;
end;
:: from SCMBISORT, 2007.07.26, A.T.
theorem
for f,g be FinSequence of INT,m,n be Nat st 1<=n & n <= len
f & 1<=m & m <= len f & g=f+*(m,f/.n) +*(n,f/.m) holds f.m=g.n & f.n=g.m & (for
k be set st k<>m & k<>n & k in dom f holds f.k=g.k) & f,g
are_fiberwise_equipotent
proof
let f,g be FinSequence of INT,m,n be Nat;
assume that
A1: 1<=n & n <= len f and
A2: 1<=m & m <= len f and
A3: g=f+*(m,f/.n) +*(n,f/.m);
A4: dom (f+*(m,f/.n))=dom f by Th29;
A5: n in dom f by A1,FINSEQ_3:25;
hence
A6: g.n=f/.m by A3,A4,Th30
.=f.m by A2,FINSEQ_4:15;
A7: m in dom f by A2,FINSEQ_3:25;
thus
A8: now
per cases;
suppose
m=n;
hence g.m=f.n by A6;
end;
suppose
m<>n;
hence g.m=(f+*(m,f/.n)).m by A3,Th31
.=f/.n by A7,Th30
.=f.n by A1,FINSEQ_4:15;
end;
end;
A9: now
let k be set;
assume that
A10: k<>m and
A11: k<>n and
k in dom f;
thus g.k=(f+*(m,f/.n)).k by A3,A11,Th31
.=f.k by A10,Th31;
end;
dom g =dom f by A3,A4,Th29;
hence thesis by A5,A7,A6,A8,A9,RFINSEQ:28;
end;
:: from SCMFSA10, 2007.07.27, A.T.
theorem
for f being Function, a, A, b, B, c, C being set st a <> b & a <> c
holds ( f +* (a .--> A) +* (b .--> B) +* (c .--> C) ).a = A
proof
let f be Function, a, A, b, B, c, C be set;
assume a <> b & a <> c;
hence
( f +* (a .--> A) +* (b .--> B) +* (c .--> C) ).a = ( f +* (a .--> A) )
.a by FUNCT_4:91
.= A by Th93;
end;
:: comp TOPALG_3:1, 2008.01.18, A.T.
theorem Th114:
for A, B, a, b being set, f being Function of A,B st b in B
holds f +* (a,b) is Function of A,B
proof
let A, B, a, b be set, f be Function of A,B such that
A1: b in B;
A2: dom f = A by A1,FUNCT_2:def 1;
per cases;
suppose
not a in A;
hence thesis by A2,Def2;
end;
suppose
A3: a in A;
set g = a .--> b;
set f1 = f +* g;
rng g = {b} by FUNCOP_1:8;
then rng g c= B by A1,ZFMISC_1:31;
then
A4: rng f1 c= rng f \/ rng g & rng f \/ rng g c= B \/ B by FUNCT_4:17
,XBOOLE_1:13;
A5: {a} c= A by A3,ZFMISC_1:31;
dom f1 = A \/ dom g by A2,FUNCT_4:def 1
.= A \/ {a}
.= A by A5,XBOOLE_1:12;
then
A6: f +* g is Function of A,B by A4,FUNCT_2:2,XBOOLE_1:1;
a in dom f by A1,A3,FUNCT_2:def 1;
hence thesis by A6,Def2;
end;
end;
:: missing, 2008.03.23, A.T.
theorem Th115:
rng f c= A implies f+~(x,y) = (id A+*(x,y))*f
proof
assume
A1: rng f c= A;
per cases;
suppose
x in A;
then
A2: x in dom id A;
thus f+~(x,y) = (id A)*f+*((x.-->y)*f) by A1,RELAT_1:53
.= (id A+*(x.-->y))*f by Th10
.= (id A+*(x,y))*f by A2,Def2;
end;
suppose
A3: not x in A;
then
A4: not x in dom id A;
not x in rng f by A1,A3;
hence f+~(x,y) = f by FUNCT_4:103
.= (id A)*f by A1,RELAT_1:53
.= (id A+*(x,y))*f by A4,Def2;
end;
end;
theorem
(f+*g)+~(x,y) = f+~(x,y)+*(g+~(x,y))
proof
set A = rng f \/ rng g;
A1: g+~(x,y) =(id A+*(x,y))*g by Th115,XBOOLE_1:7;
A2: dom(id A+*(x,y)) = dom id A by Th29
.= A;
rng(f+*g) c= A by FUNCT_4:17;
hence (f+*g)+~(x,y) = (id A+*(x,y))*(f+*g) by Th115
.= (id A+*(x,y))*f+*((id A+*(x,y))*g) by A2,Th9,XBOOLE_1:7
.= f+~(x,y)+*(g+~(x,y)) by A1,Th115,XBOOLE_1:7;
end;
definition
let a,b be set;
func a followed_by b -> set equals
(NAT --> b) +* (0,a);
coherence;
end;
registration
let a,b be set;
cluster a followed_by b -> Function-like Relation-like;
coherence;
end;
reserve a,b,c for set;
theorem Th117:
dom(a followed_by b) = NAT
proof
thus dom(a followed_by b) = dom((NAT --> b) +* (0,a))
.= dom(NAT --> b) by Th29
.= NAT;
end;
definition
let X be non empty set;
let a,b be Element of X;
redefine func a followed_by b -> sequence of X; :: redefines followed_by (FUNCT_7, definition)
coherence
proof
a followed_by b = (NAT --> b) +* (0,a);
hence thesis by Th114;
end;
end;
theorem Th118:
(a followed_by b).0 = a
proof
dom(NAT --> b) = NAT;
hence thesis by Th30;
end;
theorem Th119:
for n st n > 0 holds (a followed_by b).n = b
proof
let n;
A1: n in NAT by ORDINAL1:def 12;
assume n > 0;
hence (a followed_by b).n = (NAT --> b).n by Th31
.= b by A1,FUNCOP_1:7;
end;
:: from DYNKIN, 2008.09.24, A.T.
definition
let a,b,c be set;
func (a,b) followed_by c -> set equals
(NAT --> c) +* ((0,1) --> (a,b));
coherence;
end;
registration
let a,b,c be set;
cluster (a,b) followed_by c -> Function-like Relation-like;
coherence;
end;
theorem Th120:
dom (a,b) followed_by c = NAT
proof
thus dom (a,b) followed_by c = dom(NAT --> c) \/ dom (0,1) --> (a,b) by
FUNCT_4:def 1
.= NAT \/ dom (0,1) --> (a,b)
.= NAT \/ {0,1} by FUNCT_4:62
.= NAT by XBOOLE_1:12;
end;
theorem Th121:
((a,b) followed_by c).0 = a
proof
dom (0,1) --> (a,b) = {0,1} by FUNCT_4:62;
then
A1: 0 in dom (0,1) --> (a,b) by TARSKI:def 2;
thus ((a,b) followed_by c).0 = ((NAT --> c) +* ((0,1) --> (a,b))).0
.= ((0,1) --> (a,b)).0 by A1,FUNCT_4:13
.= a by FUNCT_4:63;
end;
theorem Th122:
((a,b) followed_by c).1 = b
proof
dom (0,1) --> (a,b) = {0,1} by FUNCT_4:62;
then
A1: 1 in dom (0,1) --> (a,b) by TARSKI:def 2;
thus ((a,b) followed_by c).1 = ((NAT --> c) +* ((0,1) --> (a,b))).1
.= ((0,1) --> (a,b)).1 by A1,FUNCT_4:13
.= b by FUNCT_4:63;
end;
theorem Th123:
for n st n > 1 holds ((a,b) followed_by c).n = c
proof
let n;
assume
A1: n > 1;
dom (0,1) --> (a,b) = {0,1} by FUNCT_4:62;
then
A2: not n in dom (0,1) --> (a,b) by A1,TARSKI:def 2;
A3: n in NAT by ORDINAL1:def 12;
thus ((a,b) followed_by c).n = ((NAT --> c) +* ((0,1) --> (a,b))).n
.= (NAT --> c).n by A2,FUNCT_4:11
.= c by A3,FUNCOP_1:7;
end;
theorem Th124:
(a,b) followed_by c = (a followed_by c) +* (1,b)
proof
set f = (a,b) followed_by c, g = (a followed_by c) +* (1,b);
A1: dom(a followed_by c) = NAT by Th117;
A2: dom f = NAT by Th120;
hence dom f = dom g by A1,Th29;
let x be object;
assume x in dom f;
then reconsider n=x as Nat by A2;
per cases by NAT_1:25;
suppose
A3: n = 0;
hence f.x = a by Th121
.= (a followed_by c).x by A3,Th118
.= g.x by A3,Th31;
end;
suppose
A4: n = 1;
hence f.x = b by Th122
.= g.x by A1,A4,Th30;
end;
suppose
A5: n > 1;
hence f.x = c by Th123
.= (a followed_by c).x by A5,Th119
.= g.x by A5,Th31;
end;
end;
definition
let X be non empty set;
let a,b,c be Element of X;
redefine func (a,b) followed_by c -> sequence of X; :: redefines followed_by (FUNCT_7, definition)
coherence
proof
(a,b) followed_by c = (a followed_by c) +* (1,b) by Th124;
hence thesis by Th114;
end;
end;
theorem Th125:
rng(a followed_by b) = {a,b}
proof
rng(NAT --> b) = {b} by FUNCOP_1:8;
then rng((NAT --> b)+*(0,a)) c= {b} \/ {a} by Th99;
hence rng(a followed_by b) c= {a,b} by ENUMSET1:1;
let x be object;
assume
A1: x in {a,b};
A2: dom(NAT --> b) = NAT;
1 in dom(NAT --> b);
then
A3: 1 in dom(a followed_by b) by Th29;
(a followed_by b).1 = b by Th119;
then
A4: b in rng(a followed_by b) by A3,FUNCT_1:3;
a in rng(a followed_by b) by A2,Th101;
hence thesis by A1,A4,TARSKI:def 2;
end;
theorem
rng (a,b) followed_by c = {a,b,c}
proof
A1: (a,b) followed_by c = (a followed_by c) +* (1,b) by Th124;
then
A2: dom (a,b) followed_by c = dom(a followed_by c) by Th29
.= dom(NAT --> c) by Th29
.= NAT;
((a,b) followed_by c).2 = c by Th123;
then
A3: c in rng (a,b) followed_by c by A2,FUNCT_1:3;
((a,b) followed_by c).1 = b by Th122;
then
A4: b in rng (a,b) followed_by c by A2,FUNCT_1:3;
rng(a followed_by c) = {a,c} by Th125;
then rng((a followed_by c)+*(1,b)) c= {a,c} \/ {b} by Th99;
then rng((a followed_by c)+*(1,b)) c= {a,c,b} by ENUMSET1:3;
hence rng (a,b) followed_by c c= {a,b,c} by A1,ENUMSET1:57;
let x be object;
((a,b) followed_by c).0 = a by Th121;
then
A5: a in rng (a,b) followed_by c by A2,FUNCT_1:3;
assume x in {a,b,c};
hence thesis by A5,A4,A3,ENUMSET1:def 1;
end;
:: from POLYNOM1, 2008.12.15, A.T.
definition
let A, B be set, f be Function of A, B, x be set, y be Element of B;
redefine func f+*(x,y) -> Function of A, B; :: redefines +* (FUNCT_7, definition)
coherence
proof
set F = f+*(x,y);
A1: rng F c= rng f \/ {y} by Th99;
per cases;
suppose
B is empty;
then dom f is empty;
hence thesis by Def2;
end;
suppose
A2: B is non empty;
then {y} c= B by ZFMISC_1:31;
then rng f \/ {y} c= B by XBOOLE_1:8;
then
A3: rng F c= B by A1;
dom f = A by A2,FUNCT_2:def 1;
then dom F = A by Th29;
hence thesis by A2,A3,FUNCT_2:def 1,RELSET_1:4;
end;
end;
end;
:: missing, 2008.12.14, A.T.
theorem
for A, B being non empty set, f being Function of A, B, x being
Element of A, y being set holds f+*(x,y).x = y
proof
let A, B be non empty set, f be Function of A, B, x be Element of A, y be
set;
x in A;
then x in dom f by FUNCT_2:def 1;
hence thesis by Th30;
end;
theorem
for A, B being non empty set, f,g being Function of A, B, x being
Element of A st for y being Element of A st f.y <> g.y holds y = x holds f = g
+*(x,f.x)
proof
let A, B be non empty set, f,g be Function of A, B, x be Element of A such
that
A1: for y being Element of A st f.y <> g.y holds y = x;
x in A;
then
A2: x in dom g by FUNCT_2:def 1;
A3: dom f = A by FUNCT_2:def 1
.= A \/ {x} by XBOOLE_1:12
.= dom g \/ {x} by FUNCT_2:def 1
.= dom g \/ dom(x.-->f.x);
for e being object st e in dom g \/ dom (x.-->f.x) holds (e in dom(x.-->f.x
) implies f.e = (x.-->f.x).e) & (not e in dom(x.-->f.x) implies f.e = g.e)
proof
let e be object;
assume
A4: e in dom g \/ dom (x.-->f.x);
thus e in dom(x.-->f.x) implies f.e = (x.-->f.x).e
proof
assume e in dom(x.-->f.x);
then e in {x};
then e = x by TARSKI:def 1;
hence thesis by FUNCOP_1:72;
end;
assume not e in dom(x.-->f.x);
then not e in {x};
then e <> x by TARSKI:def 1;
hence thesis by A1,A4;
end;
hence f = g+*(x.-->f.x) by A3,FUNCT_4:def 1
.= g+*(x,f.x) by A2,Def2;
end;
theorem Th129:
for g being A-defined Function holds f,f+*g equal_outside A
proof
let g be A-defined Function;
dom g c= A;
hence thesis by Th28;
end;
theorem
for f,g being A-defined Function holds f,g equal_outside A
proof
let f,g be A-defined Function;
A1: dom g \ A = {} by XBOOLE_1:37;
dom f \ A = {} by XBOOLE_1:37;
hence f|(dom f \ A) = {}
.= g|(dom g \ A) by A1;
end;
theorem
for f,g being A-defined Function, h being Function
holds h+*f, h+*g equal_outside A
proof
let f,g be A-defined Function, h be Function;
h, h+*f equal_outside A by Th129;
then
A1: h+*f,h equal_outside A;
h, h+*g equal_outside A by Th129;
hence thesis by A1;
end;
theorem
for I being NAT-defined Function holds card Shift(I,m) = card I
proof
defpred NC[set] means not contradiction;
deffunc U(Nat) = $1;
let I be NAT-defined Function;
A1: for x being set st x in dom I ex d being Element of NAT st x = U(d);
defpred X[Nat] means $1 in dom I;
deffunc V(Nat) = $1+m;
set B = { l where l is Element of NAT: U(l) in dom I },
C = { V(l) where l is Nat: l in { n: X[n] } & NC[l] },
D = { V(l) where l is Element of NAT: l in B },
E = { l+m where l is Nat: l in dom I };
A2: for d1,d2 being Element of NAT st U(d1) = U(d2) holds d1=d2;
A3: dom I,B are_equipotent from CardMono(A1,A2);
A4: C c= E
proof
let e be object;
assume e in C;
then consider l being Nat such that
A5: e =V(l) and
A6: l in { n: X[n] } & NC[l];
ex n st n=l & X[n] by A6;
hence thesis by A5;
end;
set B = { l where l is Element of NAT: X[l] };
B is Subset of NAT from DOMAIN_1:sch 7;
then
A7: B c= NAT;
set B = { l where l is Element of NAT: l in dom I };
A8: for d1,d2 be Element of NAT st V(d1) = V(d2) holds d1 = d2;
A9: B,D are_equipotent from CardMono9(A7,A8);
A10: E c= D
proof
let e be object;
assume e in E;
then consider l being Nat such that
A11: e = l+m and
A12: l in dom I;
reconsider l as Element of NAT by ORDINAL1:def 12;
l in B by A12;
hence thesis by A11;
end;
A13: dom Shift(I,m) = E by VALUED_1:def 12;
A14: D c= C
proof
let e be object;
assume e in D;
then consider l1 being Element of NAT such that
A15: e = V(l1) and
A16: l1 in B;
ex l being Element of NAT st l1 = l & U(l) in dom I by A16;
then l1 in dom I;
then l1 in { n: X[n] };
hence thesis by A15;
end;
then E c= C by A10;
then
A17: C = E by A4;
then C = D by A10,A14;
then
A18: dom Shift(I,m),dom I are_equipotent by A3,A17,A9,A13,WELLORD2:15;
thus card Shift(I,m) = card dom Shift(I,m) by CARD_1:62
.= card dom I by A18,CARD_1:5
.= card I by CARD_1:62;
end;
theorem Th133:
dom f = dom g & dom f c= A \/ B & f|B = g|B
implies f,g equal_outside A
by RELAT_1:153,XBOOLE_1:43;
theorem Th134:
dom f = dom g & B c= dom f & A misses B & f,g equal_outside A
implies f|B = g|B
by RELAT_1:153,XBOOLE_1:86;
reserve A,B,I for set, X,Y for ManySortedSet of I;
theorem
I c= A \/ B & X|B = Y|B implies X,Y equal_outside A
proof
dom X = I & dom Y = I by PARTFUN1:def 2;
hence thesis by Th133;
end;
theorem
B c= I & A misses B & X,Y equal_outside A implies X|B = Y|B
proof
dom X = I & dom Y = I by PARTFUN1:def 2;
hence thesis by Th134;
end;
registration let V be non empty set;
let f be V-valued Function, x be object, y be Element of V;
cluster f+*(x,y) -> V-valued;
coherence
proof
A1: rng(f+*(x,y)) c= rng f \/ {y} by Th99;
thus rng(f+*(x,y)) c= V by A1,XBOOLE_1:1;
end;
end;
theorem
f c= g & not x in dom f implies f c= g+*(x,y)
proof assume that
A1: f c= g;
assume not x in dom f;
then
A2: f c= f +*(x .--> y) by FUNCT_4:107;
per cases;
suppose x in dom g;
then g+*(x,y) = g+*(x.-->y) by Def2;
then f +*(x .--> y) c= g+*(x,y) by A1,FUNCT_4:123;
hence f c= g+*(x,y) by A2;
end;
suppose not x in dom g;
hence f c= g+*(x,y) by A1,Def2;
end;
end;
theorem
for I being non empty set, X being ManySortedSet of I,
l1,l2 being Element of I, i1,i2 being set
holds X +*((l1,l2) --> (i1, i2)) = X +* (l1,i1) +* (l2,i2)
proof
let I be non empty set, X be ManySortedSet of I,
l1,l2 be Element of I, i1,i2 be set;
A1: dom X = I by PARTFUN1:def 2;
then
A2: l1 in dom X;
dom(X +* (l1,i1)) = I by A1,Th29;
then
A3: l2 in dom(X +* (l1,i1));
thus X +*((l1,l2) --> (i1, i2)) =X +* ((l1 .--> i1) +* (l2 .--> i2))
.=X +* (l1 .--> i1) +* (l2 .--> i2) by FUNCT_4:14
.=X +* (l1,i1) +* (l2 .--> i2) by A2,Def2
.=X +* (l1,i1) +* (l2,i2) by A3,Def2;
end;
scheme Unionx { A()-> non empty set, a,b()-> Element of A(),
f() -> A()-valued Function,
x() -> object, F(object) -> object }:
{ F(i) where i is Element of A() : i in rng f()} =
{ F(j) where j is Element of A() : j in rng(f()+*(x(),a()))}
provided
A1: F(b()) = F(a()) and
A2: b() = f().x()
proof
set X = { F(i) where i is Element of A() : i in rng f()},
Y = { F(j) where j is Element of A() : j in rng(f()+*(x(),a()))};
thus X c= Y
proof
let e be object;
assume e in X;
then consider j being Element of A() such that
A3: e = F(j) and
A4: j in rng f();
consider y being object such that
A5: y in dom f() and
A6: f().y = j by A4,FUNCT_1:def 3;
y in dom(f()+*(x(),a())) by A5,Th29;
then
A7: (f()+*(x(),a())).y in rng(f()+*(x(),a())) by FUNCT_1:3;
now per cases;
suppose y = x();
hence e = F((f()+*(x(),a())).y) by A1,A2,A3,A6,Th30,A5;
end;
suppose y <> x();
hence e = F((f()+*(x(),a())).y) by A3,Th31,A6;
end;
end;
hence e in Y by A7;
end;
let e be object;
assume e in Y;
then consider j being Element of A() such that
A8: e = F(j) and
A9: j in rng(f()+*(x(),a()));
consider y being object such that
A10: y in dom(f()+*(x(),a())) and
A11: (f()+*(x(),a())).y = j by A9,FUNCT_1:def 3;
A12: y in dom f() by A10,Th29;
then
A13: f().y in rng f() by FUNCT_1:3;
now per cases;
suppose y = x();
hence e = F(f().y) by A1,A2,A8,A11,Th30,A12;
end;
suppose y <> x();
hence e = F(f().y) by A8,Th31,A11;
end;
end;
hence e in X by A13;
end;