:: Properties of Number-Valued Functions
:: by Library Committee
::
:: Received December 18, 2007
:: Copyright (c) 2007-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, FINSEQ_1, FUNCT_1, RELAT_1, XBOOLE_0, ORDINAL1,
XXREAL_0, VALUED_0, RAT_1, COMPLEX1, ARYTM_1, ARYTM_3, MEMBERED,
PARTFUN1, TARSKI, SUBSET_1, CARD_1, XCMPLX_0, INT_1, SQUARE_1, FUNCT_4,
FINSET_1, NAT_1, ORDINAL2, VALUED_1, AMISTD_1, FUNCOP_1, AMISTD_2,
AMISTD_3, ORDINAL4, REAL_1, NUMBER09;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, FINSET_1, CARD_1, XCMPLX_0,
NUMBERS, COMPLEX1, XXREAL_0, XXREAL_2, FUNCOP_1, XREAL_0, RAT_1, INT_1,
INT_2, SQUARE_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_4,
FINSEQ_1, MEMBERED, NAT_1, VALUED_0;
constructors PARTFUN1, RAT_1, VALUED_0, SQUARE_1, MEMBERED, INT_2, FINSEQ_1,
NAT_1, FUNCT_4, NAT_D, RELSET_1, XXREAL_2, FUNCOP_1, DOMAIN_1, WELLORD2,
FINSEQ_3, REAL_1;
registrations ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED,
VALUED_0, RAT_1, INT_1, NAT_1, FUNCT_1, FINSET_1, XXREAL_0, RELAT_1,
XXREAL_2, FUNCOP_1, FUNCT_4, CARD_1, FINSEQ_1;
requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, VALUED_0,
WELLORD2;
equalities XBOOLE_0, XCMPLX_0, SQUARE_1, FINSEQ_1, FUNCOP_1;
expansions TARSKI, XBOOLE_0, FUNCT_1, FINSEQ_1, VALUED_0, WELLORD2;
theorems FUNCT_1, FUNCT_2, RELSET_1, PARTFUN1, VALUED_0, COMPLEX1, FINSEQ_1,
XBOOLE_0, TARSKI, GRFUNC_1, RELAT_1, FUNCT_4, FINSET_1, NAT_1, INT_1,
ORDINAL1, XXREAL_0, ZFMISC_1, XXREAL_2, XBOOLE_1, CARD_1,
CARD_2, RAT_1, XTUPLE_0, XREAL_1, FINSEQ_3;
schemes FUNCT_1, CLASSES1, FRAENKEL, RECDEF_1, NAT_1;
begin :: f1 + f2
Lm1: for f being FinSequence, h being Function st dom h = dom f holds
h is FinSequence
proof
let f be FinSequence, h be Function such that
A1: dom h = dom f;
h is FinSequence-like
proof
take len f;
thus thesis by A1,FINSEQ_1:def 3;
end;
hence thesis;
end;
Lm2: for f, g being FinSequence, h being Function st dom h = dom f /\ dom g
holds h is FinSequence
proof
let f, g be FinSequence, h be Function such that
A1: dom h = dom f /\ dom g;
consider n being Nat such that
A2: dom f = Seg n by FINSEQ_1:def 2;
consider m being Nat such that
A3: dom g = Seg m by FINSEQ_1:def 2;
h is FinSequence-like
proof
per cases;
suppose
A4: n <= m;
take n;
thus thesis by A1,A2,A3,A4,FINSEQ_1:7;
end;
suppose
A5: m <= n;
take m;
thus thesis by A1,A2,A3,A5,FINSEQ_1:7;
end;
end;
hence thesis;
end;
registration
cluster complex-valued for FinSequence;
existence
proof
take <*>COMPLEX;
thus thesis;
end;
end;
:: move somewhere
registration
let r be Rational;
cluster |. r .| -> rational;
coherence
proof
|. r .| = -r or |. r .| = r by COMPLEX1:71;
hence thesis;
end;
end;
definition
let f1,f2 be complex-valued Function;
deffunc F(object) = f1.$1 + f2.$1;
set X = dom f1 /\ dom f2;
func f1 + f2 -> Function means
:Def1:
dom it = dom f1 /\ dom f2 &
for c being object st c in dom it holds it.c = f1.c + f2.c;
existence
proof
ex f being Function st dom f = X & for x being object st x in X holds f.x
= F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let f, g be Function such that
A1: dom f = X and
A2: for c being object st c in dom f holds f.c = F(c) and
A3: dom g = X and
A4: for c being object st c in dom g holds g.c = F(c);
now
let x be object;
assume
A5: x in dom f;
hence f.x = F(x) by A2
.= g.x by A1,A3,A4,A5;
end;
hence thesis by A1,A3;
end;
commutativity;
end;
registration
let f1,f2 be complex-valued Function;
cluster f1+f2 -> complex-valued;
coherence
proof
let x be object;
assume x in dom (f1+f2);
then (f1+f2).x = f1.x + f2.x by Def1;
hence thesis;
end;
end;
registration
let f1,f2 be real-valued Function;
cluster f1+f2 -> real-valued;
coherence
proof
let x be object;
assume x in dom (f1+f2);
then (f1+f2).x = f1.x + f2.x by Def1;
hence thesis;
end;
end;
registration
let f1,f2 be rational-valued Function;
cluster f1+f2 -> RAT-valued;
coherence
proof
let y be object;
assume y in rng(f1+f2);
then consider x being object such that
A1: x in dom (f1+f2) and
A2: (f1+f2).x = y by FUNCT_1:def 3;
(f1+f2).x = f1.x + f2.x by A1,Def1;
hence thesis by A2,RAT_1:def 2;
end;
end;
registration
let f1,f2 be integer-valued Function;
cluster f1+f2 -> INT-valued;
coherence
proof
let y be object;
assume y in rng(f1+f2);
then consider x being object such that
A1: x in dom (f1+f2) and
A2: (f1+f2).x = y by FUNCT_1:def 3;
(f1+f2).x = f1.x + f2.x by A1,Def1;
hence thesis by A2,INT_1:def 2;
end;
end;
registration
let f1,f2 be natural-valued Function;
cluster f1+f2 -> natural-valued;
coherence
proof
let x be object;
assume x in dom (f1+f2);
then (f1+f2).x = f1.x + f2.x by Def1;
hence thesis;
end;
end;
definition
let C be set;
let D1,D2 be complex-membered set;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
redefine func f1+f2 -> PartFunc of C,COMPLEX; :: redefines + (VALUED_1, definition)
coherence
proof
dom (f1+f2) = dom f1 /\ dom f2 & rng (f1+f2) c= COMPLEX by Def1;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D1,D2 be real-membered set;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
redefine func f1+f2 -> PartFunc of C,REAL; :: redefines + (VALUED_1, definition)
coherence
proof
dom (f1+f2) = dom f1 /\ dom f2 & rng (f1+f2) c= REAL by Def1,VALUED_0:def 3
;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D1,D2 be rational-membered set;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
redefine func f1+f2 -> PartFunc of C,RAT; :: redefines + (VALUED_1, definition)
coherence
proof
dom (f1+f2) = dom f1 /\ dom f2 & rng (f1+f2) c= RAT by Def1,RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D1,D2 be integer-membered set;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
redefine func f1+f2 -> PartFunc of C,INT; :: redefines + (VALUED_1, definition)
coherence
proof
dom (f1+f2) = dom f1 /\ dom f2 & rng (f1+f2) c= INT by Def1,RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D1,D2 be natural-membered set;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
redefine func f1+f2 -> PartFunc of C,NAT; :: redefines + (VALUED_1, definition)
coherence
proof
dom (f1+f2) = dom f1 /\ dom f2 & rng (f1+f2) c= NAT by Def1,VALUED_0:def 6;
hence thesis by RELSET_1:4;
end;
end;
registration
let C be set;
let D1,D2 be complex-membered non empty set;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1+f2 -> total for PartFunc of C,COMPLEX;
coherence
proof
dom f1 = C & dom f2 = C by FUNCT_2:def 1;
then dom(f1+f2) = C /\ C by Def1
.= C;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D1,D2 be real-membered non empty set;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1+f2 -> total for PartFunc of C,REAL;
coherence
proof
dom f1 = C & dom f2 = C by FUNCT_2:def 1;
then dom(f1+f2) = C /\ C by Def1
.= C;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D1,D2 be rational-membered non empty set;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1+f2 -> total for PartFunc of C,RAT;
coherence
proof
dom f1 = C & dom f2 = C by FUNCT_2:def 1;
then dom(f1+f2) = C /\ C by Def1
.= C;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D1,D2 be integer-membered non empty set;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1+f2 -> total for PartFunc of C,INT;
coherence
proof
dom f1 = C & dom f2 = C by FUNCT_2:def 1;
then dom(f1+f2) = C /\ C by Def1
.= C;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D1,D2 be natural-membered non empty set;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1+f2 -> total for PartFunc of C,NAT;
coherence
proof
dom f1 = C & dom f2 = C by FUNCT_2:def 1;
then dom(f1+f2) = C /\ C by Def1
.= C;
hence thesis by PARTFUN1:def 2;
end;
end;
theorem
for C being set, D1,D2 being complex-membered non empty set for f1
being Function of C,D1, f2 being Function of C,D2 for c being Element of C
holds (f1+f2).c = f1.c + f2.c
proof
let C be set;
let D1,D2 be complex-membered non empty set;
let f1 be Function of C,D1, f2 be Function of C,D2;
A1: dom(f1+f2) = C by FUNCT_2:def 1;
let c be Element of C;
per cases;
suppose
C is non empty;
hence thesis by A1,Def1;
end;
suppose
A2: C is empty;
then f1.c = 0;
hence thesis by A2;
end;
end;
registration
let f1, f2 be complex-valued FinSequence;
cluster f1+f2 -> FinSequence-like;
coherence
proof
dom(f1+f2) = dom f1 /\ dom f2 by Def1;
hence thesis by Lm2;
end;
end;
begin :: r + f
definition
let f be complex-valued Function, r be Complex;
deffunc F(object) = r + f.$1;
func r + f -> Function means
:Def2:
dom it = dom f &
for c being object st c in dom it holds it.c = r + f.c;
existence
proof
ex g being Function st dom g = dom f & for x being object st x in dom f
holds g.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let h, g be Function such that
A1: dom h = dom f and
A2: for c being object st c in dom h holds h.c = F(c) and
A3: dom g = dom f and
A4: for c being object st c in dom g holds g.c = F(c);
now
let x be object;
assume
A5: x in dom h;
hence h.x = F(x) by A2
.= g.x by A1,A3,A4,A5;
end;
hence thesis by A1,A3;
end;
end;
notation
let f be complex-valued Function, r be Complex;
synonym f + r for r + f;
end;
registration
let f be complex-valued Function, r be Complex;
cluster r+f -> complex-valued;
coherence
proof
let x be object;
assume x in dom (r+f);
then (r+f).x = r + f.x by Def2;
hence thesis;
end;
end;
registration
let f be real-valued Function, r be Real;
cluster r+f -> real-valued;
coherence
proof
let x be object;
assume x in dom (r+f);
then (r+f).x = r + f.x by Def2;
hence thesis;
end;
end;
registration
let f be rational-valued Function, r be Rational;
cluster r+f -> RAT-valued;
coherence
proof
let y be object;
assume y in rng (r+f);
then consider x being object such that
A1: x in dom (r+f) and
A2: (r+f).x = y by FUNCT_1:def 3;
(r+f).x = r + f.x by A1,Def2;
hence thesis by A2,RAT_1:def 2;
end;
end;
registration
let f be integer-valued Function, r be Integer;
cluster r+f -> INT-valued;
coherence
proof
let y be object;
assume y in rng (r+f);
then consider x being object such that
A1: x in dom (r+f) and
A2: (r+f).x = y by FUNCT_1:def 3;
(r+f).x = r + f.x by A1,Def2;
hence thesis by A2,INT_1:def 2;
end;
end;
registration
let f be natural-valued Function, r be Nat;
cluster r+f -> natural-valued;
coherence
proof
let x be object;
assume x in dom (r+f);
then (r+f).x = r + f.x by Def2;
hence thesis;
end;
end;
definition
let C be set;
let D be complex-membered set;
let f be PartFunc of C,D;
let r be Complex;
redefine func r+f -> PartFunc of C,COMPLEX; :: redefines + (VALUED_1, definition)
coherence
proof
dom (r+f) = dom f & rng (r+f) c= COMPLEX by Def2;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be real-membered set;
let f be PartFunc of C,D;
let r be Real;
redefine func r+f -> PartFunc of C,REAL; :: redefines + (VALUED_1, definition)
coherence
proof
dom (r+f) = dom f & rng (r+f) c= REAL by Def2,VALUED_0:def 3;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be rational-membered set;
let f be PartFunc of C,D;
let r be Rational;
redefine func r+f -> PartFunc of C,RAT; :: redefines + (VALUED_1, definition)
coherence
proof
dom (r+f) = dom f & rng (r+f) c= RAT by Def2,RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be integer-membered set;
let f be PartFunc of C,D;
let r be Integer;
redefine func r+f -> PartFunc of C,INT; :: redefines + (VALUED_1, definition)
coherence
proof
dom (r+f) = dom f & rng (r+f) c= INT by Def2,RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be natural-membered set;
let f be PartFunc of C,D;
let r be Nat;
redefine func r+f -> PartFunc of C,NAT; :: redefines + (VALUED_1, definition)
coherence
proof
dom (r+f) = dom f & rng (r+f) c= NAT by Def2,VALUED_0:def 6;
hence thesis by RELSET_1:4;
end;
end;
registration
let C be set;
let D be complex-membered non empty set;
let f be Function of C,D;
let r be Complex;
cluster r+f -> total for PartFunc of C,COMPLEX;
coherence
proof
dom(r+f) = dom f by Def2
.= C by FUNCT_2:def 1;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D be real-membered non empty set;
let f be Function of C,D;
let r be Real;
cluster r+f -> total for PartFunc of C,REAL;
coherence
proof
dom(r+f) = dom f by Def2
.= C by FUNCT_2:def 1;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D be rational-membered non empty set;
let f be Function of C,D;
let r be Rational;
cluster r+f -> total for PartFunc of C,RAT;
coherence
proof
dom(r+f) = dom f by Def2
.= C by FUNCT_2:def 1;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D be integer-membered non empty set;
let f be Function of C,D;
let r be Integer;
cluster r+f -> total for PartFunc of C,INT;
coherence
proof
dom(r+f) = dom f by Def2
.= C by FUNCT_2:def 1;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D be natural-membered non empty set;
let f be Function of C,D;
let r be Nat;
cluster r+f -> total for PartFunc of C,NAT;
coherence
proof
dom(r+f) = dom f by Def2
.= C by FUNCT_2:def 1;
hence thesis by PARTFUN1:def 2;
end;
end;
theorem
for C being non empty set, D being complex-membered non empty set
for f being Function of C,D, r being Complex
for c being Element of C holds
(r+f).c = r + f.c
proof
let C be non empty set;
let D be complex-membered non empty set;
let f be Function of C,D, r be Complex;
dom(r+f) = C by FUNCT_2:def 1;
hence thesis by Def2;
end;
registration
let f be complex-valued FinSequence, r be Complex;
cluster r+f -> FinSequence-like;
coherence
proof
dom (r+f) = dom f by Def2;
hence thesis by Lm1;
end;
end;
begin :: f - r
definition
let f be complex-valued Function, r be Complex;
func f - r -> Function equals
-r + f;
coherence;
end;
theorem
for f being complex-valued Function, r being Complex holds dom
(f-r) = dom f & for c being object st c in dom f holds (f-r).c = f.c - r
proof
let f be complex-valued Function, r be Complex;
dom (f-r) = dom f by Def2;
hence thesis by Def2;
end;
registration
let f be complex-valued Function, r be Complex;
cluster f-r -> complex-valued;
coherence;
end;
registration
let f be real-valued Function, r be Real;
cluster f-r -> real-valued;
coherence;
end;
registration
let f be rational-valued Function, r be Rational;
cluster f-r -> RAT-valued;
coherence;
end;
registration
let f be integer-valued Function, r be Integer;
cluster f-r -> INT-valued;
coherence;
end;
definition
let C be set;
let D be complex-membered set;
let f be PartFunc of C,D;
let r be Complex;
redefine func f-r -> PartFunc of C,COMPLEX; :: redefines - (VALUED_1, definition)
coherence
proof
dom (f-r) = dom f & rng (f-r) c= COMPLEX by Def2;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be real-membered set;
let f be PartFunc of C,D;
let r be Real;
redefine func f-r -> PartFunc of C,REAL; :: redefines - (VALUED_1, definition)
coherence
proof
dom (f-r) = dom f & rng (f-r) c= REAL by Def2,VALUED_0:def 3;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be rational-membered set;
let f be PartFunc of C,D;
let r be Rational;
redefine func f-r -> PartFunc of C,RAT; :: redefines - (VALUED_1, definition)
coherence
proof
dom (f-r) = dom f & rng (f-r) c= RAT by Def2,RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be integer-membered set;
let f be PartFunc of C,D;
let r be Integer;
redefine func f-r -> PartFunc of C,INT; :: redefines - (VALUED_1, definition)
coherence
proof
dom (f-r) = dom f & rng (f-r) c= INT by Def2,RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
end;
registration
let C be set;
let D be complex-membered non empty set;
let f be Function of C,D;
let r be Complex;
cluster f-r -> total for PartFunc of C,COMPLEX;
coherence;
end;
registration
let C be set;
let D be real-membered non empty set;
let f be Function of C,D;
let r be Real;
cluster f-r -> total for PartFunc of C,REAL;
coherence;
end;
registration
let C be set;
let D be rational-membered non empty set;
let f be Function of C,D;
let r be Rational;
cluster f-r -> total for PartFunc of C,RAT;
coherence;
end;
registration
let C be set;
let D be integer-membered non empty set;
let f be Function of C,D;
let r be Integer;
cluster f-r -> total for PartFunc of C,INT;
coherence;
end;
theorem
for C being non empty set, D being complex-membered non empty set for
f being Function of C,D, r being Complex for c being Element of C holds
(f-r).c = f.c - r
proof
let C be non empty set;
let D be complex-membered non empty set;
let f be Function of C,D, r be Complex;
dom (f-r) = C by FUNCT_2:def 1;
hence thesis by Def2;
end;
registration
let f be complex-valued FinSequence, r be Complex;
cluster f-r -> FinSequence-like;
coherence;
end;
begin :: f1 (#) f2
definition
let f1,f2 be complex-valued Function;
deffunc F(object) = f1.$1 * f2.$1;
set X = dom f1 /\ dom f2;
func f1 (#) f2 -> Function means
:Def4:
dom it = dom f1 /\ dom f2 & for c
being object st c in dom it holds it.c = f1.c * f2.c;
existence
proof
ex f being Function st dom f = X & for x being object st x in X holds f.x
= F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let f, g be Function such that
A1: dom f = X and
A2: for c being object st c in dom f holds f.c = F(c) and
A3: dom g = X and
A4: for c being object st c in dom g holds g.c = F(c);
now
let x be object;
assume
A5: x in dom f;
hence f.x = F(x) by A2
.= g.x by A1,A3,A4,A5;
end;
hence thesis by A1,A3;
end;
commutativity;
end;
theorem
for f1,f2 being complex-valued Function
for c being object holds (f1(#)f2).c = f1.c * f2.c
proof
let f1,f2 be complex-valued Function;
let c be object;
A1: dom (f1(#)f2) = dom f1 /\ dom f2 by Def4;
per cases;
suppose
c in dom (f1(#)f2);
hence thesis by Def4;
end;
suppose
A2: not c in dom (f1(#)f2);
then not c in dom f1 or not c in dom f2 by A1,XBOOLE_0:def 4;
then f1.c = 0 or f2.c = 0 by FUNCT_1:def 2;
hence thesis by A2,FUNCT_1:def 2;
end;
end;
registration
let f1,f2 be complex-valued Function;
cluster f1(#)f2 -> complex-valued;
coherence
proof
let x be object;
assume x in dom (f1(#)f2);
then (f1(#)f2).x = f1.x * f2.x by Def4;
hence thesis;
end;
end;
registration
let f1,f2 be real-valued Function;
cluster f1(#)f2 -> real-valued;
coherence
proof
let x be object;
assume x in dom (f1(#)f2);
then (f1(#)f2).x = f1.x * f2.x by Def4;
hence thesis;
end;
end;
registration
let f1,f2 be rational-valued Function;
cluster f1(#)f2 -> RAT-valued;
coherence
proof
let y be object;
assume y in rng (f1(#)f2);
then consider x being object such that
A1: x in dom (f1(#)f2) and
A2: (f1(#)f2).x = y by FUNCT_1:def 3;
(f1(#)f2).x = f1.x * f2.x by A1,Def4;
hence thesis by A2,RAT_1:def 2;
end;
end;
registration
let f1,f2 be integer-valued Function;
cluster f1(#)f2 -> INT-valued;
coherence
proof
let y be object;
assume y in rng (f1(#)f2);
then consider x being object such that
A1: x in dom (f1(#)f2) and
A2: (f1(#)f2).x = y by FUNCT_1:def 3;
(f1(#)f2).x = f1.x * f2.x by A1,Def4;
hence thesis by A2,INT_1:def 2;
end;
end;
registration
let f1,f2 be natural-valued Function;
cluster f1(#)f2 -> natural-valued;
coherence
proof
let x be object;
assume x in dom (f1(#)f2);
then (f1(#)f2).x = f1.x * f2.x by Def4;
hence thesis;
end;
end;
definition
let C be set;
let D1,D2 be complex-membered set;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
redefine func f1(#)f2 -> PartFunc of C,COMPLEX; :: redefines (#) (VALUED_1, definition)
coherence
proof
dom (f1(#)f2) = dom f1 /\ dom f2 & rng (f1(#)f2) c= COMPLEX by Def4;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D1,D2 be real-membered set;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
redefine func f1(#)f2 -> PartFunc of C,REAL; :: redefines (#) (VALUED_1, definition)
coherence
proof
dom (f1(#)f2) = dom f1 /\ dom f2 & rng (f1(#)f2) c= REAL by Def4,
VALUED_0:def 3;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D1,D2 be rational-membered set;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
redefine func f1(#)f2 -> PartFunc of C,RAT; :: redefines (#) (VALUED_1, definition)
coherence
proof
dom (f1(#)f2) = dom f1 /\ dom f2 & rng (f1(#)f2) c= RAT by Def4,
RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D1,D2 be integer-membered set;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
redefine func f1(#)f2 -> PartFunc of C,INT; :: redefines (#) (VALUED_1, definition)
coherence
proof
dom (f1(#)f2) = dom f1 /\ dom f2 & rng (f1(#)f2) c= INT by Def4,
RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D1,D2 be natural-membered set;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
redefine func f1(#)f2 -> PartFunc of C,NAT; :: redefines (#) (VALUED_1, definition)
coherence
proof
dom (f1(#)f2) = dom f1 /\ dom f2 & rng (f1(#)f2) c= NAT by Def4,
VALUED_0:def 6;
hence thesis by RELSET_1:4;
end;
end;
registration
let C be set;
let D1,D2 be complex-membered non empty set;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1(#)f2 -> total for PartFunc of C,COMPLEX;
coherence
proof
dom f1 = C & dom f2 = C by FUNCT_2:def 1;
then dom(f1(#)f2) = C /\ C by Def4
.= C;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D1,D2 be real-membered non empty set;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1(#)f2 -> total for PartFunc of C,REAL;
coherence
proof
dom f1 = C & dom f2 = C by FUNCT_2:def 1;
then dom(f1(#)f2) = C /\ C by Def4
.= C;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D1,D2 be rational-membered non empty set;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1(#)f2 -> total for PartFunc of C,RAT;
coherence
proof
dom f1 = C & dom f2 = C by FUNCT_2:def 1;
then dom(f1(#)f2) = C /\ C by Def4
.= C;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D1,D2 be integer-membered non empty set;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1(#)f2 -> total for PartFunc of C,INT;
coherence
proof
dom f1 = C & dom f2 = C by FUNCT_2:def 1;
then dom(f1(#)f2) = C /\ C by Def4
.= C;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D1,D2 be natural-membered non empty set;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1(#)f2 -> total for PartFunc of C,NAT;
coherence
proof
dom f1 = C & dom f2 = C by FUNCT_2:def 1;
then dom(f1(#)f2) = C /\ C by Def4
.= C;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let f1, f2 be complex-valued FinSequence;
cluster f1(#)f2 -> FinSequence-like;
coherence
proof
dom(f1(#)f2) = dom f1 /\ dom f2 by Def4;
hence thesis by Lm2;
end;
end;
begin :: r (#) f
definition
let f be complex-valued Function, r be Complex;
deffunc F(object) = r * f.$1;
func r (#) f -> Function means
:Def5:
dom it = dom f & for c being object st c
in dom it holds it.c = r * f.c;
existence
proof
ex g being Function st dom g = dom f & for x being object st x in dom f
holds g.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let h, g be Function such that
A1: dom h = dom f and
A2: for c being object st c in dom h holds h.c = F(c) and
A3: dom g = dom f and
A4: for c being object st c in dom g holds g.c = F(c);
now
let x be object;
assume
A5: x in dom h;
hence h.x = F(x) by A2
.= g.x by A1,A3,A4,A5;
end;
hence thesis by A1,A3;
end;
end;
notation
let f be complex-valued Function, r be Complex;
synonym f (#) r for r (#) f;
end;
theorem Th6:
for f being complex-valued Function, r being Complex for c
being object holds (r(#)f).c = r * f.c
proof
let f be complex-valued Function, r be Complex;
let c be object;
A1: dom f = dom (r(#)f) by Def5;
per cases;
suppose
c in dom f;
hence thesis by A1,Def5;
end;
suppose
A2: not c in dom f;
hence (r(#)f).c = r*0 by A1,FUNCT_1:def 2
.= r * f.c by A2,FUNCT_1:def 2;
end;
end;
registration
let f be complex-valued Function, r be Complex;
cluster r(#)f -> complex-valued;
coherence
proof
let x be object;
assume x in dom (r(#)f);
then (r(#)f).x = r * f.x by Def5;
hence thesis;
end;
end;
registration
let f be real-valued Function, r be Real;
cluster r(#)f -> real-valued;
coherence
proof
let x be object;
assume x in dom (r(#)f);
then (r(#)f).x = r * f.x by Def5;
hence thesis;
end;
end;
registration
let f be rational-valued Function, r be Rational;
cluster r(#)f -> RAT-valued;
coherence
proof
let y be object;
assume y in rng (r(#)f);
then consider x being object such that
A1: x in dom (r(#)f) and
A2: (r(#)f).x = y by FUNCT_1:def 3;
(r(#)f).x = r * f.x by A1,Def5;
hence thesis by A2,RAT_1:def 2;
end;
end;
registration
let f be integer-valued Function, r be Integer;
cluster r(#)f -> INT-valued;
coherence
proof
let y be object;
assume y in rng (r(#)f);
then consider x being object such that
A1: x in dom (r(#)f) and
A2: (r(#)f).x = y by FUNCT_1:def 3;
(r(#)f).x = r * f.x by A1,Def5;
hence thesis by A2,INT_1:def 2;
end;
end;
registration
let f be natural-valued Function, r be Nat;
cluster r(#)f -> natural-valued;
coherence
proof
let x be object;
assume x in dom (r(#)f);
then (r(#)f).x = r * f.x by Def5;
hence thesis;
end;
end;
definition
let C be set;
let D be complex-membered set;
let f be PartFunc of C,D;
let r be Complex;
redefine func r(#)f -> PartFunc of C,COMPLEX; :: redefines (#) (VALUED_1, definition)
coherence
proof
dom (r(#)f) = dom f & rng (r(#)f) c= COMPLEX by Def5;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be real-membered set;
let f be PartFunc of C,D;
let r be Real;
redefine func r(#)f -> PartFunc of C,REAL; :: redefines (#) (VALUED_1, definition)
coherence
proof
dom (r(#)f) = dom f & rng (r(#)f) c= REAL by Def5,VALUED_0:def 3;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be rational-membered set;
let f be PartFunc of C,D;
let r be Rational;
redefine func r(#)f -> PartFunc of C,RAT; :: redefines (#) (VALUED_1, definition)
coherence
proof
dom (r(#)f) = dom f & rng (r(#)f) c= RAT by Def5,RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be integer-membered set;
let f be PartFunc of C,D;
let r be Integer;
redefine func r(#)f -> PartFunc of C,INT; :: redefines (#) (VALUED_1, definition)
coherence
proof
dom (r(#)f) = dom f & rng (r(#)f) c= INT by Def5,RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be natural-membered set;
let f be PartFunc of C,D;
let r be Nat;
redefine func r(#)f -> PartFunc of C,NAT; :: redefines (#) (VALUED_1, definition)
coherence
proof
dom (r(#)f) = dom f & rng (r(#)f) c= NAT by Def5,VALUED_0:def 6;
hence thesis by RELSET_1:4;
end;
end;
registration
let C be set;
let D be complex-membered non empty set;
let f be Function of C,D;
let r be Complex;
cluster r(#)f -> total for PartFunc of C,COMPLEX;
coherence
proof
dom(r(#)f) = dom f by Def5
.= C by FUNCT_2:def 1;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D be real-membered non empty set;
let f be Function of C,D;
let r be Real;
cluster r(#)f -> total for PartFunc of C,REAL;
coherence
proof
dom(r(#)f) = dom f by Def5
.= C by FUNCT_2:def 1;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D be rational-membered non empty set;
let f be Function of C,D;
let r be Rational;
cluster r(#)f -> total for PartFunc of C,RAT;
coherence
proof
dom(r(#)f) = dom f by Def5
.= C by FUNCT_2:def 1;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D be integer-membered non empty set;
let f be Function of C,D;
let r be Integer;
cluster r(#)f -> total for PartFunc of C,INT;
coherence
proof
dom(r(#)f) = dom f by Def5
.= C by FUNCT_2:def 1;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D be natural-membered non empty set;
let f be Function of C,D;
let r be Nat;
cluster r(#)f -> total for PartFunc of C,NAT;
coherence
proof
dom(r(#)f) = dom f by Def5
.= C by FUNCT_2:def 1;
hence thesis by PARTFUN1:def 2;
end;
end;
theorem
for C being non empty set, D being complex-membered non empty set for
f being Function of C,D, r being Complex for g being Function of C,
COMPLEX st for c being Element of C holds g.c = r * f.c holds g = r(#)f
proof
let C be non empty set, D be complex-membered non empty set;
let f be Function of C,D, r be Complex;
let g be Function of C,COMPLEX such that
A1: for c being Element of C holds g.c = r * f.c;
let x be Element of C;
thus g.x = r*f.x by A1
.= (r(#)f).x by Th6;
end;
registration
let f be complex-valued FinSequence, r be Complex;
cluster r(#)f -> FinSequence-like;
coherence
proof
dom (r(#)f) = dom f by Def5;
hence thesis by Lm1;
end;
end;
begin :: -f
definition
let f be complex-valued Function;
func -f -> complex-valued Function equals
(-1) (#) f;
coherence;
involutiveness
proof
let r, h be complex-valued Function;
assume
A1: r = (-1)(#)h;
thus dom ((-1)(#)r) = dom r by Def5
.= dom h by A1,Def5;
let c be object;
assume c in dom h;
reconsider a = (-1)*(h.c) as Complex;
thus h.c = (-1) * a
.= (-1)*r.c by A1,Th6
.= ((-1)(#)r).c by Th6;
end;
end;
theorem Th8:
for f being complex-valued Function holds dom -f = dom f & for c
being object holds (-f).c = -(f.c)
proof
let f be complex-valued Function;
thus
A1: dom -f = dom f by Def5;
let c be object;
per cases;
suppose
c in dom f;
hence (-f).c = (-1)*f.c by A1,Def5
.= -(f.c);
end;
suppose
A2: not c in dom f;
hence (-f).c = -(0 qua Complex) by A1,FUNCT_1:def 2
.= -(f.c) by A2,FUNCT_1:def 2;
end;
end;
theorem
for f being complex-valued Function, g being Function st dom f = dom g
& for c being object st c in dom f holds g.c = -(f.c) holds g = -f
proof
let f be complex-valued Function, g be Function;
assume that
A1: dom f = dom g and
A2: for c being object st c in dom f holds g.c = -(f.c);
thus dom -f = dom g by A1,Def5;
let c be object;
assume
A3: c in dom g;
thus (-f).c = -f.c by Th8
.= g.c by A1,A2,A3;
end;
registration
let f be complex-valued Function;
cluster -f -> complex-valued;
coherence;
end;
registration
let f be real-valued Function;
cluster -f -> real-valued;
coherence;
end;
registration
let f be rational-valued Function;
cluster -f -> RAT-valued;
coherence;
end;
registration
let f be integer-valued Function;
cluster -f -> INT-valued;
coherence;
end;
definition
let C be set;
let D be complex-membered set;
let f be PartFunc of C,D;
redefine func -f -> PartFunc of C,COMPLEX; :: redefines - (VALUED_1, definition)
coherence
proof
dom -f = dom f & rng -f c= COMPLEX by Def5;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be real-membered set;
let f be PartFunc of C,D;
redefine func -f -> PartFunc of C,REAL; :: redefines - (VALUED_1, definition)
coherence
proof
dom -f = dom f & rng -f c= REAL by Def5,VALUED_0:def 3;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be rational-membered set;
let f be PartFunc of C,D;
redefine func -f -> PartFunc of C,RAT; :: redefines - (VALUED_1, definition)
coherence
proof
dom -f = dom f & rng -f c= RAT by Def5,RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be integer-membered set;
let f be PartFunc of C,D;
redefine func -f -> PartFunc of C,INT; :: redefines - (VALUED_1, definition)
coherence
proof
dom -f = dom f & rng -f c= INT by Def5,RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
end;
registration
let C be set;
let D be complex-membered non empty set;
let f be Function of C,D;
cluster -f -> total for PartFunc of C,COMPLEX;
coherence;
end;
registration
let C be set;
let D be real-membered non empty set;
let f be Function of C,D;
cluster -f -> total for PartFunc of C,REAL;
coherence;
end;
registration
let C be set;
let D be rational-membered non empty set;
let f be Function of C,D;
cluster -f -> total for PartFunc of C,RAT;
coherence;
end;
registration
let C be set;
let D be integer-membered non empty set;
let f be Function of C,D;
cluster -f -> total for PartFunc of C,INT;
coherence;
end;
registration
let f be complex-valued FinSequence;
cluster -f -> FinSequence-like;
coherence;
end;
begin :: f"
definition
let f be complex-valued Function;
deffunc F(object) = (f.$1)";
func f" -> complex-valued Function means
:Def7:
dom it = dom f & for c being
object st c in dom it holds it.c = (f.c)";
existence
proof
consider g being Function such that
A1: dom g = dom f & for x being object st x in dom f holds g.x = F(x)
from FUNCT_1:sch 3;
g is complex-valued
proof
let x be object;
assume x in dom g;
then g.x = (f.x)" by A1;
hence thesis;
end;
hence thesis by A1;
end;
uniqueness
proof
let h, g be complex-valued Function such that
A2: dom h = dom f and
A3: for c being object st c in dom h holds h.c = F(c) and
A4: dom g = dom f and
A5: for c being object st c in dom g holds g.c = F(c);
now
let x be object;
assume
A6: x in dom h;
hence h.x = F(x) by A3
.= g.x by A2,A4,A5,A6;
end;
hence thesis by A2,A4;
end;
involutiveness
proof
let r, h be complex-valued Function;
assume that
A7: dom r = dom h and
A8: for c being object st c in dom r holds r.c = (h.c)";
thus dom r = dom h by A7;
let c be object;
assume
A9: c in dom h;
thus h.c = (h.c)""
.= (r.c)" by A7,A8,A9;
end;
end;
::better name
theorem Th10:
for f being complex-valued Function for c being object holds
f".c = (f.c)"
proof
let f be complex-valued Function;
let c be object;
A1: dom (f") = dom f by Def7;
per cases;
suppose
c in dom f;
hence thesis by A1,Def7;
end;
suppose
A2: not c in dom f;
hence f".c = 0 qua Complex" by A1,FUNCT_1:def 2
.= (f.c)" by A2,FUNCT_1:def 2;
end;
end;
registration
let f be real-valued Function;
cluster f" -> real-valued;
coherence
proof
let x be object;
assume x in dom (f");
then f".x = (f.x)" by Def7;
hence thesis;
end;
end;
registration
let f be rational-valued Function;
cluster f" -> RAT-valued;
coherence
proof
let y be object;
assume y in rng (f");
then consider x being object such that
A1: x in dom (f") and
A2: (f").x = y by FUNCT_1:def 3;
f".x = (f.x)" by A1,Def7;
hence thesis by A2,RAT_1:def 2;
end;
end;
definition
let C be set;
let D be complex-membered set;
let f be PartFunc of C,D;
redefine func f" -> PartFunc of C,COMPLEX; :: redefines " (VALUED_1, definition)
coherence
proof
dom (f") = dom f & rng (f") c= COMPLEX by Def7;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be real-membered set;
let f be PartFunc of C,D;
redefine func f" -> PartFunc of C,REAL; :: redefines " (VALUED_1, definition)
coherence
proof
dom (f") = dom f & rng (f") c= REAL by Def7,VALUED_0:def 3;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be rational-membered set;
let f be PartFunc of C,D;
redefine func f" -> PartFunc of C,RAT; :: redefines " (VALUED_1, definition)
coherence
proof
dom (f") = dom f & rng (f") c= RAT by Def7,RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
end;
registration
let C be set;
let D be complex-membered non empty set;
let f be Function of C,D;
cluster f" -> total for PartFunc of C,COMPLEX;
coherence
proof
dom (f") = dom f by Def7
.= C by FUNCT_2:def 1;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D be real-membered non empty set;
let f be Function of C,D;
cluster f" -> total for PartFunc of C,REAL;
coherence
proof
dom (f") = dom f by Def7
.= C by FUNCT_2:def 1;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D be rational-membered non empty set;
let f be Function of C,D;
cluster f" -> total for PartFunc of C,RAT;
coherence
proof
dom (f") = dom f by Def7
.= C by FUNCT_2:def 1;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let f be complex-valued FinSequence;
cluster f" -> FinSequence-like;
coherence
proof
dom (f") = dom f by Def7;
hence thesis by Lm1;
end;
end;
begin :: f^2
definition
let f be complex-valued Function;
func f^2 -> Function equals
f (#) f;
coherence;
end;
theorem Th11:
for f being complex-valued Function holds dom (f^2) = dom f &
for c being object holds f^2.c = (f.c)^2
proof
let f be complex-valued Function;
thus
A1: dom (f^2) = dom f /\ dom f by Def4
.= dom f;
let c be object;
per cases;
suppose
c in dom f;
hence thesis by A1,Def4;
end;
suppose
A2: not c in dom f;
hence f^2.c = 0 qua Complex^2 by A1,FUNCT_1:def 2
.= (f.c)^2 by A2,FUNCT_1:def 2;
end;
end;
registration
let f be complex-valued Function;
cluster f^2 -> complex-valued;
coherence;
end;
registration
let f be real-valued Function;
cluster f^2 -> real-valued;
coherence;
end;
registration
let f be rational-valued Function;
cluster f^2 -> RAT-valued;
coherence;
end;
registration
let f be integer-valued Function;
cluster f^2 -> INT-valued;
coherence;
end;
registration
let f be natural-valued Function;
cluster f^2 -> natural-valued;
coherence;
end;
definition
let C be set;
let D be complex-membered set;
let f be PartFunc of C,D;
redefine func f^2 -> PartFunc of C,COMPLEX; :: redefines ^2 (VALUED_1, definition)
coherence
proof
dom (f^2) = dom f & rng (f^2) c= COMPLEX by Th11;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be real-membered set;
let f be PartFunc of C,D;
redefine func f^2 -> PartFunc of C,REAL; :: redefines ^2 (VALUED_1, definition)
coherence
proof
dom (f^2) = dom f & rng (f^2) c= REAL by Th11,VALUED_0:def 3;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be rational-membered set;
let f be PartFunc of C,D;
redefine func f^2 -> PartFunc of C,RAT; :: redefines ^2 (VALUED_1, definition)
coherence
proof
dom (f^2) = dom f & rng (f^2) c= RAT by Th11,RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be integer-membered set;
let f be PartFunc of C,D;
redefine func f^2 -> PartFunc of C,INT; :: redefines ^2 (VALUED_1, definition)
coherence
proof
dom (f^2) = dom f & rng (f^2) c= INT by Th11,RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be natural-membered set;
let f be PartFunc of C,D;
redefine func f^2 -> PartFunc of C,NAT; :: redefines ^2 (VALUED_1, definition)
coherence
proof
dom (f^2) = dom f & rng (f^2) c= NAT by Th11,VALUED_0:def 6;
hence thesis by RELSET_1:4;
end;
end;
registration
let C be set;
let D be complex-membered non empty set;
let f be Function of C,D;
cluster f^2 -> total for PartFunc of C,COMPLEX;
coherence;
end;
registration
let C be set;
let D be real-membered non empty set;
let f be Function of C,D;
cluster f^2 -> total for PartFunc of C,REAL;
coherence;
end;
registration
let C be set;
let D be rational-membered non empty set;
let f be Function of C,D;
cluster f^2 -> total for PartFunc of C,RAT;
coherence;
end;
registration
let C be set;
let D be integer-membered non empty set;
let f be Function of C,D;
cluster f^2 -> total for PartFunc of C,INT;
coherence;
end;
registration
let C be set;
let D be natural-membered non empty set;
let f be Function of C,D;
cluster f^2 -> total for PartFunc of C,NAT;
coherence;
end;
registration
let f be complex-valued FinSequence;
cluster f^2 -> FinSequence-like;
coherence;
end;
begin :: f1 - f2
definition
let f1,f2 be complex-valued Function;
func f1 - f2 -> Function equals
f1 + - f2;
coherence;
end;
registration
let f1,f2 be complex-valued Function;
cluster f1-f2 -> complex-valued;
coherence;
end;
registration
let f1,f2 be real-valued Function;
cluster f1-f2 -> real-valued;
coherence;
end;
registration
let f1,f2 be rational-valued Function;
cluster f1-f2 -> RAT-valued;
coherence;
end;
registration
let f1,f2 be integer-valued Function;
cluster f1-f2 -> INT-valued;
coherence;
end;
theorem Th12:
for f1,f2 being complex-valued Function holds dom (f1-f2) = dom
f1 /\ dom f2
proof
let f1,f2 be complex-valued Function;
thus dom (f1-f2) = dom f1 /\ dom -f2 by Def1
.= dom f1 /\ dom f2 by Def5;
end;
theorem
for f1,f2 being complex-valued Function
for c being object st c in dom (f1-f2) holds (f1-f2).c = f1.c - f2.c
proof
let f1,f2 be complex-valued Function;
let c be object;
assume c in dom (f1-f2);
hence (f1-f2).c = f1.c+(-f2).c by Def1
.= f1.c-f2.c by Th8;
end;
theorem
for f1,f2 being complex-valued Function, f being Function st dom f =
dom (f1-f2) & for c being object st c in dom f holds f.c = f1.c - f2.c
holds f = f1-f2
proof
let f1,f2 be complex-valued Function, f be Function such that
A1: dom f = dom (f1-f2) and
A2: for c being object st c in dom f holds f.c = f1.c - f2.c;
thus dom f = dom (f1-f2) by A1;
let c be object;
assume
A3: c in dom f;
hence f.c = f1.c - f2.c by A2
.= f1.c+(-f2).c by Th8
.= (f1-f2).c by A1,A3,Def1;
end;
definition
let C be set;
let D1,D2 be complex-membered set;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
redefine func f1-f2 -> PartFunc of C,COMPLEX; :: redefines - (VALUED_1, definition)
coherence
proof
dom (f1-f2) = dom f1 /\ dom f2 & rng (f1-f2) c= COMPLEX by Th12;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D1,D2 be real-membered set;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
redefine func f1-f2 -> PartFunc of C,REAL; :: redefines - (VALUED_1, definition)
coherence
proof
dom (f1-f2) = dom f1 /\ dom f2 & rng (f1-f2) c= REAL by Th12,VALUED_0:def 3
;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D1,D2 be rational-membered set;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
redefine func f1-f2 -> PartFunc of C,RAT; :: redefines - (VALUED_1, definition)
coherence
proof
dom (f1-f2) = dom f1 /\ dom f2 & rng (f1-f2) c= RAT by Th12,RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D1,D2 be integer-membered set;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
redefine func f1-f2 -> PartFunc of C,INT; :: redefines - (VALUED_1, definition)
coherence
proof
dom (f1-f2) = dom f1 /\ dom f2 & rng (f1-f2) c= INT by Th12,RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
end;
Lm3: for C being set, D1,D2 being complex-membered non empty set, f1 being
Function of C,D1, f2 being Function of C,D2 holds dom(f1-f2) = C
proof
let C be set;
let D1,D2 be complex-membered non empty set;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
thus dom(f1-f2) = dom f1 /\ dom -f2 by Def1
.= C /\ dom -f2 by FUNCT_2:def 1
.= C /\ C by FUNCT_2:def 1
.= C;
end;
registration
let C be set;
let D1,D2 be complex-membered non empty set;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1-f2 -> total for PartFunc of C,COMPLEX;
coherence
by Lm3,PARTFUN1:def 2;
end;
registration
let C be set;
let D1,D2 be real-membered non empty set;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1-f2 -> total for PartFunc of C,REAL;
coherence
by Lm3,PARTFUN1:def 2;
end;
registration
let C be set;
let D1,D2 be rational-membered non empty set;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1-f2 -> total for PartFunc of C,RAT;
coherence
by Lm3,PARTFUN1:def 2;
end;
registration
let C be set;
let D1,D2 be integer-membered non empty set;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1-f2 -> total for PartFunc of C,INT;
coherence
by Lm3,PARTFUN1:def 2;
end;
theorem
for C being set, D1,D2 being complex-membered non empty set for f1
being Function of C,D1, f2 being Function of C,D2 for c being Element of C
holds (f1-f2).c = f1.c - f2.c
proof
let C be set;
let D1,D2 be complex-membered non empty set;
let f1 be Function of C,D1, f2 be Function of C,D2;
let c be Element of C;
A1: dom(f1-f2) = C by FUNCT_2:def 1;
per cases;
suppose
C is non empty;
hence (f1-f2).c = f1.c + (-f2).c by A1,Def1
.= f1.c - f2.c by Th8;
end;
suppose
A2: C is empty;
then f2.c = 0;
hence thesis by A2;
end;
end;
registration
let f1, f2 be complex-valued FinSequence;
cluster f1-f2 -> FinSequence-like;
coherence;
end;
begin :: f1 /" f2
definition
let f1,f2 be complex-valued Function;
func f1 /" f2 -> Function equals
f1 (#) (f2");
coherence;
end;
theorem Th16:
for f1,f2 being complex-valued Function holds dom (f1/"f2) = dom
f1 /\ dom f2
proof
let f1,f2 be complex-valued Function;
thus dom (f1/"f2) = dom f1 /\ dom (f2") by Def4
.= dom f1 /\ dom f2 by Def7;
end;
theorem
for f1,f2 being complex-valued Function
for c being object holds (f1/"f2).c = f1.c / f2.c
proof
let f1,f2 be complex-valued Function;
let c be object;
A1: dom (f1/"f2) = dom f1 /\ dom f2 by Th16;
per cases;
suppose
c in dom (f1/"f2);
hence (f1/"f2).c = f1.c * (f2").c by Def4
.= f1.c / f2.c by Th10;
end;
suppose
A2: not c in dom (f1/"f2);
then not c in dom f1 or not c in dom f2 by A1,XBOOLE_0:def 4;
then
A3: f1.c = 0 or f2.c = 0 by FUNCT_1:def 2;
thus (f1/"f2).c = 0 / 0 by A2,FUNCT_1:def 2
.= f1.c / f2.c by A3;
end;
end;
registration
let f1,f2 be complex-valued Function;
cluster f1/"f2 -> complex-valued;
coherence;
end;
registration
let f1,f2 be real-valued Function;
cluster f1/"f2 -> real-valued;
coherence;
end;
registration
let f1,f2 be rational-valued Function;
cluster f1/"f2 -> RAT-valued;
coherence;
end;
definition
let C be set;
let D1,D2 be complex-membered set;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
redefine func f1/"f2 -> PartFunc of C,COMPLEX; :: redefines /" (VALUED_1, definition)
coherence
proof
dom (f1/"f2) = dom f1 /\ dom f2 & rng (f1/"f2) c= COMPLEX by Th16;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D1,D2 be real-membered set;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
redefine func f1/"f2 -> PartFunc of C,REAL; :: redefines /" (VALUED_1, definition)
coherence
proof
dom (f1/"f2) = dom f1 /\ dom f2 & rng (f1/"f2) c= REAL by Th16,
VALUED_0:def 3;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D1,D2 be rational-membered set;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
redefine func f1/"f2 -> PartFunc of C,RAT; :: redefines /" (VALUED_1, definition)
coherence
proof
dom (f1/"f2) = dom f1 /\ dom f2 & rng (f1/"f2) c= RAT by Th16,
RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
end;
Lm4: for C being set, D1,D2 being complex-membered non empty set for f1 being
Function of C,D1, f2 being Function of C,D2 holds dom(f1/"f2) = C
proof
let C be set;
let D1,D2 be complex-membered non empty set;
let f1 be Function of C,D1, f2 be Function of C,D2;
thus dom(f1/"f2) = dom f1 /\ dom f2 by Th16
.= C /\ dom f2 by FUNCT_2:def 1
.= C /\ C by FUNCT_2:def 1
.= C;
end;
registration
let C be set;
let D1,D2 be complex-membered non empty set;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1/"f2 -> total for PartFunc of C,COMPLEX;
coherence
by Lm4,PARTFUN1:def 2;
end;
registration
let C be set;
let D1,D2 be real-membered non empty set;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1/"f2 -> total for PartFunc of C,REAL;
coherence
by Lm4,PARTFUN1:def 2;
end;
registration
let C be set;
let D1,D2 be rational-membered non empty set;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1/"f2 -> total for PartFunc of C,RAT;
coherence
by Lm4,PARTFUN1:def 2;
end;
registration
let f1, f2 be complex-valued FinSequence;
cluster f1/"f2 -> FinSequence-like;
coherence;
end;
begin :: abs f
definition
let f be complex-valued Function;
deffunc F(object) = |.f.$1.|;
func |. f .| -> real-valued Function means
:Def11:
dom it = dom f & for c
being object st c in dom it holds it.c = |. f.c .|;
existence
proof
consider g being Function such that
A1: dom g = dom f & for x being object st x in dom f holds g.x = F(x)
from FUNCT_1:sch 3;
g is real-valued
proof
let x be object;
assume x in dom g;
then g.x = |. f.x .| by A1;
hence thesis;
end;
hence thesis by A1;
end;
uniqueness
proof
let h, g be real-valued Function such that
A2: dom h = dom f and
A3: for c being object st c in dom h holds h.c = F(c) and
A4: dom g = dom f and
A5: for c being object st c in dom g holds g.c = F(c);
now
let x be object;
assume
A6: x in dom h;
hence h.x = F(x) by A3
.= g.x by A2,A4,A5,A6;
end;
hence thesis by A2,A4;
end;
projectivity
proof
let r be real-valued Function;
let h be complex-valued Function;
assume that
dom r = dom h and
A7: for c being object st c in dom r holds r.c = |.h.c.|;
thus dom r = dom r;
let c be object;
assume
A8: c in dom r;
hence r.c = |.|.h.c.|.| by A7
.= |.r.c.| by A7,A8;
end;
end;
notation
let f be complex-valued Function;
synonym abs f for |. f .|;
end;
theorem
for f being complex-valued Function
for c being object holds |.f.|.c = |.f.c.|
proof
let f be complex-valued Function;
let c be object;
A1: dom |.f.| = dom f by Def11;
per cases;
suppose
c in dom f;
hence thesis by A1,Def11;
end;
suppose
A2: not c in dom f;
hence |.f.|.c = |.0 qua Complex.| by A1,COMPLEX1:44,FUNCT_1:def 2
.= |.f.c.| by A2,FUNCT_1:def 2;
end;
end;
registration
let f be rational-valued Function;
cluster |.f.| -> RAT-valued;
coherence
proof
let y be object;
assume y in rng |.f.|;
then consider x being object such that
A1: x in dom |.f.| and
A2: (|.f.|).x = y by FUNCT_1:def 3;
|.f.|.x = |.f.x.| by A1,Def11;
hence thesis by A2,RAT_1:def 2;
end;
end;
registration
let f be integer-valued Function;
cluster |.f.| -> natural-valued;
coherence
proof
let x be object;
|.f.x.| is natural;
hence thesis by Def11;
end;
end;
definition
let C be set;
let D be complex-membered set;
let f be PartFunc of C,D;
redefine func |.f.| -> PartFunc of C,REAL; :: redefines |. (VALUED_1, definition)
coherence
proof
dom |.f.| = dom f & rng |.f.| c= REAL by Def11;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be complex-membered set;
let f be PartFunc of C,D;
redefine func abs(f) -> PartFunc of C,REAL; :: redefines abs (VALUED_1, synonym) → |. (VALUED_1, definition)
coherence
proof
abs(f) = |.f.|;
hence thesis;
end;
end;
definition
let C be set;
let D be rational-membered set;
let f be PartFunc of C,D;
redefine func |.f.| -> PartFunc of C,RAT; :: redefines |. (VALUED_1, definition)
coherence
proof
dom |.f.| = dom f & rng |.f.| c= RAT by Def11,RELAT_1:def 19;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be rational-membered set;
let f be PartFunc of C,D;
redefine func abs(f) -> PartFunc of C,RAT; :: redefines abs (VALUED_1, synonym) → |. (VALUED_1, definition)
coherence
proof
abs(f) = |.f.|;
hence thesis;
end;
end;
definition
let C be set;
let D be integer-membered set;
let f be PartFunc of C,D;
redefine func |.f.| -> PartFunc of C,NAT; :: redefines |. (VALUED_1, definition)
coherence
proof
dom |.f.| = dom f & rng |.f.| c= NAT by Def11,VALUED_0:def 6;
hence thesis by RELSET_1:4;
end;
end;
definition
let C be set;
let D be integer-membered set;
let f be PartFunc of C,D;
redefine func abs(f) -> PartFunc of C,NAT; :: redefines abs (VALUED_1, synonym) → |. (VALUED_1, definition)
coherence
proof
abs(f) = |.f.|;
hence thesis;
end;
end;
registration
let C be set;
let D be complex-membered non empty set;
let f be Function of C,D;
cluster |.f.| -> total for PartFunc of C,REAL;
coherence
proof
dom |.f.| = dom f by Def11
.= C by FUNCT_2:def 1;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D be rational-membered non empty set;
let f be Function of C,D;
cluster |.f.| -> total for PartFunc of C,RAT;
coherence
proof
dom |.f.| = dom f by Def11
.= C by FUNCT_2:def 1;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let C be set;
let D be integer-membered non empty set;
let f be Function of C,D;
cluster |.f.| -> total for PartFunc of C,NAT;
coherence
proof
dom |.f.| = dom f by Def11
.= C by FUNCT_2:def 1;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let f be complex-valued FinSequence;
cluster |.f.| -> FinSequence-like;
coherence
proof
dom abs f = dom f by Def11;
hence thesis by Lm1;
end;
end;
theorem
for f, g being FinSequence, h being Function st dom h = dom f /\ dom g
holds h is FinSequence by Lm2;
begin :: Addenda
:: from RELOC, 2008.02.14, A.T.
reserve m,j,p,q,n,l for Element of NAT;
definition
let p be Function, k be Nat;
func Shift(p,k) -> Function means
:Def12:
dom it = { m+k where m is Nat:m in dom p } &
for m being Nat st m in dom p holds it.(m+k) = p.m;
existence
proof
defpred P[object,object] means ex m being Nat st $1 = m+k & $2 = p.m;
set A = { m+k where m is Nat:m in dom p };
A1: for e being object st e in A ex u being object st P[e,u]
proof
let e be object;
assume e in A;
then consider m being Nat such that
A2: e = m+k and
m in dom p;
take p.m;
thus thesis by A2;
end;
consider f being Function such that
A3: dom f = A and
A4: for e being object st e in A holds P[e,f.e] from CLASSES1:sch 1(A1);
take f;
thus dom f = { m+k where m is Nat :m in dom p } by A3;
let m be Nat;
assume m in dom p;
then m+k in A;
then ex j being Nat st m+k = j+k & f.(m+k) = p.j by A4;
hence thesis;
end;
uniqueness
proof
let IT1,IT2 be Function such that
A5: dom IT1 = { m+k where m is Nat:m in dom p } and
A6: for m being Nat st m in dom p holds IT1.(m+k) = p.m and
A7: dom IT2 = { m+k where m is Nat:m in dom p } and
A8: for m being Nat st m in dom p holds IT2.(m+k) = p.m;
for x being object st x in dom IT1 holds IT1.x = IT2.x
proof
let x be object;
assume x in dom IT1;
then consider m being Nat such that
A9: x = m+k & m in dom p by A5;
thus IT1.x = p.m by A6,A9
.= IT2.x by A8,A9;
end;
hence thesis by A5,A7;
end;
end;
registration
let p be Function, k be Nat;
cluster Shift(p,k) -> NAT-defined;
coherence
proof
A1: dom Shift(p,k) = { m+k where m is Nat:m in dom p } by Def12;
Shift(p,k) is NAT-defined
proof
let x be object;
assume x in dom Shift(p,k);
then ex m being Nat st x = m+k & m in dom p by A1;
hence thesis by ORDINAL1:def 12;
end;
hence thesis;
end;
end;
theorem :: SCMFSA8C:11
for P,Q being Function, k being Nat st P c= Q holds Shift(P
,k) c= Shift(Q,k)
proof
let P,Q be Function;
let k be Nat;
assume
A1: P c= Q;
then
A2: dom P c= dom Q by GRFUNC_1:2;
A3: dom Shift(P,k) = {m + k where m is Nat: m in dom P} by Def12;
A4: dom Shift(Q,k) = {m + k where m is Nat: m in dom Q} by Def12;
A5: now
let x be object;
assume x in dom Shift(P,k);
then ex m1 being Nat st x = m1 + k & m1 in dom P by A3;
hence x in dom Shift(Q,k) by A2,A4;
end;
now
let x be object;
assume x in dom Shift(P,k);
then consider m1 being Nat such that
A6: x = m1 + k and
A7: m1 in dom P by A3;
thus Shift(P,k).x = Shift(P,k).(m1 + k) by A6
.= P.m1 by A7,Def12
.= Q.m1 by A1,A7,GRFUNC_1:2
.= Shift(Q,k).(m1 + k) by A2,A7,Def12
.= Shift(Q,k).x by A6;
end;
hence thesis by A5,GRFUNC_1:2,TARSKI:def 3;
end;
theorem :: SCMFSA_4:32
for n,m being Nat
for I being Function holds Shift(Shift(I,m),n) = Shift(I,m+n)
proof let n,m be Nat;
let I be Function;
set A = {l+m where l is Nat:l in dom I };
A1: dom Shift(I,m) = A by Def12;
A2: now
let l be Nat;
assume
A3: l in dom I;
then
A4: l+m in dom Shift(I,m) by A1;
thus Shift(Shift(I,m),n).(l+(m+n)) = Shift(Shift(I,m),n).(l+m+n)
.= Shift(I,m).(l+m) by A4,Def12
.= I.l by A3,Def12;
end;
{p+n where p is Nat: p in A } = { q+(m+n) where q is Nat: q in dom I}
proof
thus {p+n where p is Nat: p in A } c= { q+(m+n) where q is Nat: q in dom I}
proof
let x be object;
assume x in {p+n where p is Nat: p in A };
then consider p being Nat such that
A5: x = p+n and
A6: p in A;
consider l being Nat such that
A7: p = l+m and
A8: l in dom I by A6;
x = l+(m+n) by A5,A7;
hence thesis by A8;
end;
let x be object;
assume x in { q+(m+n) where q is Nat: q in dom I};
then consider q being Nat such that
A9: x = q+(m+n) & q in dom I;
x = (q+m)+n & q+m in A by A9;
hence thesis;
end;
then dom Shift(Shift(I,m),n) =
{ l+(m+n) where l is Nat: l in dom I} by A1,Def12;
hence thesis by A2,Def12;
end;
theorem :: SCMFSA_4:33
for s,f be Function for n being Nat holds Shift(f*s,n) = f*Shift(s,n)
proof
let s,f be Function;
let n be Nat;
A1: dom(f*s) c= dom s by RELAT_1:25;
A2: dom Shift(s,n)= { m+n where m is Nat: m in dom s } by Def12;
now
let e be object;
thus e in { m+n where m is Nat: m in dom(f*s) }
implies e in dom Shift(s,n) & Shift(s,n).
e in dom f
proof
assume e in { m+n where m is Nat: m in dom(f*s) };
then consider m being Nat such that
A3: e = m+n and
A4: m in dom(f*s);
thus e in dom Shift(s,n) by A2,A1,A3,A4;
Shift(s,n).e = s.m by A1,A3,A4,Def12;
hence thesis by A4,FUNCT_1:11;
end;
assume e in dom Shift(s,n);
then consider m0 being Nat such that
A5: e = m0+n and
A6: m0 in dom s by A2;
assume Shift(s,n).e in dom f;
then s.m0 in dom f by A5,A6,Def12;
then m0 in dom(f*s) by A6,FUNCT_1:11;
hence e in { m+n where m is Nat: m in dom(f*s) } by A5;
end;
then Shift(s,n)"dom f = { m+n where m is Nat: m in dom(f*s) }
by FUNCT_1:def 7;
then
A7: dom(f*Shift(s,n)) = { m+n where m is Nat: m in dom(f*s) } by RELAT_1:147;
now
let m be Nat;
assume
A8: m in dom(f*s);
then m+n in dom Shift(s,n) by A2,A1;
hence (f*Shift(s,n)).(m+n) = f.(Shift(s,n).(m+n)) by FUNCT_1:13
.= f.(s.m) by A1,A8,Def12
.= (f*s).m by A8,FUNCT_1:12;
end;
hence thesis by A7,Def12;
end;
theorem :: SCMFSA_4:34
for I,J being Function, n being Nat
holds Shift(I +* J, n) = Shift(I,n) +* Shift(J,n)
proof
let I,J be Function, n be Nat;
A1: dom Shift(J,n) = { m+n where m is Nat: m in dom J } by Def12;
A2: now
let m be Nat such that
A3: m in dom(I +* J);
per cases;
suppose
A4: m in dom J;
then m+n in dom Shift(J,n) by A1;
hence (Shift(I,n) +* Shift(J,n)).(m+n) = Shift(J,n).(m+n) by FUNCT_4:13
.= J.m by A4,Def12
.= (I +* J).m by A4,FUNCT_4:13;
end;
suppose
A5: not m in dom J;
m in dom I \/ dom J by A3,FUNCT_4:def 1;
then
A6: m in dom I by A5,XBOOLE_0:def 3;
not ex l being Nat st m+n = l+n & l in dom J by A5;
then not m+n in dom Shift(J,n) by A1;
hence (Shift(I,n) +* Shift(J,n)).(m+n) = Shift(I,n).(m+n) by FUNCT_4:11
.= I.m by A6,Def12
.= (I +* J).m by A5,FUNCT_4:11;
end;
end;
A7: dom Shift(I,n) = { m+n where m is Nat: m in dom I } by Def12;
A8: dom Shift(I,n) \/ dom Shift(J,n)
= { m+n where m is Nat: m in dom I \/ dom J }
proof
hereby
let x be object;
assume x in dom Shift(I,n) \/ dom Shift(J,n);
then x in dom Shift(I,n) or x in dom Shift(J,n) by XBOOLE_0:def 3;
then consider m being Nat such that
A9: x = m+n & m in dom J or x = m+n & m in dom I by A1,A7;
m in dom I \/ dom J by A9,XBOOLE_0:def 3;
hence x in { l+n where l is Nat: l in dom I \/ dom J } by A9;
end;
let x be object;
assume x in { m+n where m is Nat: m in dom I \/ dom J };
then consider m being Nat such that
A10: x = m+n and
A11: m in dom I \/ dom J;
m in dom I or m in dom J by A11,XBOOLE_0:def 3;
then x in dom Shift(I,n) or x in dom Shift(J,n) by A1,A7,A10;
hence thesis by XBOOLE_0:def 3;
end;
dom(I +* J) = dom I \/ dom J by FUNCT_4:def 1;
then dom(Shift(I,n) +* Shift(J,n)) =
{ m+n where m is Nat: m in dom(I +* J ) } by A8,FUNCT_4:def 1;
hence thesis by A2,Def12;
end;
:: from SCMPDS_4, 2008.03.16, A.T.
theorem Th24:
for p being Function,k,il being Nat st il in dom p
holds il+k in dom Shift(p,k)
proof
let p be Function, k,il be Nat such that
A1: il in dom p;
dom Shift(p,k) = { loc+k where loc is Nat : loc in dom p} by Def12;
hence thesis by A1;
end;
:: missing, 2008.03.16, A.T.
theorem Th25:
for p being Function, k being Nat holds rng Shift(p,k) c= rng p
proof
let p be Function, k being Nat;
let y be object;
assume y in rng Shift(p,k);
then consider x being object such that
A1: x in dom Shift(p,k) and
A2: y = Shift(p,k).x by FUNCT_1:def 3;
x in { m+k where m is Nat:m in dom p } by A1,Def12;
then consider m being Nat such that
A3: x = m+k and
A4: m in dom p;
p.m = Shift(p,k).x by A3,A4,Def12;
hence thesis by A2,A4,FUNCT_1:def 3;
end;
theorem
for p being Function st dom p c= NAT for k being Nat holds
rng Shift(p,k) = rng p
proof
let p be Function such that
A1: dom p c= NAT;
let k be Nat;
thus rng Shift(p,k) c= rng p by Th25;
let y be object;
assume y in rng p;
then consider x being object such that
A2: x in dom p and
A3: y = p.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A1,A2;
x+k in dom Shift(p,k) & Shift(p,k).(x+k) = y by A2,A3,Def12,Th24;
hence thesis by FUNCT_1:def 3;
end;
registration
let p be finite Function, k be Nat;
cluster Shift(p,k) -> finite;
coherence
proof
deffunc F(Nat) = $1+k;
A1: dom p is finite;
A2: { F(w) where w is Element of NAT: w in dom p } is finite
from FRAENKEL:sch 21(A1);
dom Shift(p,k) c= { F(w) where w is Element of NAT: w in dom p }
proof
let e be object;
assume e in dom Shift(p,k);
then e in { F(i) where i is Nat: i in dom p } by Def12;
then consider i being Nat such that
A3: e = F(i) & i in dom p;
reconsider i as Element of NAT by ORDINAL1:def 12;
e = F(i) & i in dom p by A3;
hence e in { F(w) where w is Element of NAT: w in dom p };
end;
hence thesis by A2,FINSET_1:10;
end;
end;
reserve e1,e2 for ExtReal;
definition
let X be non empty ext-real-membered set, s be sequence of X;
redefine attr s is increasing means :: redefines increasing (VALUED_0, definition)
for n being Nat holds s.n < s.(n+1);
compatibility
proof
thus s is increasing implies for n being Nat holds s.n < s.(n+1 )
proof
assume
A1: s is increasing;
let n be Nat;
A2: n < n+1 by NAT_1:13;
dom s = NAT & n in NAT by FUNCT_2:def 1,ORDINAL1:def 12;
hence thesis by A1,A2;
end;
assume
A3: for n being Nat holds s.n < s.(n+1);
let e1,e2;
assume e1 in dom s & e2 in dom s;
then reconsider m=e1, n=e2 as Nat;
defpred P[Nat] means m < $1 implies s.m < s.$1;
A4: for j being Nat st P[j] holds P[j+1]
proof
let j being Nat such that
A5: P[j];
assume m < j+1;
then m <= j by NAT_1:13;
then s.m < s.j or m = j by A5,XXREAL_0:1;
hence thesis by A3,XXREAL_0:2;
end;
assume
A6: e1 < e2;
A7: P[0];
for j being Nat holds P[j] from NAT_1:sch 2(A7,A4);
then s.m < s.n by A6;
hence thesis;
end;
redefine attr s is decreasing means :: redefines decreasing (VALUED_0, definition)
for n being Nat holds s.n > s.(n+1);
compatibility
proof
thus s is decreasing implies for n being Nat holds s.n > s.(n+1 )
proof
assume
A8: s is decreasing;
let n be Nat;
A9: n < n+1 by NAT_1:13;
dom s = NAT & n in NAT by FUNCT_2:def 1,ORDINAL1:def 12;
hence thesis by A8,A9;
end;
assume
A10: for n being Nat holds s.n > s.(n+1);
let e1,e2;
assume e1 in dom s & e2 in dom s;
then reconsider m=e1, n=e2 as Nat;
defpred P[Nat] means m < $1 implies s.m > s.$1;
A11: for j being Nat st P[j] holds P[j+1]
proof
let j being Nat such that
A12: P[j];
assume m < j+1;
then m <= j by NAT_1:13;
then s.m > s.j or m = j by A12,XXREAL_0:1;
hence thesis by A10,XXREAL_0:2;
end;
assume
A13: e1 < e2;
A14: P[0];
for j being Nat holds P[j] from NAT_1:sch 2(A14,A11);
then s.m > s.n by A13;
hence thesis;
end;
redefine attr s is non-decreasing means :: redefines non-decreasing (VALUED_0, definition)
for n being Nat holds s.n <= s.(n+1);
compatibility
proof
thus s is non-decreasing implies for n being Nat holds s.n <= s.(n+1 )
proof
assume
A15: s is non-decreasing;
let n be Nat;
A16: n < n+1 by NAT_1:13;
dom s = NAT & n in NAT by FUNCT_2:def 1,ORDINAL1:def 12;
hence thesis by A15,A16;
end;
assume
A17: for n being Nat holds s.n <= s.(n+1);
let e1,e2;
assume e1 in dom s & e2 in dom s;
then reconsider m=e1, n=e2 as Nat;
defpred P[Nat] means m <= $1 implies s.m <= s.$1;
A18: for j being Nat st P[j] holds P[j+1]
proof
let j being Nat such that
A19: P[j];
assume m <= j+1;
then
A20: m < j+1 or m = j+1 by XXREAL_0:1;
s.j <= s.(j+1) by A17;
hence thesis by A19,A20,NAT_1:13,XXREAL_0:2;
end;
assume
A21: e1 <= e2;
A22: P[0];
for j being Nat holds P[j] from NAT_1:sch 2(A22,A18);
then s.m <= s.n by A21;
hence thesis;
end;
redefine attr s is non-increasing means :: redefines non-increasing (VALUED_0, definition)
for n being Nat holds s.n >= s.(n+1);
compatibility
proof
thus s is non-increasing implies for n being Nat holds s.n >= s.(n+1 )
proof
assume
A23: s is non-increasing;
let n be Nat;
A24: n < n+1 by NAT_1:13;
dom s = NAT & n in NAT by FUNCT_2:def 1,ORDINAL1:def 12;
hence thesis by A23,A24;
end;
assume
A25: for n being Nat holds s.n >= s.(n+1);
let e1,e2;
assume e1 in dom s & e2 in dom s;
then reconsider m=e1, n=e2 as Nat;
defpred P[Nat] means m <= $1 implies s.m >= s.$1;
A26: for j being Nat st P[j] holds P[j+1]
proof
let j being Nat such that
A27: P[j];
assume m <= j+1;
then
A28: m < j+1 or m = j+1 by XXREAL_0:1;
s.j >= s.(j+1) by A25;
hence thesis by A27,A28,NAT_1:13,XXREAL_0:2;
end;
assume
A29: e1 <= e2;
A30: P[0];
for j being Nat holds P[j] from NAT_1:sch 2(A30,A26);
then s.m >= s.n by A29;
hence thesis;
end;
end;
:: from KURATO_2, 2008.09.05, A.T.
scheme
SubSeqChoice { X() -> non empty set, S() -> sequence of X(), P[set]} :
ex S1 being subsequence of S() st for n being Element of NAT holds P[S1.n]
provided
A1: for n being Element of NAT ex m being Element of NAT st n <= m & P[S
().m]
proof
defpred P1[set,set,set] means $3 in NAT & (for m,k being Element of NAT st m
= $2 & k = $3 holds m < k & P[S().k]);
consider n0 being Element of NAT such that
0 <= n0 and
A2: P[S().n0] by A1;
A3: for n being Nat for x being set ex y being set st P1[n,x,y]
proof
let n be Nat, x be set;
per cases;
suppose
x in NAT;
then reconsider mx = x as Element of NAT;
consider my being Element of NAT such that
A4: mx + 1 <= my & P[S().my] by A1;
take my;
thus my in NAT;
thus thesis by A4,NAT_1:13;
end;
suppose
A5: not x in NAT;
take 0;
set y = 0;
thus y in NAT;
let m, k be Element of NAT;
assume that
A6: m = x and
k = y;
thus thesis by A5,A6;
end;
end;
consider g being Function such that
A7: dom g = NAT and
A8: g.0 = n0 and
A9: for n being Nat holds P1[n,g.n,g.(n+1)] from RECDEF_1:
sch 1(A3);
rng g c= NAT
proof
defpred P[Nat] means g.$1 in NAT;
let y be object;
assume y in rng g;
then consider x being object such that
A10: x in dom g and
A11: g.x = y by FUNCT_1:def 3;
reconsider n = x as Element of NAT by A7,A10;
A12: for k being Nat holds P[k] implies P[k+1] by A9;
A13: P[0] by A8;
for k being Nat holds P[k] from NAT_1:sch 2(A13,A12);
then g.n in NAT;
hence thesis by A11;
end;
then reconsider g as sequence of NAT by A7,FUNCT_2:2;
g is increasing
by A9;
then reconsider g as increasing sequence of NAT;
reconsider S1 = S() * g as sequence of X();
A14: dom S1 = NAT by FUNCT_2:def 1;
reconsider S1 as subsequence of S();
take S1;
thus for n being Element of NAT holds P[S1.n]
proof
let n be Element of NAT;
per cases;
suppose
n = 0;
hence thesis by A2,A8,A14,FUNCT_1:12;
end;
suppose
n <> 0;
then n >= 0 qua Nat + 1 by NAT_1:13;
then reconsider n9 = n-1 as Element of NAT by INT_1:5;
reconsider k = g.(n9+1) as Element of NAT;
for m,k being Element of NAT st m = g.n9 & k = g.(n9+1) holds P[S()
.k] by A9;
then P[S().k];
hence thesis by A14,FUNCT_1:12;
end;
end;
end;
:: from AMISTD_2, 2010.02.05, A.T.
theorem
for k being Nat
for F being NAT-defined Function
holds dom F,dom Shift(F,k) are_equipotent
proof
let k be Nat;
let F be NAT-defined Function;
defpred P[object,object] means
ex il being Element of NAT
st $1 = il & $2 = k+il;
A1: for e being object st e in dom F ex u being object st P[e,u]
proof
let e be object;
assume e in dom F;
then reconsider e as Element of NAT;
take k+e, e;
thus thesis;
end;
consider f being Function such that
A2: dom f = dom F and
A3: for x being object st x in dom F holds P[x,f.x] from CLASSES1:sch 1(A1);
take f;
hereby
let x1, x2 be object such that
A4: x1 in dom f and
A5: x2 in dom f and
A6: f.x1 = f.x2;
consider i1 being Element of NAT such that
A7: x1 = i1 and
A8: f.x1 = k+i1 by A2,A3,A4;
consider i2 being Element of NAT such that
A9: x2 = i2 and
A10: f.x2 = k+i2 by A2,A3,A5;
thus x1 = x2 by A7,A6,A8,A10,A9;
end;
thus dom f = dom F by A2;
A11: dom Shift(F,k) = { (m+k) where m is Nat: m in dom F } by Def12;
hereby
let y be object;
assume y in rng f;
then consider x being object such that
A12: x in dom f and
A13: f.x = y by FUNCT_1:def 3;
consider il being Element of NAT such that
A14: x = il and
A15: f.x = k+il by A2,A3,A12;
thus y in dom Shift(F,k) by A2,A11,A12,A13,A14,A15;
end;
let y be object;
assume y in dom Shift(F,k);
then consider m being Nat such that
A16: y = (m+k) and
A17: m in dom F by A11;
consider il being Element of NAT such that
A18: m = il and
A19: f.m = k+il by A3,A17;
thus thesis by A2,A16,A17,A18,A19,FUNCT_1:def 3;
end;
registration
let F be NAT-defined Function;
reduce Shift(F,0) to F;
reducibility
proof
A1: dom F = { m+(0 qua Nat) where m is Nat: m in dom F }
proof
hereby
let a be object;
assume
A2: a in dom F;
then reconsider l=a as Element of NAT;
a = (l qua Nat)+(0 qua Complex);
hence a in { m+(0 qua Nat)
where m is Nat: m in dom F } by A2;
end;
let a be object;
assume
a in { m+(0 qua Complex) where m is Nat: m in dom F };
then ex m being Nat
st a = m+(0 qua Complex) & m in dom F;
hence thesis;
end;
for m being Nat st m in dom F holds F.(m+(0 qua Complex)) = F.m;
hence thesis by A1,Def12;
end;
end;
registration
let X be non empty set;
let F be X-valued Function, k be Nat;
cluster Shift(F,k) -> X-valued;
coherence
proof
A1: dom Shift(F,k) = { (m+k) where m is Nat: m in dom F } by Def12;
thus rng Shift(F,k) c= X
proof let x be object;
assume x in rng Shift(F,k);
then consider y being object such that
A2: y in dom Shift(F,k) and
A3: x = Shift(F,k).y by FUNCT_1:def 3;
consider m being Nat such that
A4: y = (m+k) and
A5: m in dom F by A2,A1;
Shift(F,k).(m+k) = F.m by A5,Def12
.= F/.m by A5,PARTFUN1:def 6;
hence x in X by A3,A4;
end;
end;
end;
registration :: move somewhere !!!
cluster non empty NAT-defined for Function;
existence
proof
take id NAT;
thus thesis;
end;
end;
registration
let F be empty Function, k be Nat;
cluster Shift(F,k) -> empty;
coherence
proof
A1: dom Shift(F,k) = { (m+k) where m is Nat: m in dom F } by Def12;
assume Shift(F,k) is non empty;
then reconsider f = Shift(F,k) as non empty Function;
dom f is non empty;
then consider a being object such that
A2: a in dom Shift(F,k);
ex m being Nat st a = (m+k) & m in dom F by A1,A2;
hence thesis;
end;
end;
registration
let F be non empty NAT-defined Function, k be Nat;
cluster Shift(F,k) -> non empty;
coherence
proof
A1: dom Shift(F,k) = { (m+k) where m is Nat: m in dom F } by Def12;
consider a being object such that
A2: a in dom F by XBOOLE_0:def 1;
reconsider a as Element of NAT by A2;
consider m being Nat such that
A3: a = m;
reconsider m as Element of NAT by ORDINAL1:def 12;
(m+k) in dom Shift(F,k) by A1,A2,A3;
hence thesis;
end;
end;
::$CT
theorem
for F being Function, k being Nat st k > 0
holds not 0 in dom Shift(F,k)
proof
let F be Function, k be Nat such that
A1: k > 0 and
A2: 0 in dom Shift(F,k);
dom Shift(F,k) = { m+k where m is Nat: m in dom F } by Def12;
then ex m being Nat st 0 = m+k & m in dom F by A2;
hence contradiction by A1;
end;
registration
cluster NAT-defined finite non empty for Function;
existence
proof
take f = 0 .--> 0;
thus dom f c= NAT by ZFMISC_1:31;
thus thesis;
end;
end;
registration
let F be NAT-defined Relation;
cluster dom F -> natural-membered;
coherence;
end;
definition
let F be non empty NAT-defined finite Function;
func LastLoc F -> Element of NAT equals
max dom F;
coherence by ORDINAL1:def 12;
end;
definition
let F be non empty NAT-defined finite Function;
func CutLastLoc F -> Function equals
F \ ( LastLoc F .--> F.LastLoc F );
coherence;
end;
registration
let F be non empty NAT-defined finite Function;
cluster CutLastLoc F -> NAT-defined finite;
coherence;
end;
theorem
for F being non empty NAT-defined finite Function holds
LastLoc F in dom F by XXREAL_2:def 8;
theorem
for F, G being non empty NAT-defined finite Function st F c= G holds
LastLoc F <= LastLoc G by RELAT_1:11,XXREAL_2:59;
theorem
for F being non empty NAT-defined finite Function, l being
Element of NAT st l in dom F holds l <= LastLoc F by XXREAL_2:def 8;
definition
let F be non empty NAT-defined Function;
func FirstLoc F -> Element of NAT equals
min dom F;
coherence by ORDINAL1:def 12;
end;
theorem
for F being non empty NAT-defined finite Function holds
FirstLoc F in dom F by XXREAL_2:def 7;
theorem
for F, G being non empty NAT-defined finite Function st F c= G holds
FirstLoc G <= FirstLoc F by RELAT_1:11,XXREAL_2:60;
theorem
for l1 being Element of NAT
for F being non empty NAT-defined finite Function st l1 in dom
F holds FirstLoc F <= l1 by XXREAL_2:def 7;
theorem Th35:
for F being non empty NAT-defined finite Function
holds dom CutLastLoc F = (dom F) \ {LastLoc F}
proof
let F be non empty NAT-defined finite Function;
A1: dom (LastLoc F .--> (F.LastLoc F)) = {LastLoc F};
reconsider R = {[LastLoc F, F.LastLoc F]} as Relation;
A2: R = LastLoc F .--> (F.LastLoc F) by FUNCT_4:82;
then
A3: dom R = {LastLoc F};
thus dom CutLastLoc F c= (dom F) \ {LastLoc F}
proof
let x be object;
assume x in dom CutLastLoc F;
then consider y being object such that
A4: [x,y] in F \ R by A2,XTUPLE_0:def 12;
A5: not [x,y] in R by A4,XBOOLE_0:def 5;
A6: x in dom F by A4,XTUPLE_0:def 12;
per cases by A5,TARSKI:def 1;
suppose x <> LastLoc F;
then not x in dom R by A3,TARSKI:def 1;
hence thesis by A2,A6,XBOOLE_0:def 5;
end;
suppose
A7: y <> F.LastLoc F;
now
assume x in dom R;
then x = LastLoc F by A3,TARSKI:def 1;
hence contradiction by A4,A7,FUNCT_1:1;
end;
hence thesis by A2,A6,XBOOLE_0:def 5;
end;
end;
thus thesis by A1,XTUPLE_0:25;
end;
theorem
for F being non empty NAT-defined finite Function
holds dom F = dom CutLastLoc F \/ {LastLoc F}
proof
let F be non empty NAT-defined finite Function;
LastLoc F in dom F by XXREAL_2:def 8;
then
A1: {LastLoc F} c= dom F by ZFMISC_1:31;
dom CutLastLoc F = (dom F) \ {LastLoc F} by Th35;
hence thesis by A1,XBOOLE_1:45;
end;
registration
cluster 1-element NAT-defined finite for Function;
existence
proof
take 0 .--> 0;
thus thesis;
end;
end;
registration
let F be 1-element NAT-defined finite Function;
cluster CutLastLoc F -> empty;
coherence
proof
LastLoc F in dom F by XXREAL_2:def 8;
then
A1: [LastLoc F,F.LastLoc F] in F by FUNCT_1:def 2;
assume not thesis;
then consider a being object such that
A2: a in CutLastLoc F;
A3: a = [LastLoc F,F.LastLoc F] by A1,A2,ZFMISC_1:def 10;
not a in LastLoc F .--> F.LastLoc F by A2,XBOOLE_0:def 5;
then not a in {[LastLoc F,F.LastLoc F]} by FUNCT_4:82;
hence thesis by A3,TARSKI:def 1;
end;
end;
theorem Th37:
for F being non empty NAT-defined finite Function
holds card CutLastLoc F = card F - 1
proof
let F be non empty NAT-defined finite Function;
LastLoc F .--> F.LastLoc F c= F
proof
let a, b be object;
assume [a,b] in LastLoc F .--> F.LastLoc F;
then [a,b] in {[LastLoc F,F.LastLoc F]} by FUNCT_4:82;
then
A1: [a,b] = [LastLoc F,F.LastLoc F] by TARSKI:def 1;
LastLoc F in dom F by XXREAL_2:def 8;
hence thesis by A1,FUNCT_1:def 2;
end;
hence card CutLastLoc F = card F - card (LastLoc F .--> F.LastLoc F)
by CARD_2:44
.= card F - card {[LastLoc F,F.LastLoc F]} by FUNCT_4:82
.= card F - 1 by CARD_1:30;
end;
begin :: 2011.04.20, A.T.
registration let X be set, f be X-defined complex-valued Function;
cluster -f -> X-defined;
coherence
proof
A1: dom -f = dom f by Def5;
thus dom -f c= X by A1;
end;
cluster f" -> X-defined;
coherence
proof
A2: dom(f") = dom f by Def7;
thus dom(f") c= X by A2;
end;
cluster f^2 -> X-defined;
coherence
proof
A3: dom(f^2) = dom f by Th11;
thus dom(f^2) c= X by A3;
end;
cluster |.f.| -> X-defined;
coherence
proof
A4: dom |.f.| = dom f by Def11;
thus dom |.f.| c= X by A4;
end;
end;
registration let X be set;
cluster total for X-defined natural-valued Function;
existence
proof
take the total PartFunc of X, NAT;
thus thesis;
end;
end;
registration let X be set,
f be total X-defined complex-valued Function;
cluster -f -> total;
coherence
proof
A1: dom -f = dom f by Def5;
dom f = X by PARTFUN1:def 2;
hence thesis by A1,PARTFUN1:def 2;
end;
cluster f" -> total;
coherence
proof
A2: dom(f") = dom f by Def7;
dom f = X by PARTFUN1:def 2;
hence thesis by A2,PARTFUN1:def 2;
end;
cluster f^2 -> total;
coherence
proof
A3: dom(f^2) = dom f by Th11;
dom f = X by PARTFUN1:def 2;
hence thesis by A3,PARTFUN1:def 2;
end;
cluster |.f.| -> total;
coherence
proof
A4: dom |.f.| = dom f by Def11;
dom f = X by PARTFUN1:def 2;
hence thesis by A4,PARTFUN1:def 2;
end;
end;
registration
let X be set, f be X-defined complex-valued Function,
r be Complex;
cluster r+f -> X-defined;
coherence
proof
A1: dom(r+f) = dom f by Def2;
thus dom(r+f) c= X by A1;
end;
cluster f-r -> X-defined;
coherence;
cluster r(#)f -> X-defined;
coherence
proof
A2: dom(r(#)f) = dom f by Def5;
thus dom(r(#)f) c= X by A2;
end;
end;
registration let X be set,
f be total X-defined complex-valued Function,
r be Complex;
cluster r+f -> total;
coherence
proof
A1: dom(r+f) = dom f by Def2;
dom f = X by PARTFUN1:def 2;
hence thesis by A1,PARTFUN1:def 2;
end;
cluster f-r -> total;
coherence;
cluster r(#)f -> total;
coherence
proof
A2: dom(r(#)f) = dom f by Def5;
dom f = X by PARTFUN1:def 2;
hence thesis by A2,PARTFUN1:def 2;
end;
end;
registration
let X be set, f1 be complex-valued Function;
let f2 be X-defined complex-valued Function;
cluster f1 + f2 -> X-defined;
coherence
proof
A1: dom(f1 + f2) = dom f1 /\ dom f2 by Def1;
thus dom(f1 + f2) c= X by A1;
end;
cluster f1 - f2 -> X-defined;
coherence;
cluster f1(#)f2 -> X-defined;
coherence
proof
A2: dom(f1(#)f2) = dom f1 /\ dom f2 by Def4;
thus dom(f1(#)f2) c= X by A2;
end;
cluster f1/"f2 -> X-defined;
coherence;
end;
registration let X be set;
let f1,f2 be total X-defined complex-valued Function;
cluster f1 + f2 -> total;
coherence
proof
A1: dom(f1 + f2) = dom f1 /\ dom f2 by Def1;
dom f1 = X & dom f2 = X by PARTFUN1:def 2;
hence thesis by A1,PARTFUN1:def 2;
end;
cluster f1 - f2 -> total;
coherence;
cluster f1(#)f2 -> total;
coherence
proof
A2: dom(f1(#)f2) = dom f1 /\ dom f2 by Def4;
dom f1 = X & dom f2 = X by PARTFUN1:def 2;
hence thesis by A2,PARTFUN1:def 2;
end;
cluster f1/"f2 -> total;
coherence;
end;
registration let X be non empty set;
let F be X-valued non empty NAT-defined finite Function;
cluster CutLastLoc F -> X-valued;
coherence;
end;
theorem
for f being Function
for i,n being Nat st i in dom Shift(f,n)
ex j being Nat st j in dom f & i = j + n
proof let f be Function;
let i,n be Nat;
A1: dom Shift(f,n) = { m+n where m is Nat:m in dom f } by Def12;
assume i in dom Shift(f,n);
then ex m being Nat st i = m + n & m in dom f by A1;
hence ex j being Nat st j in dom f & i = j + n;
end;
:: from PNPROC_1, 2012.02.20, A.T.
registration
let p be FinSubsequence;
let i be Nat;
cluster Shift(p,i) -> FinSubsequence-like;
coherence
proof
set X = {k+i where k is Nat : k in dom p },
f = Shift(p,i);
consider K being Nat such that
A1: dom p c= Seg K by FINSEQ_1:def 12;
A2: dom f = X by Def12;
X c= Seg (i+K)
proof
let x be object;
assume x in X;
then consider k being Nat such that
A3: x = k+i and
A4: k in dom p;
A5: i+k >= k by NAT_1:11;
A6: k >= 1 by A1,A4,FINSEQ_1:1;
A7: k <= K by A1,A4,FINSEQ_1:1;
i+k >= 1 by A5,A6,XXREAL_0:2;
hence thesis by A3,A7,FINSEQ_1:1,XREAL_1:6;
end;
hence f is FinSubsequence-like by A2;
end;
end;
reserve i for Nat,
k,k1,k2,j1 for Element of NAT,
x,x1,x2,y for set;
theorem Th39:
for p being FinSequence
holds dom Shift(p,i) = {j1 where j1 is Nat: i+1 <= j1 & j1 <= i+(len p)}
proof
let p be FinSequence;
A1: dom p = Seg len p by FINSEQ_1:def 3
.= {k where k is Nat: 1 <= k & k <= len p};
set X = {j1 where j1 is Nat: i+1 <= j1 & j1 <= i+(len p)};
A2: dom Shift(p,i) = {k1+i where k1 is Nat: k1 in dom p} by Def12;
thus dom Shift(p,i) c= X
proof
let x be object;
assume x in dom Shift(p,i);
then consider k1 being Nat such that
A3: x = k1+i and
A4: k1 in dom p by A2;
consider k being Nat such that
A5: k1 = k and
A6: 1 <= k and
A7: k <= len p by A1,A4;
A8: i+1 <= i+k by A6,XREAL_1:7;
i+k <= i+(len p) by A7,XREAL_1:7;
hence thesis by A3,A5,A8;
end;
let x be object;
assume x in X;
then consider j1 being Nat such that
A9: x = j1 and
A10: i+1 <= j1 and
A11: j1 <= i+(len p);
i+(0 qua Nat) <= i+1 by XREAL_1:7;
then consider k2 being Nat such that
A12: j1 = i+k2 by A10,NAT_1:10,XXREAL_0:2;
A13: 1 <= k2 by A10,A12,XREAL_1:6;
k2 <= len p by A11,A12,XREAL_1:6;
then k2 in dom p by A1,A13;
hence thesis by A2,A9,A12;
end;
theorem Th40:
for q being FinSubsequence ex ss being FinSubsequence st
dom ss = dom q & rng ss = dom Shift(q,i) &
(for k st k in dom q holds ss.k = i+k) & ss is one-to-one
proof
let q be FinSubsequence;
consider n being Nat such that
A1: dom q c= Seg n by FINSEQ_1:def 12;
defpred P[object,object] means ex k st k = $1 & $2 = i+k;
A2: for x being object st x in dom q ex y being object st P[x,y]
proof
let x be object;
assume x in dom q;
then reconsider x as Element of NAT;
take i+x;
thus thesis;
end;
consider f being Function such that
A3: dom f = dom q and
A4: for x being object st x in dom q holds P[x, f.x] from CLASSES1:sch 1(A2);
reconsider ss = f as FinSubsequence by A1,A3,FINSEQ_1:def 12;
A5: dom Shift(q,i) = {k+i where k is Nat: k in dom q} by Def12;
A6: rng ss = dom Shift(q,i)
proof
thus rng ss c= dom Shift(q,i)
proof
let y be object;
assume y in rng ss;
then consider x being object such that
A7: x in dom ss and
A8: y = ss.x by FUNCT_1:def 3;
ex k1 st ( k1 = x)&( ss.x = i+k1) by A3,A4,A7;
hence thesis by A3,A5,A7,A8;
end;
let y be object;
assume y in dom Shift(q,i);
then consider k2 being Nat such that
A9: y = k2+i and
A10: k2 in dom q by A5;
ex k3 being Element of NAT st ( k3 = k2)&( ss.k2 = i+k3)
by A4,A10;
hence thesis by A3,A9,A10,FUNCT_1:def 3;
end;
A11: for k st k in dom q holds ss.k = i+k
proof
let k;
assume k in dom q;
then ex k1 st ( k1 = k)&( ss.k = i+k1) by A4;
hence thesis;
end;
for x1,x2 being object
st x1 in dom ss & x2 in dom ss & ss.x1 = ss.x2 holds x1 = x2
proof
let x1,x2 be object;
assume that
A12: x1 in dom ss and
A13: x2 in dom ss and
A14: ss.x1 = ss.x2;
A15: ex k1 st ( k1 = x1)&( ss.x1 = i+k1) by A3,A4,A12;
ex k2 st ( k2 = x2)&( ss.x2 = i+k2) by A3,A4,A13;
hence thesis by A14,A15;
end;
then ss is one-to-one;
hence thesis by A3,A6,A11;
end;
Lm5: for p being FinSequence holds ex fs being FinSequence st
dom fs = dom p & rng fs = dom Shift(p,i) &
(for k st k in dom p holds fs.k = i+k) & fs is one-to-one
proof
let p be FinSequence;
consider ss being FinSubsequence such that
A1: dom ss = dom p and
A2: rng ss = dom Shift(p,i) and
A3: for k st k in dom p holds ss.k = i+k and
A4: ss is one-to-one by Th40;
dom ss = Seg len p by A1,FINSEQ_1:def 3;
then reconsider fs = ss as FinSequence by FINSEQ_1:def 2;
dom fs = dom p by A1;
hence thesis by A2,A3,A4;
end;
theorem Th41:
for q being FinSubsequence holds card q = card Shift(q,i)
proof
let q be FinSubsequence;
ex ss being FinSubsequence st ( dom ss = dom q)&( rng ss =
dom Shift(q,i))&( for k st k in dom q holds ss.k = i+k)&( ss is one-to-one)
by Th40;
then
A1: dom q, dom Shift(q,i) are_equipotent;
A2: card dom q = card q by CARD_1:62;
card dom Shift(q,i) = card Shift(q,i) by CARD_1:62;
hence thesis by A1,A2,CARD_1:5;
end;
theorem Th42:
for p being FinSequence holds dom p = dom Seq Shift(p,i)
proof
let p be FinSequence;
A1: rng Sgm dom Shift(p,i) = dom Shift(p,i) by FINSEQ_1:50;
A2: dom p = Seg len p by FINSEQ_1:def 3;
A3: dom Sgm dom Shift(p,i) = Seg len Sgm dom Shift(p,i) by FINSEQ_1:def 3;
A4: len Sgm dom Shift(p,i) = card dom Shift(p,i) by FINSEQ_3:39;
card dom Shift(p,i) = card Shift(p,i) by CARD_1:62;
then card dom Shift(p,i) = len p by Th41;
hence thesis by A1,A2,A3,A4,RELAT_1:27;
end;
theorem Th43:
for p being FinSequence st k in dom p holds (Sgm dom Shift(p,i)).k = i + k
proof
let p be FinSequence;
assume
A1: k in dom p;
consider fs being FinSequence such that
A2: dom fs = dom p and
A3: rng fs = dom Shift(p,i) and
A4: for j st j in dom p holds fs.j = i+j
and fs is one-to-one by Lm5;
reconsider fs as FinSequence of NAT by A3,FINSEQ_1:def 4;
for n,m being Nat st 1 <= n & n < m & m <= len fs holds fs.n < fs.m
proof
let n,m be Nat;
assume that
A6: 1 <= n and
A7: n < m and
A8: m <= len fs;
set k1 = fs.n;
set k2 = fs.m;
reconsider n,m as Element of NAT by ORDINAL1:def 12;
A11: dom fs = Seg len fs by FINSEQ_1:def 3
.= {n1 where n1 is Nat: 1 <= n1 & n1 <= len fs};
n+1 <= m by A7,INT_1:7;
then n+1 <= len fs by A8,XXREAL_0:2;
then
A12: n <= (len fs) - 1 by XREAL_1:19;
(len fs) + (0 qua Nat) <= (len fs) + 1 by XREAL_1:7;
then (len fs) - 1 <= len fs by XREAL_1:20;
then n <= len fs by A12,XXREAL_0:2;
then
A13: n in dom p by A2,A6,A11;
1 <= m by A6,A7,XXREAL_0:2;
then
A14: m in dom p by A2,A8,A11;
A15: k1 = i+n by A4,A13;
k2 = i+m by A4,A14;
hence thesis by A7,A15,XREAL_1:8;
end;
then fs = Sgm dom Shift(p,i) by A3,FINSEQ_1:def 14;
hence thesis by A1,A4;
end;
theorem Th44:
for p being FinSequence st k in dom p holds (Seq Shift(p,i)).k = p.k
proof
let p be FinSequence;
assume
A1: k in dom p;
then
A2: k in dom Seq Shift(p,i) by Th42;
(Shift(p,i)*(Sgm dom Shift(p,i))).k
= Shift(p,i).((Sgm dom Shift(p,i)).k) by A2,FUNCT_1:12
.= Shift(p,i).(i+k) by A1,Th43;
hence thesis by A1,Def12;
end;
theorem
for p being FinSequence holds Seq Shift(p,i) = p
proof
let p be FinSequence;
A1: dom Seq Shift(p,i) = dom p by Th42;
for x being object holds
x in dom p implies (Seq Shift(p,i)).x = p.x by Th44;
hence thesis by A1;
end;
reserve p1,p2 for FinSequence;
Lm6: for j,k,l being Nat st
1 <= j & j <= l or l+1 <= j & j <= l+k holds 1 <= j & j <= l+k
proof
let j,k,l be Nat;
assume that
A1: 1 <= j & j <= l or l+1 <= j & j <= l+k;
per cases by A1;
suppose
A2: 1 <= j & j <= l;
l+(0 qua Nat) <= l+k by XREAL_1:7;
hence thesis by A2,XXREAL_0:2;
end;
suppose
A3: l+1 <= j & j <= l+k;
0 qua Nat+1 <= l+1 by XREAL_1:7;
hence thesis by A3,XXREAL_0:2;
end;
end;
theorem Th46:
dom (p1 \/ Shift(p2,len p1)) = Seg (len p1 + len p2)
proof
A1: dom (p1 \/ Shift(p2,len p1)) = dom p1 \/ dom (Shift(p2,len p1))
by XTUPLE_0:23;
A2: dom p1 = Seg len p1 by FINSEQ_1:def 3
.= {k where k is Nat: 1 <= k & k <= len p1};
A3: dom (Shift(p2,len p1))
= {k1 where k1 is Nat: len p1 + 1 <= k1 & k1 <= len p1 + len p2}
by Th39;
thus dom (p1 \/ Shift(p2,len p1)) c= Seg (len p1 + len p2)
proof
let x be object;
assume x in dom (p1 \/ (Shift(p2,len p1)));
then
A4: x in dom p1 or x in dom (Shift(p2,len p1)) by A1,XBOOLE_0:def 3;
then
A5: ex k3 being Nat st x = k3 & 1 <= k3 & k3 <=
len p1 or x = k3 & len p1 + 1 <= k3 & k3 <= len p1 + len p2 by A2,A3;
reconsider x as Nat by A4;
A6: 1 <= x by A5,Lm6;
x <= len p1 + len p2 by A5,Lm6;
hence thesis by A6;
end;
let x be object;
assume x in Seg (len p1 + len p2);
then consider j being Nat such that
A7: x = j and
A8: 1 <= j and
A9: j <= len p1 + len p2;
reconsider i0 = len p1 as Integer;
1 <= j & j <= i0 or i0 + 1 <= j & j <= i0 + len p2 by A8,A9,INT_1:7;
then x in dom p1 or x in dom Shift(p2,len p1) by A2,A3,A7;
hence thesis by A1,XBOOLE_0:def 3;
end;
theorem Th47:
for p1 being FinSequence, p2 being FinSubsequence st len p1 <= i holds
dom p1 misses dom Shift(p2,i)
proof
let p1 be FinSequence, p2 be FinSubsequence;
assume
A1: len p1 <= i;
A2: dom p1 = Seg len p1 by FINSEQ_1:def 3
.= {k where k is Nat: 1 <= k & k <= len p1};
A3: dom Shift(p2,i) = {k+i where k is Nat: k in dom p2} by Def12;
not ex x being object st x in dom p1 /\ dom Shift(p2,i)
proof
given x being object such that
A4: x in dom p1 /\ dom Shift(p2,i);
A5: x in dom p1 by A4,XBOOLE_0:def 4;
A6: x in dom Shift(p2,i) by A4,XBOOLE_0:def 4;
A7: ex k1 being Nat st ( x = k1)&( 1 <= k1)&( k1 <= len p1) by A2,A5;
consider k2 being Nat such that
A8: x = k2+i and
A9: k2 in dom p2 by A3,A6;
consider n being Nat such that
A10: dom p2 c= Seg n by FINSEQ_1:def 12;
A11: k2 in Seg n by A9,A10;
A12: ex m being Nat st k2 = m & 1 <= m & m <= n by A11;
reconsider x as Element of NAT by A4;
len p1 + k2 <= i+k2 by A1,XREAL_1:7;
then (len p1 + k2) - k2 < x - 0 by A8,A12,XREAL_1:15;
hence contradiction by A7;
end;
hence dom p1 /\ dom Shift(p2,i) = {} by XBOOLE_0:def 1;
end;
theorem
for p1,p2 being FinSequence holds p1^p2 = p1 \/ (Shift(p2,len p1))
proof
let p1,p2;
A1: dom (p1 \/ (Shift(p2,len p1))) = Seg (len p1 + len p2) by Th46;
dom p1 misses dom (Shift(p2,len p1)) by Th47;
then reconsider p = p1 \/ (Shift(p2,len p1)) as FinSequence by A1,
FINSEQ_1:def 2,GRFUNC_1:13;
A2: dom p = Seg (len p1 + len p2) by Th46;
A3: for k be Nat st k in dom p1 holds p.k = p1.k
proof
let k be Nat;
assume k in dom p1;
then [k,p1.k] in p1 by FUNCT_1:def 2;
then [k,p1.k] in p by XBOOLE_0:def 3;
hence thesis by FUNCT_1:1;
end;
for k be Nat st k in dom p2 holds p.(len p1 + k) = p2.k
proof
let k be Nat;
assume
A4: k in dom p2;
dom (Shift(p2,len p1)) = {j+len p1 where j is Nat: j in dom p2} by Def12;
then len p1 + k in dom (Shift(p2,len p1)) by A4;
then [len p1 + k, (Shift(p2,len p1)).(len p1 + k)] in
(Shift(p2,len p1)) by FUNCT_1:def 2;
then [len p1 + k, (Shift(p2,len p1)).(len p1 + k)] in p
by XBOOLE_0:def 3;
then p.(len p1 + k) = (Shift(p2,len p1)).(len p1 + k) by FUNCT_1:1;
hence thesis by A4,Def12;
end;
hence thesis by A2,A3,FINSEQ_1:def 7;
end;
theorem
for p1 being FinSequence, p2 being FinSubsequence st i >= len p1
holds p1 misses Shift(p2,i)
proof
let p1 be FinSequence, p2 be FinSubsequence;
assume i >= len p1;
then dom p1 misses dom Shift(p2,i) by Th47;
hence thesis by RELAT_1:179 ;
end;
theorem
for F being total NAT-defined Function, p be NAT-defined Function,
n be Element of NAT st Shift(p,n) c= F
for i being Element of NAT st i in dom p holds F.(n+i) = p.i
proof
let F be total NAT-defined Function, p be NAT-defined Function,
n be Element of NAT such that
A1: Shift(p,n) c= F;
let i be Element of NAT;
assume
A2: i in dom p;
then n+i in dom Shift(p,n) by Th24;
hence F.(n+i) = Shift(p,n).(n+i) by A1,GRFUNC_1:2
.= p.i by A2,Def12;
end;
theorem Th51:
for p,q being FinSubsequence st q c= p holds Shift(q,i) c= Shift(p,i)
proof
let p,q be FinSubsequence;
assume
A1: q c= p;
A2: dom Shift(q,i) = {k+i where k is Nat: k in dom q} by Def12;
A3: dom Shift(p,i) = {k+i where k is Nat: k in dom p} by Def12;
let x,y be object;
assume
A4: [x,y] in Shift(q,i);
then
A5: x in dom Shift(q,i) by FUNCT_1:1;
A6: y = Shift(q,i).x by A4,FUNCT_1:1;
consider k being Nat such that
A7: x = k+i and
A8: k in dom q by A2,A5;
A9: dom q c= dom p by A1,GRFUNC_1:2;
then
A10: x in dom Shift(p,i) by A3,A7,A8;
y = q.k by A6,A7,A8,Def12
.= p.k by A1,A8,GRFUNC_1:2
.= Shift(p,i).x by A7,A8,A9,Def12;
hence thesis by A10,FUNCT_1:1;
end;
theorem
for p1,p2 being FinSequence holds Shift(p2,len p1) c= p1^p2
proof
let p1,p2 be FinSequence;
A1: dom Shift(p2,len p1) = {k+len p1 where k is Nat: k in dom p2} by Def12;
A2: dom Shift(p2,len p1) =
{k where k is Nat: len p1 + 1 <= k & k <= len p1 + len p2}
by Th39;
A3: dom (p1^p2) = Seg (len p1 + len p2) by FINSEQ_1:def 7
.= {k where k is Nat: 1 <= k & k <= len p1 + len p2};
let x,y be object;
assume
A4: [x,y] in Shift(p2,len p1);
then
A5: x in dom Shift(p2,len p1) by FUNCT_1:1;
A6: y = Shift(p2,len p1).x by A4,FUNCT_1:1;
consider k being Nat such that
A7: x = k and
A8: len p1 + 1 <= k and
A9: k <= len p1 + len p2 by A2,A5;
1 <= len p1 + 1 by INT_1:6;
then 1 <= k by A8,XXREAL_0:2;
then
A10: x in dom (p1^p2) by A3,A7,A9;
consider j being Nat such that
A11: x = j+len p1 and
A12: j in dom p2 by A1,A5;
y = p2.j by A6,A11,A12,Def12
.= (p1^p2).x by A11,A12,FINSEQ_1:def 7;
hence thesis by A10,FUNCT_1:1;
end;
reserve q,q1,q2,q3,q4 for FinSubsequence,
p1,p2 for FinSequence;
theorem Th53:
dom q1 misses dom q2 implies dom Shift(q1,i) misses dom Shift(q2,i)
proof
assume
A1: dom q1 misses dom q2;
A2: dom Shift(q1,i) = {k+i where k is Nat: k in dom q1} by Def12;
A3: dom Shift(q2,i) = {k+i where k is Nat: k in dom q2} by Def12;
now
given x being object such that
A4: x in dom Shift(q1,i) /\ dom Shift(q2,i);
A5: x in dom Shift(q1,i) by A4,XBOOLE_0:def 4;
A6: x in dom Shift(q2,i) by A4,XBOOLE_0:def 4;
A7: ex k1 being Nat st ( x = k1+i)&( k1 in dom q1) by A2,A5;
consider k2 being Nat such that
A8: x = k2+i and
A9: k2 in dom q2 by A3,A6;
k2 in dom q1 /\ dom q2 by A7,A8,A9,XBOOLE_0:def 4;
hence contradiction by A1;
end;
hence dom Shift(q1,i) /\ dom Shift(q2,i) = {} by XBOOLE_0:def 1;
end;
theorem
for q,q1,q2 being FinSubsequence st q = q1 \/ q2 & q1 misses q2 holds
Shift(q1,i) \/ Shift(q2,i) = Shift(q,i)
proof
let q,q1,q2 be FinSubsequence such that
A1: q = q1 \/ q2 and
A2: q1 misses q2;
A3: dom Shift(q,i) = {k+i where k is Nat: k in dom q} by Def12;
A4: dom Shift(q1,i) = {k+i where k is Nat: k in dom q1} by Def12;
A5: dom Shift(q2,i) = {k+i where k is Nat: k in dom q2} by Def12;
A6: q1 c= q by A1,XBOOLE_1:7;
A7: q2 c= q by A1,XBOOLE_1:7;
A8: Shift(q1,i) c= Shift(q,i) by A1,Th51,XBOOLE_1:7;
A9: Shift(q2,i) c= Shift(q,i) by A1,Th51,XBOOLE_1:7;
dom q1 misses dom q2 by A2,A6,A7,FUNCT_1:112;
then dom Shift(q1,i) misses dom Shift(q2,i) by Th53;
then reconsider q3 = Shift(q1,i) \/ Shift(q2,i) as Function by GRFUNC_1:13;
let x,y be object;
thus [x,y] in Shift(q1,i) \/ Shift(q2,i) implies [x,y] in Shift(q,i)
proof
assume
A10: [x,y] in Shift(q1,i) \/ Shift(q2,i);
then x in dom q3 by FUNCT_1:1;
then
A11: x in dom Shift(q1,i) \/ dom Shift(q2,i) by XTUPLE_0:23;
A12: now
assume
A13: x in dom Shift(q1,i);
A14: dom Shift(q1,i) c= dom Shift(q,i) by A8,GRFUNC_1:2;
Shift(q1,i).x = Shift(q,i).x by A8,A13,GRFUNC_1:2;
then [x,Shift(q,i).x] in Shift(q1,i) by A13,FUNCT_1:def 2;
then [x,Shift(q,i).x] in q3 by XBOOLE_0:def 3;
hence x in dom Shift(q,i) & y = Shift(q,i).x by A10,A13,A14,FUNCT_1:def 1
;
end;
now
assume
A15: x in dom Shift(q2,i);
A16: dom Shift(q2,i) c= dom Shift(q,i) by A9,GRFUNC_1:2;
Shift(q2,i).x = Shift(q,i).x by A9,A15,GRFUNC_1:2;
then [x,Shift(q,i).x] in Shift(q2,i) by A15,FUNCT_1:def 2;
then [x,Shift(q,i).x] in q3 by XBOOLE_0:def 3;
hence x in dom Shift(q,i) & y = Shift(q,i).x by A10,A15,A16,FUNCT_1:def 1
;
end;
hence thesis by A11,A12,FUNCT_1:1,XBOOLE_0:def 3;
end;
assume
A17: [x,y] in Shift(q,i);
then
A18: x in dom Shift(q,i) by FUNCT_1:1;
A19: y = Shift(q,i).x by A17,FUNCT_1:1;
consider k being Nat such that
A20: x = k+i and
A21: k in dom q by A3,A18;
dom q = dom q1 \/ dom q2 by A1,XTUPLE_0:23;
then
A22: k in dom q1 or k in dom q2 by A21,XBOOLE_0:def 3;
then x in dom Shift(q1,i) or x in dom Shift(q2,i) by A4,A5,A20;
then x in dom Shift(q1,i) \/ dom Shift(q2,i) by XBOOLE_0:def 3;
then
A23: x in dom q3 by XTUPLE_0:23;
A24: now
assume
A25: x in dom Shift(q1,i);
then
A26: ex k1 being Nat st ( x = k1+i)&( k1 in dom q1) by A4;
thus y = q.k by A19,A20,A21,Def12
.= q1.k by A1,A20,A26,GRFUNC_1:15
.= Shift(q1,i).x by A20,A26,Def12
.= q3.x by A25,GRFUNC_1:15;
end;
now
assume
A27: x in dom Shift(q2,i);
then
A28: ex k2 being Nat st ( x = k2+i)&( k2 in dom q2) by A5;
thus y = q.k by A19,A20,A21,Def12
.= q2.k by A1,A20,A28,GRFUNC_1:15
.= Shift(q2,i).x by A20,A28,Def12
.= q3.x by A27,GRFUNC_1:15;
end;
hence thesis by A4,A5,A20,A22,A23,A24,FUNCT_1:1;
end;
theorem Th55:
for q being FinSubsequence holds dom Seq q = dom Seq Shift(q,i)
proof
let q be FinSubsequence;
A1: len Seq q = card q by FINSEQ_3:158;
A2: len Seq Shift(q,i) = card Shift(q,i) by FINSEQ_3:158;
thus dom Seq q = Seg len Seq q by FINSEQ_1:def 3
.= dom Seq Shift(q,i) by Th41,A1,A2,FINSEQ_1:def 3;
end;
reserve l1 for Nat,
j2 for Element of NAT;
theorem Th56:
for q being FinSubsequence st k in dom Seq q
ex j st j = (Sgm dom q).k & (Sgm dom Shift(q,i)).k = i + j
proof
let q be FinSubsequence such that
A1: k in dom Seq q;
consider ss being FinSubsequence such that
A2: dom ss = dom q and
A3: rng ss = dom Shift(q,i) and
A4: for l st l in dom q holds ss.l = i+l
and ss is one-to-one by Th40;
A5: rng Seq ss = dom Shift(q,i) by A3,FINSEQ_1:101;
A6: rng Sgm dom q = dom q by FINSEQ_1:50;
A7: dom Seq q = dom (q*Sgm dom q)
.= dom Sgm dom q by A6,RELAT_1:27;
A8: for l1 st l1 in dom Seq q
ex j1 st j1 = (Sgm dom q).l1 & (Seq ss).l1 = i+j1
proof
let l1 such that
A9: l1 in dom Seq q;
A10: (Sgm dom q).l1 in rng Sgm dom q by A7,A9,FUNCT_1:def 3;
then
A11: (Sgm dom q).l1 in dom q by FINSEQ_1:50;
reconsider j1 = (Sgm dom q).l1 as Element of NAT by A10;
(Seq ss).l1 = (ss*Sgm dom ss).l1
.= ss.j1 by A2,A7,A9,FUNCT_1:13
.= i+j1 by A4,A11;
hence thesis;
end;
A12: rng ss = rng Sgm dom Shift(q,i) by A3,FINSEQ_1:50;
rng Sgm dom Shift(q,i) c= NAT;
then rng Seq ss c= NAT by A12,FINSEQ_1:101;
then reconsider fs = Seq ss as FinSequence of NAT by FINSEQ_1:def 4;
A14: dom Seq ss = dom (ss*Sgm dom ss)
.= dom Sgm dom q by A2,A6,RELAT_1:27;
for n,m being Nat st 1 <= n & n < m & m <= len fs holds fs.n < fs.m
proof
let n,m be Nat;
assume that
A15: 1 <= n and
A16: n < m and
A17: m <= len fs;
set k1 = fs.n;
set k2 = fs.m;
reconsider n,m as Element of NAT by ORDINAL1:def 12;
A20: dom fs = Seg len fs by FINSEQ_1:def 3
.= {l3 where l3 is Nat: 1 <= l3 & l3 <= len fs};
n+1 <= m by A16,INT_1:7;
then n+1 <= len fs by A17,XXREAL_0:2;
then
A21: n <= (len fs) - 1 by XREAL_1:19;
(len fs) + (0 qua Nat) <= (len fs) + 1 by XREAL_1:7;
then (len fs) - 1 <= len fs by XREAL_1:20;
then n <= len fs by A21,XXREAL_0:2;
then
A22: n in dom Seq q by A7,A14,A15,A20;
1 <= m by A15,A16,XXREAL_0:2;
then
A23: m in dom Seq q by A7,A14,A17,A20;
consider j2 being Element of NAT such that
A24: j2 = (Sgm dom q).n and
A25: fs.n = i+j2 by A8,A22;
consider j3 being Element of NAT such that
A26: j3 = (Sgm dom q).m and
A27: fs.m = i+j3 by A8,A23;
dom Seq ss = Seg len fs by FINSEQ_1:def 3;
then len fs = len Sgm dom q by A14,FINSEQ_1:def 3;
then j2 < j3 by A15,A16,A17,A24,A26,FINSEQ_1:def 14;
hence thesis by A25,A27,XREAL_1:8;
end;
then fs = Sgm dom Shift(q,i) by A5,FINSEQ_1:def 14;
hence thesis by A1,A8;
end;
theorem Th57:
for q being FinSubsequence st
k in dom Seq q holds (Seq Shift(q,i)).k = (Seq q).k
proof
let q be FinSubsequence;
assume
A1: k in dom Seq q;
then consider j such that
A2: j = (Sgm dom q).k and
A3: (Sgm dom Shift(q,i)).k = i+j by Th56;
A4: rng Sgm dom q = dom q by FINSEQ_1:50;
A5: dom Seq q = dom Seq Shift(q,i) by Th55
.= dom (Shift(q,i)*(Sgm dom Shift(q,i)));
A6: dom Seq q = dom (q*Sgm dom q)
.= dom Sgm dom q by A4,RELAT_1:27;
then j in rng Sgm dom q by A1,A2,FUNCT_1:def 3;
then
A7: j in dom q by FINSEQ_1:50;
(Seq Shift(q,i)).k = (Shift(q,i)*(Sgm dom Shift(q,i))).k
.= Shift(q,i).((Sgm dom Shift(q,i)).k)
by A1,A5,FUNCT_1:12
.= q.j by A3,A7,Def12
.= (q*Sgm dom q).k by A1,A2,A6,FUNCT_1:13
.= (Seq q).k;
hence thesis;
end;
theorem
for q being FinSubsequence holds Seq q = Seq Shift(q,i)
proof
let q be FinSubsequence;
A1: dom Seq q = dom Seq Shift(q,i) by Th55;
for x being object holds
x in dom Seq q implies (Seq Shift(q,i)).x = (Seq q).x by Th57;
hence thesis by A1;
end;
theorem Th59:
for q being FinSubsequence st
dom q c= Seg k holds dom Shift(q,i) c= Seg (i+k)
proof
let q be FinSubsequence;
assume
A1: dom q c= Seg k;
A2: dom Shift(q,i) = {j+i where j is Nat: j in dom q} by Def12;
let x be object;
assume x in dom Shift(q,i);
then consider j1 being Nat such that
A3: x = j1+i and
A4: j1 in dom q by A2;
j1 in Seg k by A1,A4;
then
A5: ex j2 being Nat st ( j1 = j2)&( 1 <= j2)&( j2 <= k);
A6: 0 qua Nat+1 <= i+j1 by A5,XREAL_1:7;
i+j1 <= i+k by A5,XREAL_1:7;
hence thesis by A3,A6;
end;
theorem Th60:
for p being FinSequence, q1,q2 being FinSubsequence st q1 c= p
ex ss being FinSubsequence st ss = q1 \/ Shift(q2,len p)
proof
let p be FinSequence, q1,q2 be FinSubsequence;
assume q1 c= p;
then
A1: dom q1 c= dom p by GRFUNC_1:2;
dom p misses dom Shift(q2,len p) by Th47;
then reconsider ss = q1 \/ Shift(q2,len p) as Function by A1,GRFUNC_1:13
,XBOOLE_1:63;
A2: dom p = Seg len p by FINSEQ_1:def 3;
consider k be Nat such that
A3: dom q2 c= Seg k by FINSEQ_1:def 12;
k in NAT by ORDINAL1:def 12;
then
A4: dom Shift(q2,len p) c= Seg (len p + k) by A3,Th59;
len p + (0 qua Nat) <= len p + k by XREAL_1:7;
then Seg len p c= Seg (len p + k) by FINSEQ_1:5;
then dom q1 c= Seg (len p + k) by A1,A2;
then dom q1 \/ dom Shift(q2,len p) c= Seg (len p + k) by A4,XBOOLE_1:8;
then dom (q1 \/ Shift(q2,len p)) c= Seg (len p + k) by XTUPLE_0:23;
then reconsider ss as FinSubsequence by FINSEQ_1:def 12;
take ss;
thus thesis;
end;
Lm7: for p,q being FinSubsequence st q c= p holds
dom Shift(q,i) c= dom Shift(p,i)
proof
let p,q be FinSubsequence;
assume
A1: q c= p;
A2: dom Shift(q,i) = {k+i where k is Nat: k in dom q} by Def12;
A3: dom Shift(p,i) = {k+i where k is Nat: k in dom p} by Def12;
A4: dom q c= dom p by A1,GRFUNC_1:2;
let x be object;
assume x in dom Shift(q,i);
then ex k1 being Nat st ( x = k1+i)&( k1 in dom q) by A2;
hence thesis by A3,A4;
end;
Lm8: for p1,p2 being FinSequence, q1,q2 being FinSubsequence st
q1 c= p1 & q2 c= p2 holds Sgm (dom q1 \/ dom Shift(q2,len p1))
= (Sgm dom q1)^(Sgm dom Shift(q2,len p1))
proof
let p1,p2 be FinSequence, q1,q2 be FinSubsequence;
assume that
A1: q1 c= p1 and
A2: q2 c= p2;
for m,n being Nat
st m in dom q1 & n in dom Shift(q2,len p1) holds m < n
proof
let m,n be Nat such that
A5: m in dom q1 and
A6: n in dom Shift(q2,len p1);
A7: dom p1 = Seg len p1 by FINSEQ_1:def 3
.= {k where k is Nat: 1 <= k & k <= len p1};
A8: dom Shift(p2,len p1)
= {k where k is Nat : len p1 + 1 <= k & k <= len p1 + len p2}
by Th39;
A9: dom q1 c= dom p1 by A1,GRFUNC_1:2;
A10: dom Shift(q2,len p1) c= dom Shift(p2,len p1) by A2,Lm7;
A11: m in dom p1 by A5,A9;
A12: n in dom Shift(p2,len p1) by A6,A10;
consider k3 being Nat such that
A13: k3 = m
and 1 <= k3 and
A14: k3 <= len p1 by A7,A11;
consider k4 being Nat such that
A15: k4 = n and
A16: len p1 + 1 <= k4
and k4 <= len p1 + len p2 by A8,A12;
len p1 < len p1 + 1 by XREAL_1:29;
then k3 <= len p1 + 1 by A14,XXREAL_0:2;
then
A17: k3 <= k4 by A16,XXREAL_0:2;
k3 <> k4 by A5,A6,A9,A13,A15,Th47,XBOOLE_0:3;
hence thesis by A13,A15,A17,XXREAL_0:1;
end;
hence thesis by FINSEQ_3:42;
end;
theorem Th61:
for p1,p2 being FinSequence, q1,q2 being FinSubsequence st q1 c= p1 & q2 c= p2
ex ss being FinSubsequence st ss = q1 \/ Shift(q2,len p1) &
dom Seq ss = Seg (len Seq q1 + len Seq q2)
proof
let p1,p2 be FinSequence, q1,q2 be FinSubsequence;
assume that
A1: q1 c= p1 and
A2: q2 c= p2;
consider ss being FinSubsequence such that
A3: ss = q1 \/ Shift(q2,len p1) by A1,Th60;
A6: rng Sgm dom ss = dom ss by FINSEQ_1:50;
A7: dom Seq ss = dom Sgm dom ss by A6,RELAT_1:27
.= dom Sgm (dom q1 \/ dom Shift(q2,len p1)) by A3,XTUPLE_0:23
.= dom ((Sgm dom q1)^(Sgm dom Shift(q2,len p1))) by A1,A2,Lm8
.= Seg (len Sgm dom q1 + len Sgm dom Shift(q2,len p1))
by FINSEQ_1:def 7;
A8: len Sgm dom Shift(q2,len p1) = card dom Shift(q2,len p1) by FINSEQ_3:39;
A9: len Sgm dom q1 = card dom q1 by FINSEQ_3:39;
len Sgm dom Shift(q2,len p1) = card Shift(q2,len p1) by A8,CARD_1:62;
then
A10: len Sgm dom Shift(q2,len p1) = card q2 by Th41;
A11: len Sgm dom q1 = card q1 by A9,CARD_1:62;
A12: len Sgm dom Shift(q2,len p1) = len Seq q2 by A10,FINSEQ_3:158;
len Sgm dom q1 = len Seq q1 by A11,FINSEQ_3:158;
hence thesis by A3,A7,A12;
end;
theorem Th62:
for p1,p2 being FinSequence, q1,q2 being FinSubsequence st q1 c= p1 & q2 c= p2
ex ss being FinSubsequence st ss = q1 \/ Shift(q2,len p1) &
dom Seq ss = Seg (len Seq q1 + len Seq q2) &
Seq ss = Seq q1 \/ Shift(Seq q2,len Seq q1)
proof
let p1,p2 be FinSequence, q1,q2 be FinSubsequence;
assume that
A1: q1 c= p1 and
A2: q2 c= p2;
consider ss being FinSubsequence such that
A3: ss = q1 \/ Shift(q2,len p1) and
A4: dom Seq ss = Seg (len Seq q1 + len Seq q2) by A1,A2,Th61;
A5: dom Seq q1 = Seg len Seq q1 by FINSEQ_1:def 3
.= {k where k is Nat: 1 <= k & k <= len Seq q1};
A6: dom Shift(Seq q2,len Seq q1)
= {k where k is Nat: len Seq q1 + 1 <= k & k <= len Seq q1 + len Seq q2}
by Th39;
A7: Seg (len Seq q1 + len Seq q2)
= dom Seq q1 \/ dom Shift(Seq q2,len Seq q1)
proof
thus Seg (len Seq q1 + len Seq q2)
c= dom Seq q1 \/ dom Shift(Seq q2,len Seq q1)
proof
let x be object;
assume x in Seg (len Seq q1 + len Seq q2);
then consider k1 being Nat such that
A8: x = k1 and
A9: 1 <= k1 and
A10: k1 <= len Seq q1 + len Seq q2;
A11: 1 <= k1 & k1 <= len Seq q1 implies k1 in dom Seq q1 by A5;
len Seq q1 + 1 <= k1 & k1 <= len Seq q1 + len Seq q2 implies
k1 in dom Shift(Seq q2,len Seq q1) by A6;
hence thesis by A8,A9,A10,A11,INT_1:7,XBOOLE_0:def 3;
end;
let x be object;
assume
A12: x in dom Seq q1 \/ dom Shift(Seq q2,len Seq q1);
A13: now
assume x in dom Seq q1;
then consider k1 being Nat such that
A14: x = k1 and
A15: 1 <= k1 and
A16: k1 <= len Seq q1 by A5;
len Seq q1 + (0 qua Nat) <= len Seq q1 + len Seq q2 by XREAL_1:7;
then k1 <= len Seq q1 + len Seq q2 by A16,XXREAL_0:2;
hence thesis by A14,A15;
end;
now
assume x in dom Shift(Seq q2,len Seq q1);
then consider k2 being Nat such that
A17: x = k2 and
A18: len Seq q1 + 1 <= k2 and
A19: k2 <= len Seq q1 + len Seq q2 by A6;
0 qua Nat+1 <= len Seq q1 + 1 by XREAL_1:7;
then 1 <= k2 by A18,XXREAL_0:2;
hence thesis by A17,A19;
end;
hence thesis by A12,A13,XBOOLE_0:def 3;
end;
A20: dom Seq q1 \/ dom Shift(Seq q2,len Seq q1)
= dom (Seq q1 \/ Shift(Seq q2,len Seq q1)) by XTUPLE_0:23;
dom Seq q1 misses dom Shift(Seq q2,len Seq q1) by Th47;
then reconsider ss1 = Seq q1 \/ Shift(Seq q2,len Seq q1) as Function
by GRFUNC_1:13;
for x being object st x in dom Seq ss holds (Seq ss).x = ss1.x
proof
let x be object;
assume
A21: x in dom Seq ss;
A22: (Seq ss).x = (ss*Sgm dom ss).x
.= ss.((Sgm dom ss).x) by A21,FUNCT_1:12
.= ss.((Sgm (dom q1 \/ dom Shift(q2,len p1))).x) by A3,XTUPLE_0:23
.= ss.(((Sgm dom q1)^(Sgm dom Shift(q2,len p1))).x) by A1,A2,Lm8;
A23: now
assume
A24: x in dom Seq q1;
then
A25: x in dom Sgm dom q1 by FINSEQ_1:100;
then (Sgm dom q1).x in rng Sgm dom q1 by FUNCT_1:def 3;
then
A26: (Sgm dom q1).x in dom q1 by FINSEQ_1:50;
(Seq ss).x = ss.((Sgm dom q1).x) by A22,A25,FINSEQ_1:def 7
.= q1.((Sgm dom q1).x) by A3,A26,GRFUNC_1:15
.= (q1*Sgm dom q1).x by A25,FUNCT_1:13
.= (Seq q1).x;
hence thesis by A24,GRFUNC_1:15;
end;
now
assume
A27: x in dom Shift(Seq q2,len Seq q1);
dom Shift(Seq q2,len Seq q1)
= {j+len Seq q1 where j is Nat: j in dom Seq q2 }
by Def12;
then consider j being Nat such that
A28: x = j+len Seq q1 and
A29: j in dom Seq q2 by A27;
A30: ss1.x = Shift(Seq q2,len Seq q1).x by A27,GRFUNC_1:15
.= (Seq q2).j by A28,A29,Def12;
card dom q1 = len Sgm dom q1 by FINSEQ_3:39;
then
A33: card q1 = len Sgm dom q1 by CARD_1:62;
A34: len Seq q1 = card q1 by FINSEQ_3:158;
A35: dom Seq q2 = Seg len Seq q2 by FINSEQ_1:def 3;
card q2 = len Seq q2 by FINSEQ_3:158;
then
A36: card Shift(q2,len p1) = len Seq q2 by Th41;
then
A37: card dom Shift(q2,len p1) = len Seq q2 by CARD_1:62;
A38: card dom Shift(q2,len p1) = len Sgm dom Shift(q2,len p1)
by FINSEQ_3:39;
A39: len Sgm dom Shift(q2,len p1) = len Seq q2 by A37,FINSEQ_3:39;
A40: dom Seq q2 = dom Sgm dom Shift(q2,len p1) by A35,A36,A38,CARD_1:62
,FINSEQ_1:def 3;
A41: j in dom Sgm dom Shift(q2,len p1) by A29,A35,A39,FINSEQ_1:def 3;
(Sgm dom Shift(q2,len p1)).j in rng Sgm dom Shift(q2,len p1)
by A29,A40,FUNCT_1:def 3;
then
A42: (Sgm dom Shift(q2,len p1)).j in dom Shift(q2,len p1) by FINSEQ_1:50;
(Seq ss).x
= ss.((Sgm dom Shift(q2,len p1)).j) by A22,A28,A33,A34,A41,
FINSEQ_1:def 7
.= Shift(q2,len p1).((Sgm dom Shift(q2,len p1)).j)
by A3,A42,GRFUNC_1:15
.= (Shift(q2,len p1)*(Sgm dom Shift(q2,len p1))).j
by A29,A40,FUNCT_1:13
.= (Seq Shift(q2,len p1)).j
.= (Seq q2).j by A29,Th57;
hence thesis by A30;
end;
hence thesis by A4,A7,A21,A23,XBOOLE_0:def 3;
end;
then Seq ss = ss1 by A4,A7,A20;
hence thesis by A3,A4;
end;
theorem
for p1,p2 being FinSequence, q1,q2 being FinSubsequence st q1 c= p1 & q2 c= p2
ex ss being FinSubsequence st
ss = q1 \/ Shift(q2,len p1) & (Seq q1)^(Seq q2) = Seq ss
proof
let p1,p2 be FinSequence, q1,q2 be FinSubsequence;
assume that
A1: q1 c= p1 and
A2: q2 c= p2;
consider ss being FinSubsequence such that
A3: ss = q1 \/ Shift(q2,len p1) and
A4: dom Seq ss = Seg (len Seq q1 + len Seq q2) and
A5: Seq ss = Seq q1 \/ Shift(Seq q2,len Seq q1) by A1,A2,Th62;
A6: for j1 be Nat st j1 in dom Seq q1 holds (Seq ss).j1 = (Seq q1).j1
by A5,GRFUNC_1:15;
for j2 be Nat st j2 in dom Seq q2 holds (Seq ss).(len Seq q1 + j2) =
(Seq q2).j2
proof
let j2 be Nat;
assume
A7: j2 in dom Seq q2;
dom Shift(Seq q2,len Seq q1) =
{k+len Seq q1 where k is Nat: k in dom Seq q2} by Def12;
then len Seq q1 + j2 in dom Shift(Seq q2,len Seq q1) by A7;
hence (Seq ss).(len Seq q1 + j2)
= Shift(Seq q2,len Seq q1).(len Seq q1 + j2) by A5,GRFUNC_1:15
.= (Seq q2).j2 by A7,Def12;
end;
then Seq ss = (Seq q1)^(Seq q2) by A4,A6,FINSEQ_1:def 7;
hence thesis by A3;
end;
theorem
for F being non empty NAT-defined finite Function
holds card CutLastLoc F = card F -' 1
proof let F be non empty NAT-defined finite Function;
A1: card F >= 0+1 by NAT_1:13;
thus card CutLastLoc F = card F - 1 by Th37
.= card F -' 1 by A1,XREAL_1:233;
end;
theorem
for F,G being non empty NAT-defined finite Function
st dom F = dom G
holds LastLoc F = LastLoc G;
theorem
for f being non empty NAT-defined finite Function
holds Shift(f +~ (x,y),i) = Shift(f,i) +~ (x,y)
proof let f be non empty NAT-defined finite Function;
A1: dom f = dom(f +~ (x,y)) by FUNCT_4:99;
A2: dom(Shift(f,i) +~ (x,y))
= dom Shift(f,i) by FUNCT_4:99
.= { m+i where m is Nat:m in dom(f +~ (x,y)) } by A1,Def12;
for m being Nat st m in dom(f +~ (x,y))
holds (Shift(f,i) +~ (x,y)).(m+i) = (f +~ (x,y)).m
proof let m be Nat;
assume m in dom(f +~ (x,y));
then
A3: m+i in dom(Shift(f,i) +~ (x,y)) by A2;
then
A4: m+i in dom Shift(f,i) by FUNCT_4:99;
consider mm being Nat such that
A5: m+i = mm+i and
A6: mm in dom(f +~ (x,y)) by A2,A3;
m = mm by A5;
then m in dom(f +~ (x,y)) by A6;
then
A7: m in dom f by FUNCT_4:99;
then
A8: Shift(f,i).(m+i) = f.m by Def12;
per cases;
suppose
A9: Shift(f,i).(m+i) = x;
hence (Shift(f,i) +~ (x,y)).(m+i) = y by A4,FUNCT_4:106
.= (f +~ (x,y)).m by A7,FUNCT_4:106,A9,A8;
end;
suppose
A10: Shift(f,i).(m+i) <> x;
hence (Shift(f,i) +~ (x,y)).(m+i)
= Shift(f,i).(m+i) by FUNCT_4:105
.= (f +~ (x,y)).m by A10,A8,FUNCT_4:105;
end;
end;
hence Shift(f +~ (x,y),i) = Shift(f,i) +~ (x,y) by A2,Def12;
end;
theorem
for F, G being non empty NAT-defined finite Function st dom F c= dom G
holds LastLoc F <= LastLoc G by XXREAL_2:59;