:: VALUED_1 semantic presentation
begin
Lm1: for f being FinSequence
for h being Function st dom h = dom f holds
h is FinSequence
proof
let f be FinSequence; ::_thesis: for h being Function st dom h = dom f holds
h is FinSequence
let h be Function; ::_thesis: ( dom h = dom f implies h is FinSequence )
assume A1: dom h = dom f ; ::_thesis: h is FinSequence
h is FinSequence-like
proof
take len f ; :: according to FINSEQ_1:def_2 ::_thesis: dom h = Seg (len f)
thus dom h = Seg (len f) by A1, FINSEQ_1:def_3; ::_thesis: verum
end;
hence h is FinSequence ; ::_thesis: verum
end;
Lm2: for f, g being FinSequence
for h being Function st dom h = (dom f) /\ (dom g) holds
h is FinSequence
proof
let f, g be FinSequence; ::_thesis: for h being Function st dom h = (dom f) /\ (dom g) holds
h is FinSequence
let h be Function; ::_thesis: ( dom h = (dom f) /\ (dom g) implies h is FinSequence )
assume A1: dom h = (dom f) /\ (dom g) ; ::_thesis: h is FinSequence
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
percases ( n <= m or m <= n ) ;
supposeA4: n <= m ; ::_thesis: h is FinSequence-like
take n ; :: according to FINSEQ_1:def_2 ::_thesis: dom h = Seg n
thus dom h = Seg n by A1, A2, A3, A4, FINSEQ_1:7; ::_thesis: verum
end;
supposeA5: m <= n ; ::_thesis: h is FinSequence-like
take m ; :: according to FINSEQ_1:def_2 ::_thesis: dom h = Seg m
thus dom h = Seg m by A1, A2, A3, A5, FINSEQ_1:7; ::_thesis: verum
end;
end;
end;
hence h is FinSequence ; ::_thesis: verum
end;
registration
cluster Relation-like Function-like complex-valued FinSequence-like for set ;
existence
ex b1 being FinSequence st b1 is complex-valued
proof
take <*> COMPLEX ; ::_thesis: <*> COMPLEX is complex-valued
thus <*> COMPLEX is complex-valued ; ::_thesis: verum
end;
end;
registration
let r be rational number ;
cluster|.r.| -> rational ;
coherence
|.r.| is rational
proof
( |.r.| = - r or |.r.| = r ) by COMPLEX1:71;
hence |.r.| is rational ; ::_thesis: verum
end;
end;
definition
let f1, f2 be complex-valued Function;
deffunc H1( set ) -> set = (f1 . $1) + (f2 . $1);
set X = (dom f1) /\ (dom f2);
funcf1 + f2 -> Function means :Def1: :: VALUED_1:def 1
( dom it = (dom f1) /\ (dom f2) & ( for c being set st c in dom it holds
it . c = (f1 . c) + (f2 . c) ) );
existence
ex b1 being Function st
( dom b1 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b1 holds
b1 . c = (f1 . c) + (f2 . c) ) )
proof
ex f being Function st
( dom f = (dom f1) /\ (dom f2) & ( for x being set st x in (dom f1) /\ (dom f2) holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
hence ex b1 being Function st
( dom b1 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b1 holds
b1 . c = (f1 . c) + (f2 . c) ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function st dom b1 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b1 holds
b1 . c = (f1 . c) + (f2 . c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b2 holds
b2 . c = (f1 . c) + (f2 . c) ) holds
b1 = b2
proof
let f, g be Function; ::_thesis: ( dom f = (dom f1) /\ (dom f2) & ( for c being set st c in dom f holds
f . c = (f1 . c) + (f2 . c) ) & dom g = (dom f1) /\ (dom f2) & ( for c being set st c in dom g holds
g . c = (f1 . c) + (f2 . c) ) implies f = g )
assume that
A1: dom f = (dom f1) /\ (dom f2) and
A2: for c being set st c in dom f holds
f . c = H1(c) and
A3: dom g = (dom f1) /\ (dom f2) and
A4: for c being set st c in dom g holds
g . c = H1(c) ; ::_thesis: f = g
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume A5: x in dom f ; ::_thesis: f . x = g . x
hence f . x = H1(x) by A2
.= g . x by A1, A3, A4, A5 ;
::_thesis: verum
end;
hence f = g by A1, A3, FUNCT_1:2; ::_thesis: verum
end;
commutativity
for b1 being Function
for f1, f2 being complex-valued Function st dom b1 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b1 holds
b1 . c = (f1 . c) + (f2 . c) ) holds
( dom b1 = (dom f2) /\ (dom f1) & ( for c being set st c in dom b1 holds
b1 . c = (f2 . c) + (f1 . c) ) ) ;
end;
:: deftheorem Def1 defines + VALUED_1:def_1_:_
for f1, f2 being complex-valued Function
for b3 being Function holds
( b3 = f1 + f2 iff ( dom b3 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b3 holds
b3 . c = (f1 . c) + (f2 . c) ) ) );
registration
let f1, f2 be complex-valued Function;
clusterf1 + f2 -> complex-valued ;
coherence
f1 + f2 is complex-valued
proof
let x be set ; :: according to VALUED_0:def_7 ::_thesis: ( not x in dom (f1 + f2) or (f1 + f2) . x is complex )
assume x in dom (f1 + f2) ; ::_thesis: (f1 + f2) . x is complex
then (f1 + f2) . x = (f1 . x) + (f2 . x) by Def1;
hence (f1 + f2) . x is complex ; ::_thesis: verum
end;
end;
registration
let f1, f2 be real-valued Function;
clusterf1 + f2 -> real-valued ;
coherence
f1 + f2 is real-valued
proof
let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (f1 + f2) or (f1 + f2) . x is real )
assume x in dom (f1 + f2) ; ::_thesis: (f1 + f2) . x is real
then (f1 + f2) . x = (f1 . x) + (f2 . x) by Def1;
hence (f1 + f2) . x is real ; ::_thesis: verum
end;
end;
registration
let f1, f2 be RAT -valued Function;
clusterf1 + f2 -> RAT -valued ;
coherence
f1 + f2 is RAT -valued
proof
let y be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not y in rng (f1 + f2) or y in RAT )
assume y in rng (f1 + f2) ; ::_thesis: y in RAT
then consider x being set 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 y in RAT by A2, RAT_1:def_2; ::_thesis: verum
end;
end;
registration
let f1, f2 be INT -valued Function;
clusterf1 + f2 -> INT -valued ;
coherence
f1 + f2 is INT -valued
proof
let y be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not y in rng (f1 + f2) or y in INT )
assume y in rng (f1 + f2) ; ::_thesis: y in INT
then consider x being set 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 y in INT by A2, INT_1:def_2; ::_thesis: verum
end;
end;
registration
let f1, f2 be natural-valued Function;
clusterf1 + f2 -> natural-valued ;
coherence
f1 + f2 is natural-valued
proof
let x be set ; :: according to VALUED_0:def_12 ::_thesis: ( not x in dom (f1 + f2) or (f1 + f2) . x is natural )
assume x in dom (f1 + f2) ; ::_thesis: (f1 + f2) . x is natural
then (f1 + f2) . x = (f1 . x) + (f2 . x) by Def1;
hence (f1 + f2) . x is natural ; ::_thesis: verum
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;
:: original: +
redefine funcf1 + f2 -> PartFunc of C,COMPLEX;
coherence
f1 + f2 is PartFunc of C,COMPLEX
proof
( dom (f1 + f2) = (dom f1) /\ (dom f2) & rng (f1 + f2) c= COMPLEX ) by Def1, VALUED_0:def_1;
hence f1 + f2 is PartFunc of C,COMPLEX by RELSET_1:4; ::_thesis: verum
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;
:: original: +
redefine funcf1 + f2 -> PartFunc of C,REAL;
coherence
f1 + f2 is PartFunc of C,REAL
proof
( dom (f1 + f2) = (dom f1) /\ (dom f2) & rng (f1 + f2) c= REAL ) by Def1, VALUED_0:def_3;
hence f1 + f2 is PartFunc of C,REAL by RELSET_1:4; ::_thesis: verum
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;
:: original: +
redefine funcf1 + f2 -> PartFunc of C,RAT;
coherence
f1 + f2 is PartFunc of C,RAT
proof
( dom (f1 + f2) = (dom f1) /\ (dom f2) & rng (f1 + f2) c= RAT ) by Def1, RELAT_1:def_19;
hence f1 + f2 is PartFunc of C,RAT by RELSET_1:4; ::_thesis: verum
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;
:: original: +
redefine funcf1 + f2 -> PartFunc of C,INT;
coherence
f1 + f2 is PartFunc of C,INT
proof
( dom (f1 + f2) = (dom f1) /\ (dom f2) & rng (f1 + f2) c= INT ) by Def1, RELAT_1:def_19;
hence f1 + f2 is PartFunc of C,INT by RELSET_1:4; ::_thesis: verum
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;
:: original: +
redefine funcf1 + f2 -> PartFunc of C,NAT;
coherence
f1 + f2 is PartFunc of C,NAT
proof
( dom (f1 + f2) = (dom f1) /\ (dom f2) & rng (f1 + f2) c= NAT ) by Def1, VALUED_0:def_6;
hence f1 + f2 is PartFunc of C,NAT by RELSET_1:4; ::_thesis: verum
end;
end;
registration
let C be set ;
let D1, D2 be non empty complex-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
clusterf1 + f2 -> total for PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = f1 + f2 holds
b1 is total
proof
( dom f1 = C & dom f2 = C ) by FUNCT_2:def_1;
then dom (f1 + f2) = C /\ C by Def1
.= C ;
hence for b1 being PartFunc of C,COMPLEX st b1 = f1 + f2 holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D1, D2 be non empty real-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
clusterf1 + f2 -> total for PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = f1 + f2 holds
b1 is total
proof
( dom f1 = C & dom f2 = C ) by FUNCT_2:def_1;
then dom (f1 + f2) = C /\ C by Def1
.= C ;
hence for b1 being PartFunc of C,REAL st b1 = f1 + f2 holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D1, D2 be non empty rational-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
clusterf1 + f2 -> total for PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = f1 + f2 holds
b1 is total
proof
( dom f1 = C & dom f2 = C ) by FUNCT_2:def_1;
then dom (f1 + f2) = C /\ C by Def1
.= C ;
hence for b1 being PartFunc of C,RAT st b1 = f1 + f2 holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D1, D2 be non empty integer-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
clusterf1 + f2 -> total for PartFunc of C,INT;
coherence
for b1 being PartFunc of C,INT st b1 = f1 + f2 holds
b1 is total
proof
( dom f1 = C & dom f2 = C ) by FUNCT_2:def_1;
then dom (f1 + f2) = C /\ C by Def1
.= C ;
hence for b1 being PartFunc of C,INT st b1 = f1 + f2 holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D1, D2 be non empty natural-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
clusterf1 + f2 -> total for PartFunc of C,NAT;
coherence
for b1 being PartFunc of C,NAT st b1 = f1 + f2 holds
b1 is total
proof
( dom f1 = C & dom f2 = C ) by FUNCT_2:def_1;
then dom (f1 + f2) = C /\ C by Def1
.= C ;
hence for b1 being PartFunc of C,NAT st b1 = f1 + f2 holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
theorem :: VALUED_1:1
for C being set
for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for 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 ; ::_thesis: for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for f2 being Function of C,D2
for c being Element of C holds (f1 + f2) . c = (f1 . c) + (f2 . c)
let D1, D2 be non empty complex-membered set ; ::_thesis: for f1 being Function of C,D1
for f2 being Function of C,D2
for c being Element of C holds (f1 + f2) . c = (f1 . c) + (f2 . c)
let f1 be Function of C,D1; ::_thesis: for f2 being Function of C,D2
for c being Element of C holds (f1 + f2) . c = (f1 . c) + (f2 . c)
let f2 be Function of C,D2; ::_thesis: for c being Element of C holds (f1 + f2) . c = (f1 . c) + (f2 . c)
A1: dom (f1 + f2) = C by FUNCT_2:def_1;
let c be Element of C; ::_thesis: (f1 + f2) . c = (f1 . c) + (f2 . c)
percases ( not C is empty or C is empty ) ;
suppose not C is empty ; ::_thesis: (f1 + f2) . c = (f1 . c) + (f2 . c)
hence (f1 + f2) . c = (f1 . c) + (f2 . c) by A1, Def1; ::_thesis: verum
end;
supposeA2: C is empty ; ::_thesis: (f1 + f2) . c = (f1 . c) + (f2 . c)
then dom f1 = {} ;
then f1 . c = 0 by FUNCT_1:def_2;
hence (f1 + f2) . c = (f1 . c) + (f2 . c) by A2; ::_thesis: verum
end;
end;
end;
registration
let f1, f2 be complex-valued FinSequence;
clusterf1 + f2 -> FinSequence-like ;
coherence
f1 + f2 is FinSequence-like
proof
dom (f1 + f2) = (dom f1) /\ (dom f2) by Def1;
hence f1 + f2 is FinSequence-like by Lm2; ::_thesis: verum
end;
end;
begin
definition
let f be complex-valued Function;
let r be complex number ;
deffunc H1( set ) -> set = r + (f . $1);
funcr + f -> Function means :Def2: :: VALUED_1:def 2
( dom it = dom f & ( for c being set st c in dom it holds
it . c = r + (f . c) ) );
existence
ex b1 being Function st
( dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = r + (f . c) ) )
proof
ex g being Function st
( dom g = dom f & ( for x being set st x in dom f holds
g . x = H1(x) ) ) from FUNCT_1:sch_3();
hence ex b1 being Function st
( dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = r + (f . c) ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = r + (f . c) ) & dom b2 = dom f & ( for c being set st c in dom b2 holds
b2 . c = r + (f . c) ) holds
b1 = b2
proof
let h, g be Function; ::_thesis: ( dom h = dom f & ( for c being set st c in dom h holds
h . c = r + (f . c) ) & dom g = dom f & ( for c being set st c in dom g holds
g . c = r + (f . c) ) implies h = g )
assume that
A1: dom h = dom f and
A2: for c being set st c in dom h holds
h . c = H1(c) and
A3: dom g = dom f and
A4: for c being set st c in dom g holds
g . c = H1(c) ; ::_thesis: h = g
now__::_thesis:_for_x_being_set_st_x_in_dom_h_holds_
h_._x_=_g_._x
let x be set ; ::_thesis: ( x in dom h implies h . x = g . x )
assume A5: x in dom h ; ::_thesis: h . x = g . x
hence h . x = H1(x) by A2
.= g . x by A1, A3, A4, A5 ;
::_thesis: verum
end;
hence h = g by A1, A3, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines + VALUED_1:def_2_:_
for f being complex-valued Function
for r being complex number
for b3 being Function holds
( b3 = r + f iff ( dom b3 = dom f & ( for c being set st c in dom b3 holds
b3 . c = r + (f . c) ) ) );
notation
let f be complex-valued Function;
let r be complex number ;
synonym f + r for r + f;
end;
registration
let f be complex-valued Function;
let r be complex number ;
clusterr + f -> complex-valued ;
coherence
r + f is complex-valued
proof
let x be set ; :: according to VALUED_0:def_7 ::_thesis: ( not x in dom (r + f) or (r + f) . x is complex )
assume x in dom (r + f) ; ::_thesis: (r + f) . x is complex
then (r + f) . x = r + (f . x) by Def2;
hence (r + f) . x is complex ; ::_thesis: verum
end;
end;
registration
let f be real-valued Function;
let r be real number ;
clusterr + f -> real-valued ;
coherence
r + f is real-valued
proof
let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (r + f) or (r + f) . x is real )
assume x in dom (r + f) ; ::_thesis: (r + f) . x is real
then (r + f) . x = r + (f . x) by Def2;
hence (r + f) . x is real ; ::_thesis: verum
end;
end;
registration
let f be RAT -valued Function;
let r be rational number ;
clusterr + f -> RAT -valued ;
coherence
r + f is RAT -valued
proof
let y be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not y in rng (r + f) or y in RAT )
assume y in rng (r + f) ; ::_thesis: y in RAT
then consider x being set 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 y in RAT by A2, RAT_1:def_2; ::_thesis: verum
end;
end;
registration
let f be INT -valued Function;
let r be integer number ;
clusterr + f -> INT -valued ;
coherence
r + f is INT -valued
proof
let y be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not y in rng (r + f) or y in INT )
assume y in rng (r + f) ; ::_thesis: y in INT
then consider x being set 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 y in INT by A2, INT_1:def_2; ::_thesis: verum
end;
end;
registration
let f be natural-valued Function;
let r be Nat;
clusterr + f -> natural-valued ;
coherence
r + f is natural-valued
proof
let x be set ; :: according to VALUED_0:def_12 ::_thesis: ( not x in dom (r + f) or (r + f) . x is natural )
assume x in dom (r + f) ; ::_thesis: (r + f) . x is natural
then (r + f) . x = r + (f . x) by Def2;
hence (r + f) . x is natural ; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be complex-membered set ;
let f be PartFunc of C,D;
let r be complex number ;
:: original: +
redefine funcr + f -> PartFunc of C,COMPLEX;
coherence
r + f is PartFunc of C,COMPLEX
proof
( dom (r + f) = dom f & rng (r + f) c= COMPLEX ) by Def2, VALUED_0:def_1;
hence r + f is PartFunc of C,COMPLEX by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
let r be real number ;
:: original: +
redefine funcr + f -> PartFunc of C,REAL;
coherence
r + f is PartFunc of C,REAL
proof
( dom (r + f) = dom f & rng (r + f) c= REAL ) by Def2, VALUED_0:def_3;
hence r + f is PartFunc of C,REAL by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be rational-membered set ;
let f be PartFunc of C,D;
let r be rational number ;
:: original: +
redefine funcr + f -> PartFunc of C,RAT;
coherence
r + f is PartFunc of C,RAT
proof
( dom (r + f) = dom f & rng (r + f) c= RAT ) by Def2, RELAT_1:def_19;
hence r + f is PartFunc of C,RAT by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be integer-membered set ;
let f be PartFunc of C,D;
let r be integer number ;
:: original: +
redefine funcr + f -> PartFunc of C,INT;
coherence
r + f is PartFunc of C,INT
proof
( dom (r + f) = dom f & rng (r + f) c= INT ) by Def2, RELAT_1:def_19;
hence r + f is PartFunc of C,INT by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be natural-membered set ;
let f be PartFunc of C,D;
let r be Nat;
:: original: +
redefine funcr + f -> PartFunc of C,NAT;
coherence
r + f is PartFunc of C,NAT
proof
( dom (r + f) = dom f & rng (r + f) c= NAT ) by Def2, VALUED_0:def_6;
hence r + f is PartFunc of C,NAT by RELSET_1:4; ::_thesis: verum
end;
end;
registration
let C be set ;
let D be non empty complex-membered set ;
let f be Function of C,D;
let r be complex number ;
clusterr + f -> total for PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = r + f holds
b1 is total
proof
dom (r + f) = dom f by Def2
.= C by FUNCT_2:def_1 ;
hence for b1 being PartFunc of C,COMPLEX st b1 = r + f holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D be non empty real-membered set ;
let f be Function of C,D;
let r be real number ;
clusterr + f -> total for PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = r + f holds
b1 is total
proof
dom (r + f) = dom f by Def2
.= C by FUNCT_2:def_1 ;
hence for b1 being PartFunc of C,REAL st b1 = r + f holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D be non empty rational-membered set ;
let f be Function of C,D;
let r be rational number ;
clusterr + f -> total for PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = r + f holds
b1 is total
proof
dom (r + f) = dom f by Def2
.= C by FUNCT_2:def_1 ;
hence for b1 being PartFunc of C,RAT st b1 = r + f holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D be non empty integer-membered set ;
let f be Function of C,D;
let r be integer number ;
clusterr + f -> total for PartFunc of C,INT;
coherence
for b1 being PartFunc of C,INT st b1 = r + f holds
b1 is total
proof
dom (r + f) = dom f by Def2
.= C by FUNCT_2:def_1 ;
hence for b1 being PartFunc of C,INT st b1 = r + f holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D be non empty natural-membered set ;
let f be Function of C,D;
let r be Nat;
clusterr + f -> total for PartFunc of C,NAT;
coherence
for b1 being PartFunc of C,NAT st b1 = r + f holds
b1 is total
proof
dom (r + f) = dom f by Def2
.= C by FUNCT_2:def_1 ;
hence for b1 being PartFunc of C,NAT st b1 = r + f holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
theorem :: VALUED_1:2
for C being non empty set
for D being non empty complex-membered set
for f being Function of C,D
for r being complex number
for c being Element of C holds (r + f) . c = r + (f . c)
proof
let C be non empty set ; ::_thesis: for D being non empty complex-membered set
for f being Function of C,D
for r being complex number
for c being Element of C holds (r + f) . c = r + (f . c)
let D be non empty complex-membered set ; ::_thesis: for f being Function of C,D
for r being complex number
for c being Element of C holds (r + f) . c = r + (f . c)
let f be Function of C,D; ::_thesis: for r being complex number
for c being Element of C holds (r + f) . c = r + (f . c)
let r be complex number ; ::_thesis: for c being Element of C holds (r + f) . c = r + (f . c)
dom (r + f) = C by FUNCT_2:def_1;
hence for c being Element of C holds (r + f) . c = r + (f . c) by Def2; ::_thesis: verum
end;
registration
let f be complex-valued FinSequence;
let r be complex number ;
clusterr + f -> FinSequence-like ;
coherence
r + f is FinSequence-like
proof
dom (r + f) = dom f by Def2;
hence r + f is FinSequence-like by Lm1; ::_thesis: verum
end;
end;
begin
definition
let f be complex-valued Function;
let r be complex number ;
funcf - r -> Function equals :: VALUED_1:def 3
(- r) + f;
coherence
(- r) + f is Function ;
end;
:: deftheorem defines - VALUED_1:def_3_:_
for f being complex-valued Function
for r being complex number holds f - r = (- r) + f;
theorem :: VALUED_1:3
for f being complex-valued Function
for r being complex number holds
( dom (f - r) = dom f & ( for c being set st c in dom f holds
(f - r) . c = (f . c) - r ) )
proof
let f be complex-valued Function; ::_thesis: for r being complex number holds
( dom (f - r) = dom f & ( for c being set st c in dom f holds
(f - r) . c = (f . c) - r ) )
let r be complex number ; ::_thesis: ( dom (f - r) = dom f & ( for c being set st c in dom f holds
(f - r) . c = (f . c) - r ) )
dom (f - r) = dom f by Def2;
hence ( dom (f - r) = dom f & ( for c being set st c in dom f holds
(f - r) . c = (f . c) - r ) ) by Def2; ::_thesis: verum
end;
registration
let f be complex-valued Function;
let r be complex number ;
clusterf - r -> complex-valued ;
coherence
f - r is complex-valued ;
end;
registration
let f be real-valued Function;
let r be real number ;
clusterf - r -> real-valued ;
coherence
f - r is real-valued ;
end;
registration
let f be RAT -valued Function;
let r be rational number ;
clusterf - r -> RAT -valued ;
coherence
f - r is RAT -valued ;
end;
registration
let f be INT -valued Function;
let r be integer number ;
clusterf - r -> INT -valued ;
coherence
f - r is INT -valued ;
end;
definition
let C be set ;
let D be complex-membered set ;
let f be PartFunc of C,D;
let r be complex number ;
:: original: -
redefine funcf - r -> PartFunc of C,COMPLEX;
coherence
f - r is PartFunc of C,COMPLEX
proof
( dom (f - r) = dom f & rng (f - r) c= COMPLEX ) by Def2, VALUED_0:def_1;
hence f - r is PartFunc of C,COMPLEX by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
let r be real number ;
:: original: -
redefine funcf - r -> PartFunc of C,REAL;
coherence
f - r is PartFunc of C,REAL
proof
( dom (f - r) = dom f & rng (f - r) c= REAL ) by Def2, VALUED_0:def_3;
hence f - r is PartFunc of C,REAL by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be rational-membered set ;
let f be PartFunc of C,D;
let r be rational number ;
:: original: -
redefine funcf - r -> PartFunc of C,RAT;
coherence
f - r is PartFunc of C,RAT
proof
( dom (f - r) = dom f & rng (f - r) c= RAT ) by Def2, RELAT_1:def_19;
hence f - r is PartFunc of C,RAT by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be integer-membered set ;
let f be PartFunc of C,D;
let r be integer number ;
:: original: -
redefine funcf - r -> PartFunc of C,INT;
coherence
f - r is PartFunc of C,INT
proof
( dom (f - r) = dom f & rng (f - r) c= INT ) by Def2, RELAT_1:def_19;
hence f - r is PartFunc of C,INT by RELSET_1:4; ::_thesis: verum
end;
end;
registration
let C be set ;
let D be non empty complex-membered set ;
let f be Function of C,D;
let r be complex number ;
clusterf - r -> total for PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = f - r holds
b1 is total ;
end;
registration
let C be set ;
let D be non empty real-membered set ;
let f be Function of C,D;
let r be real number ;
clusterf - r -> total for PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = f - r holds
b1 is total ;
end;
registration
let C be set ;
let D be non empty rational-membered set ;
let f be Function of C,D;
let r be rational number ;
clusterf - r -> total for PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = f - r holds
b1 is total ;
end;
registration
let C be set ;
let D be non empty integer-membered set ;
let f be Function of C,D;
let r be integer number ;
clusterf - r -> total for PartFunc of C,INT;
coherence
for b1 being PartFunc of C,INT st b1 = f - r holds
b1 is total ;
end;
theorem :: VALUED_1:4
for C being non empty set
for D being non empty complex-membered set
for f being Function of C,D
for r being complex number
for c being Element of C holds (f - r) . c = (f . c) - r
proof
let C be non empty set ; ::_thesis: for D being non empty complex-membered set
for f being Function of C,D
for r being complex number
for c being Element of C holds (f - r) . c = (f . c) - r
let D be non empty complex-membered set ; ::_thesis: for f being Function of C,D
for r being complex number
for c being Element of C holds (f - r) . c = (f . c) - r
let f be Function of C,D; ::_thesis: for r being complex number
for c being Element of C holds (f - r) . c = (f . c) - r
let r be complex number ; ::_thesis: for c being Element of C holds (f - r) . c = (f . c) - r
dom (f - r) = C by FUNCT_2:def_1;
hence for c being Element of C holds (f - r) . c = (f . c) - r by Def2; ::_thesis: verum
end;
registration
let f be complex-valued FinSequence;
let r be complex number ;
clusterf - r -> FinSequence-like ;
coherence
f - r is FinSequence-like ;
end;
begin
definition
let f1, f2 be complex-valued Function;
deffunc H1( set ) -> set = (f1 . $1) * (f2 . $1);
set X = (dom f1) /\ (dom f2);
funcf1 (#) f2 -> Function means :Def4: :: VALUED_1:def 4
( dom it = (dom f1) /\ (dom f2) & ( for c being set st c in dom it holds
it . c = (f1 . c) * (f2 . c) ) );
existence
ex b1 being Function st
( dom b1 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b1 holds
b1 . c = (f1 . c) * (f2 . c) ) )
proof
ex f being Function st
( dom f = (dom f1) /\ (dom f2) & ( for x being set st x in (dom f1) /\ (dom f2) holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
hence ex b1 being Function st
( dom b1 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b1 holds
b1 . c = (f1 . c) * (f2 . c) ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function st dom b1 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b1 holds
b1 . c = (f1 . c) * (f2 . c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b2 holds
b2 . c = (f1 . c) * (f2 . c) ) holds
b1 = b2
proof
let f, g be Function; ::_thesis: ( dom f = (dom f1) /\ (dom f2) & ( for c being set st c in dom f holds
f . c = (f1 . c) * (f2 . c) ) & dom g = (dom f1) /\ (dom f2) & ( for c being set st c in dom g holds
g . c = (f1 . c) * (f2 . c) ) implies f = g )
assume that
A1: dom f = (dom f1) /\ (dom f2) and
A2: for c being set st c in dom f holds
f . c = H1(c) and
A3: dom g = (dom f1) /\ (dom f2) and
A4: for c being set st c in dom g holds
g . c = H1(c) ; ::_thesis: f = g
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume A5: x in dom f ; ::_thesis: f . x = g . x
hence f . x = H1(x) by A2
.= g . x by A1, A3, A4, A5 ;
::_thesis: verum
end;
hence f = g by A1, A3, FUNCT_1:2; ::_thesis: verum
end;
commutativity
for b1 being Function
for f1, f2 being complex-valued Function st dom b1 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b1 holds
b1 . c = (f1 . c) * (f2 . c) ) holds
( dom b1 = (dom f2) /\ (dom f1) & ( for c being set st c in dom b1 holds
b1 . c = (f2 . c) * (f1 . c) ) ) ;
end;
:: deftheorem Def4 defines (#) VALUED_1:def_4_:_
for f1, f2 being complex-valued Function
for b3 being Function holds
( b3 = f1 (#) f2 iff ( dom b3 = (dom f1) /\ (dom f2) & ( for c being set st c in dom b3 holds
b3 . c = (f1 . c) * (f2 . c) ) ) );
theorem :: VALUED_1:5
for f1, f2 being complex-valued Function
for c being set holds (f1 (#) f2) . c = (f1 . c) * (f2 . c)
proof
let f1, f2 be complex-valued Function; ::_thesis: for c being set holds (f1 (#) f2) . c = (f1 . c) * (f2 . c)
let c be set ; ::_thesis: (f1 (#) f2) . c = (f1 . c) * (f2 . c)
A1: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by Def4;
percases ( c in dom (f1 (#) f2) or not c in dom (f1 (#) f2) ) ;
suppose c in dom (f1 (#) f2) ; ::_thesis: (f1 (#) f2) . c = (f1 . c) * (f2 . c)
hence (f1 (#) f2) . c = (f1 . c) * (f2 . c) by Def4; ::_thesis: verum
end;
supposeA2: not c in dom (f1 (#) f2) ; ::_thesis: (f1 (#) f2) . c = (f1 . c) * (f2 . c)
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 (f1 (#) f2) . c = (f1 . c) * (f2 . c) by A2, FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
registration
let f1, f2 be complex-valued Function;
clusterf1 (#) f2 -> complex-valued ;
coherence
f1 (#) f2 is complex-valued
proof
let x be set ; :: according to VALUED_0:def_7 ::_thesis: ( not x in dom (f1 (#) f2) or (f1 (#) f2) . x is complex )
assume x in dom (f1 (#) f2) ; ::_thesis: (f1 (#) f2) . x is complex
then (f1 (#) f2) . x = (f1 . x) * (f2 . x) by Def4;
hence (f1 (#) f2) . x is complex ; ::_thesis: verum
end;
end;
registration
let f1, f2 be real-valued Function;
clusterf1 (#) f2 -> real-valued ;
coherence
f1 (#) f2 is real-valued
proof
let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (f1 (#) f2) or (f1 (#) f2) . x is real )
assume x in dom (f1 (#) f2) ; ::_thesis: (f1 (#) f2) . x is real
then (f1 (#) f2) . x = (f1 . x) * (f2 . x) by Def4;
hence (f1 (#) f2) . x is real ; ::_thesis: verum
end;
end;
registration
let f1, f2 be RAT -valued Function;
clusterf1 (#) f2 -> RAT -valued ;
coherence
f1 (#) f2 is RAT -valued
proof
let y be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not y in rng (f1 (#) f2) or y in RAT )
assume y in rng (f1 (#) f2) ; ::_thesis: y in RAT
then consider x being set 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 y in RAT by A2, RAT_1:def_2; ::_thesis: verum
end;
end;
registration
let f1, f2 be INT -valued Function;
clusterf1 (#) f2 -> INT -valued ;
coherence
f1 (#) f2 is INT -valued
proof
let y be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not y in rng (f1 (#) f2) or y in INT )
assume y in rng (f1 (#) f2) ; ::_thesis: y in INT
then consider x being set 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 y in INT by A2, INT_1:def_2; ::_thesis: verum
end;
end;
registration
let f1, f2 be natural-valued Function;
clusterf1 (#) f2 -> natural-valued ;
coherence
f1 (#) f2 is natural-valued
proof
let x be set ; :: according to VALUED_0:def_12 ::_thesis: ( not x in dom (f1 (#) f2) or (f1 (#) f2) . x is natural )
assume x in dom (f1 (#) f2) ; ::_thesis: (f1 (#) f2) . x is natural
then (f1 (#) f2) . x = (f1 . x) * (f2 . x) by Def4;
hence (f1 (#) f2) . x is natural ; ::_thesis: verum
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;
:: original: (#)
redefine funcf1 (#) f2 -> PartFunc of C,COMPLEX;
coherence
f1 (#) f2 is PartFunc of C,COMPLEX
proof
( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng (f1 (#) f2) c= COMPLEX ) by Def4, VALUED_0:def_1;
hence f1 (#) f2 is PartFunc of C,COMPLEX by RELSET_1:4; ::_thesis: verum
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;
:: original: (#)
redefine funcf1 (#) f2 -> PartFunc of C,REAL;
coherence
f1 (#) f2 is PartFunc of C,REAL
proof
( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng (f1 (#) f2) c= REAL ) by Def4, VALUED_0:def_3;
hence f1 (#) f2 is PartFunc of C,REAL by RELSET_1:4; ::_thesis: verum
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;
:: original: (#)
redefine funcf1 (#) f2 -> PartFunc of C,RAT;
coherence
f1 (#) f2 is PartFunc of C,RAT
proof
( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng (f1 (#) f2) c= RAT ) by Def4, RELAT_1:def_19;
hence f1 (#) f2 is PartFunc of C,RAT by RELSET_1:4; ::_thesis: verum
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;
:: original: (#)
redefine funcf1 (#) f2 -> PartFunc of C,INT;
coherence
f1 (#) f2 is PartFunc of C,INT
proof
( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng (f1 (#) f2) c= INT ) by Def4, RELAT_1:def_19;
hence f1 (#) f2 is PartFunc of C,INT by RELSET_1:4; ::_thesis: verum
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;
:: original: (#)
redefine funcf1 (#) f2 -> PartFunc of C,NAT;
coherence
f1 (#) f2 is PartFunc of C,NAT
proof
( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng (f1 (#) f2) c= NAT ) by Def4, VALUED_0:def_6;
hence f1 (#) f2 is PartFunc of C,NAT by RELSET_1:4; ::_thesis: verum
end;
end;
registration
let C be set ;
let D1, D2 be non empty complex-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
clusterf1 (#) f2 -> total for PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = f1 (#) f2 holds
b1 is total
proof
( dom f1 = C & dom f2 = C ) by FUNCT_2:def_1;
then dom (f1 (#) f2) = C /\ C by Def4
.= C ;
hence for b1 being PartFunc of C,COMPLEX st b1 = f1 (#) f2 holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D1, D2 be non empty real-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
clusterf1 (#) f2 -> total for PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = f1 (#) f2 holds
b1 is total
proof
( dom f1 = C & dom f2 = C ) by FUNCT_2:def_1;
then dom (f1 (#) f2) = C /\ C by Def4
.= C ;
hence for b1 being PartFunc of C,REAL st b1 = f1 (#) f2 holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D1, D2 be non empty rational-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
clusterf1 (#) f2 -> total for PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = f1 (#) f2 holds
b1 is total
proof
( dom f1 = C & dom f2 = C ) by FUNCT_2:def_1;
then dom (f1 (#) f2) = C /\ C by Def4
.= C ;
hence for b1 being PartFunc of C,RAT st b1 = f1 (#) f2 holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D1, D2 be non empty integer-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
clusterf1 (#) f2 -> total for PartFunc of C,INT;
coherence
for b1 being PartFunc of C,INT st b1 = f1 (#) f2 holds
b1 is total
proof
( dom f1 = C & dom f2 = C ) by FUNCT_2:def_1;
then dom (f1 (#) f2) = C /\ C by Def4
.= C ;
hence for b1 being PartFunc of C,INT st b1 = f1 (#) f2 holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D1, D2 be non empty natural-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
clusterf1 (#) f2 -> total for PartFunc of C,NAT;
coherence
for b1 being PartFunc of C,NAT st b1 = f1 (#) f2 holds
b1 is total
proof
( dom f1 = C & dom f2 = C ) by FUNCT_2:def_1;
then dom (f1 (#) f2) = C /\ C by Def4
.= C ;
hence for b1 being PartFunc of C,NAT st b1 = f1 (#) f2 holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let f1, f2 be complex-valued FinSequence;
clusterf1 (#) f2 -> FinSequence-like ;
coherence
f1 (#) f2 is FinSequence-like
proof
dom (f1 (#) f2) = (dom f1) /\ (dom f2) by Def4;
hence f1 (#) f2 is FinSequence-like by Lm2; ::_thesis: verum
end;
end;
begin
definition
let f be complex-valued Function;
let r be complex number ;
deffunc H1( set ) -> set = r * (f . $1);
funcr (#) f -> Function means :Def5: :: VALUED_1:def 5
( dom it = dom f & ( for c being set st c in dom it holds
it . c = r * (f . c) ) );
existence
ex b1 being Function st
( dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = r * (f . c) ) )
proof
ex g being Function st
( dom g = dom f & ( for x being set st x in dom f holds
g . x = H1(x) ) ) from FUNCT_1:sch_3();
hence ex b1 being Function st
( dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = r * (f . c) ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = r * (f . c) ) & dom b2 = dom f & ( for c being set st c in dom b2 holds
b2 . c = r * (f . c) ) holds
b1 = b2
proof
let h, g be Function; ::_thesis: ( dom h = dom f & ( for c being set st c in dom h holds
h . c = r * (f . c) ) & dom g = dom f & ( for c being set st c in dom g holds
g . c = r * (f . c) ) implies h = g )
assume that
A1: dom h = dom f and
A2: for c being set st c in dom h holds
h . c = H1(c) and
A3: dom g = dom f and
A4: for c being set st c in dom g holds
g . c = H1(c) ; ::_thesis: h = g
now__::_thesis:_for_x_being_set_st_x_in_dom_h_holds_
h_._x_=_g_._x
let x be set ; ::_thesis: ( x in dom h implies h . x = g . x )
assume A5: x in dom h ; ::_thesis: h . x = g . x
hence h . x = H1(x) by A2
.= g . x by A1, A3, A4, A5 ;
::_thesis: verum
end;
hence h = g by A1, A3, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines (#) VALUED_1:def_5_:_
for f being complex-valued Function
for r being complex number
for b3 being Function holds
( b3 = r (#) f iff ( dom b3 = dom f & ( for c being set st c in dom b3 holds
b3 . c = r * (f . c) ) ) );
notation
let f be complex-valued Function;
let r be complex number ;
synonym f (#) r for r (#) f;
end;
theorem Th6: :: VALUED_1:6
for f being complex-valued Function
for r being complex number
for c being set holds (r (#) f) . c = r * (f . c)
proof
let f be complex-valued Function; ::_thesis: for r being complex number
for c being set holds (r (#) f) . c = r * (f . c)
let r be complex number ; ::_thesis: for c being set holds (r (#) f) . c = r * (f . c)
let c be set ; ::_thesis: (r (#) f) . c = r * (f . c)
A1: dom f = dom (r (#) f) by Def5;
percases ( c in dom f or not c in dom f ) ;
suppose c in dom f ; ::_thesis: (r (#) f) . c = r * (f . c)
hence (r (#) f) . c = r * (f . c) by A1, Def5; ::_thesis: verum
end;
supposeA2: not c in dom f ; ::_thesis: (r (#) f) . c = r * (f . c)
hence (r (#) f) . c = r * 0 by A1, FUNCT_1:def_2
.= r * (f . c) by A2, FUNCT_1:def_2 ;
::_thesis: verum
end;
end;
end;
registration
let f be complex-valued Function;
let r be complex number ;
clusterr (#) f -> complex-valued ;
coherence
r (#) f is complex-valued
proof
let x be set ; :: according to VALUED_0:def_7 ::_thesis: ( not x in dom (r (#) f) or (r (#) f) . x is complex )
assume x in dom (r (#) f) ; ::_thesis: (r (#) f) . x is complex
then (r (#) f) . x = r * (f . x) by Def5;
hence (r (#) f) . x is complex ; ::_thesis: verum
end;
end;
registration
let f be real-valued Function;
let r be real number ;
clusterr (#) f -> real-valued ;
coherence
r (#) f is real-valued
proof
let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (r (#) f) or (r (#) f) . x is real )
assume x in dom (r (#) f) ; ::_thesis: (r (#) f) . x is real
then (r (#) f) . x = r * (f . x) by Def5;
hence (r (#) f) . x is real ; ::_thesis: verum
end;
end;
registration
let f be RAT -valued Function;
let r be rational number ;
clusterr (#) f -> RAT -valued ;
coherence
r (#) f is RAT -valued
proof
let y be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not y in rng (r (#) f) or y in RAT )
assume y in rng (r (#) f) ; ::_thesis: y in RAT
then consider x being set 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 y in RAT by A2, RAT_1:def_2; ::_thesis: verum
end;
end;
registration
let f be INT -valued Function;
let r be integer number ;
clusterr (#) f -> INT -valued ;
coherence
r (#) f is INT -valued
proof
let y be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not y in rng (r (#) f) or y in INT )
assume y in rng (r (#) f) ; ::_thesis: y in INT
then consider x being set 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 y in INT by A2, INT_1:def_2; ::_thesis: verum
end;
end;
registration
let f be natural-valued Function;
let r be Nat;
clusterr (#) f -> natural-valued ;
coherence
r (#) f is natural-valued
proof
let x be set ; :: according to VALUED_0:def_12 ::_thesis: ( not x in dom (r (#) f) or (r (#) f) . x is natural )
assume x in dom (r (#) f) ; ::_thesis: (r (#) f) . x is natural
then (r (#) f) . x = r * (f . x) by Def5;
hence (r (#) f) . x is natural ; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be complex-membered set ;
let f be PartFunc of C,D;
let r be complex number ;
:: original: (#)
redefine funcr (#) f -> PartFunc of C,COMPLEX;
coherence
r (#) f is PartFunc of C,COMPLEX
proof
( dom (r (#) f) = dom f & rng (r (#) f) c= COMPLEX ) by Def5, VALUED_0:def_1;
hence r (#) f is PartFunc of C,COMPLEX by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
let r be real number ;
:: original: (#)
redefine funcr (#) f -> PartFunc of C,REAL;
coherence
r (#) f is PartFunc of C,REAL
proof
( dom (r (#) f) = dom f & rng (r (#) f) c= REAL ) by Def5, VALUED_0:def_3;
hence r (#) f is PartFunc of C,REAL by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be rational-membered set ;
let f be PartFunc of C,D;
let r be rational number ;
:: original: (#)
redefine funcr (#) f -> PartFunc of C,RAT;
coherence
r (#) f is PartFunc of C,RAT
proof
( dom (r (#) f) = dom f & rng (r (#) f) c= RAT ) by Def5, RELAT_1:def_19;
hence r (#) f is PartFunc of C,RAT by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be integer-membered set ;
let f be PartFunc of C,D;
let r be integer number ;
:: original: (#)
redefine funcr (#) f -> PartFunc of C,INT;
coherence
r (#) f is PartFunc of C,INT
proof
( dom (r (#) f) = dom f & rng (r (#) f) c= INT ) by Def5, RELAT_1:def_19;
hence r (#) f is PartFunc of C,INT by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be natural-membered set ;
let f be PartFunc of C,D;
let r be Nat;
:: original: (#)
redefine funcr (#) f -> PartFunc of C,NAT;
coherence
r (#) f is PartFunc of C,NAT
proof
( dom (r (#) f) = dom f & rng (r (#) f) c= NAT ) by Def5, VALUED_0:def_6;
hence r (#) f is PartFunc of C,NAT by RELSET_1:4; ::_thesis: verum
end;
end;
registration
let C be set ;
let D be non empty complex-membered set ;
let f be Function of C,D;
let r be complex number ;
clusterr (#) f -> total for PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = r (#) f holds
b1 is total
proof
dom (r (#) f) = dom f by Def5
.= C by FUNCT_2:def_1 ;
hence for b1 being PartFunc of C,COMPLEX st b1 = r (#) f holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D be non empty real-membered set ;
let f be Function of C,D;
let r be real number ;
clusterr (#) f -> total for PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = r (#) f holds
b1 is total
proof
dom (r (#) f) = dom f by Def5
.= C by FUNCT_2:def_1 ;
hence for b1 being PartFunc of C,REAL st b1 = r (#) f holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D be non empty rational-membered set ;
let f be Function of C,D;
let r be rational number ;
clusterr (#) f -> total for PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = r (#) f holds
b1 is total
proof
dom (r (#) f) = dom f by Def5
.= C by FUNCT_2:def_1 ;
hence for b1 being PartFunc of C,RAT st b1 = r (#) f holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D be non empty integer-membered set ;
let f be Function of C,D;
let r be integer number ;
clusterr (#) f -> total for PartFunc of C,INT;
coherence
for b1 being PartFunc of C,INT st b1 = r (#) f holds
b1 is total
proof
dom (r (#) f) = dom f by Def5
.= C by FUNCT_2:def_1 ;
hence for b1 being PartFunc of C,INT st b1 = r (#) f holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D be non empty natural-membered set ;
let f be Function of C,D;
let r be Nat;
clusterr (#) f -> total for PartFunc of C,NAT;
coherence
for b1 being PartFunc of C,NAT st b1 = r (#) f holds
b1 is total
proof
dom (r (#) f) = dom f by Def5
.= C by FUNCT_2:def_1 ;
hence for b1 being PartFunc of C,NAT st b1 = r (#) f holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
theorem :: VALUED_1:7
for C being non empty set
for D being non empty complex-membered set
for f being Function of C,D
for r being complex number
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 ; ::_thesis: for D being non empty complex-membered set
for f being Function of C,D
for r being complex number
for g being Function of C,COMPLEX st ( for c being Element of C holds g . c = r * (f . c) ) holds
g = r (#) f
let D be non empty complex-membered set ; ::_thesis: for f being Function of C,D
for r being complex number
for g being Function of C,COMPLEX st ( for c being Element of C holds g . c = r * (f . c) ) holds
g = r (#) f
let f be Function of C,D; ::_thesis: for r being complex number
for g being Function of C,COMPLEX st ( for c being Element of C holds g . c = r * (f . c) ) holds
g = r (#) f
let r be complex number ; ::_thesis: for g being Function of C,COMPLEX st ( for c being Element of C holds g . c = r * (f . c) ) holds
g = r (#) f
let g be Function of C,COMPLEX; ::_thesis: ( ( for c being Element of C holds g . c = r * (f . c) ) implies g = r (#) f )
assume A1: for c being Element of C holds g . c = r * (f . c) ; ::_thesis: g = r (#) f
let x be Element of C; :: according to FUNCT_2:def_8 ::_thesis: g . x = (r (#) f) . x
thus g . x = r * (f . x) by A1
.= (r (#) f) . x by Th6 ; ::_thesis: verum
end;
registration
let f be complex-valued FinSequence;
let r be complex number ;
clusterr (#) f -> FinSequence-like ;
coherence
r (#) f is FinSequence-like
proof
dom (r (#) f) = dom f by Def5;
hence r (#) f is FinSequence-like by Lm1; ::_thesis: verum
end;
end;
begin
definition
let f be complex-valued Function;
func - f -> complex-valued Function equals :: VALUED_1:def 6
(- 1) (#) f;
coherence
(- 1) (#) f is complex-valued Function ;
involutiveness
for b1, b2 being complex-valued Function st b1 = (- 1) (#) b2 holds
b2 = (- 1) (#) b1
proof
let r, h be complex-valued Function; ::_thesis: ( r = (- 1) (#) h implies h = (- 1) (#) r )
assume A1: r = (- 1) (#) h ; ::_thesis: h = (- 1) (#) r
thus dom ((- 1) (#) r) = dom r by Def5
.= dom h by A1, Def5 ; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom h or h . b1 = ((- 1) (#) r) . b1 )
let c be set ; ::_thesis: ( not c in dom h or h . c = ((- 1) (#) r) . c )
assume c in dom h ; ::_thesis: h . c = ((- 1) (#) r) . c
reconsider a = (- 1) * (h . c) as complex number ;
thus h . c = (- 1) * a
.= (- 1) * (r . c) by A1, Th6
.= ((- 1) (#) r) . c by Th6 ; ::_thesis: verum
end;
end;
:: deftheorem defines - VALUED_1:def_6_:_
for f being complex-valued Function holds - f = (- 1) (#) f;
theorem Th8: :: VALUED_1:8
for f being complex-valued Function holds
( dom (- f) = dom f & ( for c being set holds (- f) . c = - (f . c) ) )
proof
let f be complex-valued Function; ::_thesis: ( dom (- f) = dom f & ( for c being set holds (- f) . c = - (f . c) ) )
thus A1: dom (- f) = dom f by Def5; ::_thesis: for c being set holds (- f) . c = - (f . c)
let c be set ; ::_thesis: (- f) . c = - (f . c)
percases ( c in dom f or not c in dom f ) ;
suppose c in dom f ; ::_thesis: (- f) . c = - (f . c)
hence (- f) . c = (- 1) * (f . c) by A1, Def5
.= - (f . c) ;
::_thesis: verum
end;
supposeA2: not c in dom f ; ::_thesis: (- f) . c = - (f . c)
hence (- f) . c = - 0 by A1, FUNCT_1:def_2
.= - (f . c) by A2, FUNCT_1:def_2 ;
::_thesis: verum
end;
end;
end;
theorem :: VALUED_1:9
for f being complex-valued Function
for g being Function st dom f = dom g & ( for c being set st c in dom f holds
g . c = - (f . c) ) holds
g = - f
proof
let f be complex-valued Function; ::_thesis: for g being Function st dom f = dom g & ( for c being set st c in dom f holds
g . c = - (f . c) ) holds
g = - f
let g be Function; ::_thesis: ( dom f = dom g & ( for c being set st c in dom f holds
g . c = - (f . c) ) implies g = - f )
assume that
A1: dom f = dom g and
A2: for c being set st c in dom f holds
g . c = - (f . c) ; ::_thesis: g = - f
thus dom (- f) = dom g by A1, Def5; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom g or g . b1 = (- f) . b1 )
let c be set ; ::_thesis: ( not c in dom g or g . c = (- f) . c )
assume A3: c in dom g ; ::_thesis: g . c = (- f) . c
thus (- f) . c = - (f . c) by Th8
.= g . c by A1, A2, A3 ; ::_thesis: verum
end;
registration
let f be complex-valued Function;
cluster - f -> complex-valued ;
coherence
- f is complex-valued ;
end;
registration
let f be real-valued Function;
cluster - f -> complex-valued real-valued ;
coherence
- f is real-valued ;
end;
registration
let f be RAT -valued Function;
cluster - f -> RAT -valued complex-valued ;
coherence
- f is RAT -valued ;
end;
registration
let f be INT -valued Function;
cluster - f -> INT -valued complex-valued ;
coherence
- f is INT -valued ;
end;
definition
let C be set ;
let D be complex-membered set ;
let f be PartFunc of C,D;
:: original: -
redefine func - f -> PartFunc of C,COMPLEX;
coherence
- f is PartFunc of C,COMPLEX
proof
( dom (- f) = dom f & rng (- f) c= COMPLEX ) by Def5, VALUED_0:def_1;
hence - f is PartFunc of C,COMPLEX by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
:: original: -
redefine func - f -> PartFunc of C,REAL;
coherence
- f is PartFunc of C,REAL
proof
( dom (- f) = dom f & rng (- f) c= REAL ) by Def5, VALUED_0:def_3;
hence - f is PartFunc of C,REAL by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be rational-membered set ;
let f be PartFunc of C,D;
:: original: -
redefine func - f -> PartFunc of C,RAT;
coherence
- f is PartFunc of C,RAT
proof
( dom (- f) = dom f & rng (- f) c= RAT ) by Def5, RELAT_1:def_19;
hence - f is PartFunc of C,RAT by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be integer-membered set ;
let f be PartFunc of C,D;
:: original: -
redefine func - f -> PartFunc of C,INT;
coherence
- f is PartFunc of C,INT
proof
( dom (- f) = dom f & rng (- f) c= INT ) by Def5, RELAT_1:def_19;
hence - f is PartFunc of C,INT by RELSET_1:4; ::_thesis: verum
end;
end;
registration
let C be set ;
let D be non empty complex-membered set ;
let f be Function of C,D;
cluster - f -> total for PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = - f holds
b1 is total ;
end;
registration
let C be set ;
let D be non empty real-membered set ;
let f be Function of C,D;
cluster - f -> total for PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = - f holds
b1 is total ;
end;
registration
let C be set ;
let D be non empty rational-membered set ;
let f be Function of C,D;
cluster - f -> total for PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = - f holds
b1 is total ;
end;
registration
let C be set ;
let D be non empty integer-membered set ;
let f be Function of C,D;
cluster - f -> total for PartFunc of C,INT;
coherence
for b1 being PartFunc of C,INT st b1 = - f holds
b1 is total ;
end;
registration
let f be complex-valued FinSequence;
cluster - f -> complex-valued FinSequence-like ;
coherence
- f is FinSequence-like ;
end;
begin
definition
let f be complex-valued Function;
deffunc H1( set ) -> set = (f . $1) " ;
funcf " -> complex-valued Function means :Def7: :: VALUED_1:def 7
( dom it = dom f & ( for c being set st c in dom it holds
it . c = (f . c) " ) );
existence
ex b1 being complex-valued Function st
( dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = (f . c) " ) )
proof
consider g being Function such that
A1: ( dom g = dom f & ( for x being set st x in dom f holds
g . x = H1(x) ) ) from FUNCT_1:sch_3();
g is complex-valued
proof
let x be set ; :: according to VALUED_0:def_7 ::_thesis: ( not x in dom g or g . x is complex )
assume x in dom g ; ::_thesis: g . x is complex
then g . x = (f . x) " by A1;
hence g . x is complex ; ::_thesis: verum
end;
hence ex b1 being complex-valued Function st
( dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = (f . c) " ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being complex-valued Function st dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = (f . c) " ) & dom b2 = dom f & ( for c being set st c in dom b2 holds
b2 . c = (f . c) " ) holds
b1 = b2
proof
let h, g be complex-valued Function; ::_thesis: ( dom h = dom f & ( for c being set st c in dom h holds
h . c = (f . c) " ) & dom g = dom f & ( for c being set st c in dom g holds
g . c = (f . c) " ) implies h = g )
assume that
A2: dom h = dom f and
A3: for c being set st c in dom h holds
h . c = H1(c) and
A4: dom g = dom f and
A5: for c being set st c in dom g holds
g . c = H1(c) ; ::_thesis: h = g
now__::_thesis:_for_x_being_set_st_x_in_dom_h_holds_
h_._x_=_g_._x
let x be set ; ::_thesis: ( x in dom h implies h . x = g . x )
assume A6: x in dom h ; ::_thesis: h . x = g . x
hence h . x = H1(x) by A3
.= g . x by A2, A4, A5, A6 ;
::_thesis: verum
end;
hence h = g by A2, A4, FUNCT_1:2; ::_thesis: verum
end;
involutiveness
for b1, b2 being complex-valued Function st dom b1 = dom b2 & ( for c being set st c in dom b1 holds
b1 . c = (b2 . c) " ) holds
( dom b2 = dom b1 & ( for c being set st c in dom b2 holds
b2 . c = (b1 . c) " ) )
proof
let r, h be complex-valued Function; ::_thesis: ( dom r = dom h & ( for c being set st c in dom r holds
r . c = (h . c) " ) implies ( dom h = dom r & ( for c being set st c in dom h holds
h . c = (r . c) " ) ) )
assume that
A7: dom r = dom h and
A8: for c being set st c in dom r holds
r . c = (h . c) " ; ::_thesis: ( dom h = dom r & ( for c being set st c in dom h holds
h . c = (r . c) " ) )
thus dom r = dom h by A7; ::_thesis: for c being set st c in dom h holds
h . c = (r . c) "
let c be set ; ::_thesis: ( c in dom h implies h . c = (r . c) " )
assume A9: c in dom h ; ::_thesis: h . c = (r . c) "
thus h . c = ((h . c) ") "
.= (r . c) " by A7, A8, A9 ; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines " VALUED_1:def_7_:_
for f, b2 being complex-valued Function holds
( b2 = f " iff ( dom b2 = dom f & ( for c being set st c in dom b2 holds
b2 . c = (f . c) " ) ) );
theorem Th10: :: VALUED_1:10
for f being complex-valued Function
for c being set holds (f ") . c = (f . c) "
proof
let f be complex-valued Function; ::_thesis: for c being set holds (f ") . c = (f . c) "
let c be set ; ::_thesis: (f ") . c = (f . c) "
A1: dom (f ") = dom f by Def7;
percases ( c in dom f or not c in dom f ) ;
suppose c in dom f ; ::_thesis: (f ") . c = (f . c) "
hence (f ") . c = (f . c) " by A1, Def7; ::_thesis: verum
end;
supposeA2: not c in dom f ; ::_thesis: (f ") . c = (f . c) "
hence (f ") . c = 0 " by A1, FUNCT_1:def_2
.= (f . c) " by A2, FUNCT_1:def_2 ;
::_thesis: verum
end;
end;
end;
registration
let f be real-valued Function;
clusterf " -> complex-valued real-valued ;
coherence
f " is real-valued
proof
let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (f ") or (f ") . x is real )
assume x in dom (f ") ; ::_thesis: (f ") . x is real
then (f ") . x = (f . x) " by Def7;
hence (f ") . x is real ; ::_thesis: verum
end;
end;
registration
let f be RAT -valued Function;
clusterf " -> RAT -valued complex-valued ;
coherence
f " is RAT -valued
proof
let y be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not y in rng (f ") or y in RAT )
assume y in rng (f ") ; ::_thesis: y in RAT
then consider x being set 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 y in RAT by A2, RAT_1:def_2; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be complex-membered set ;
let f be PartFunc of C,D;
:: original: "
redefine funcf " -> PartFunc of C,COMPLEX;
coherence
f " is PartFunc of C,COMPLEX
proof
( dom (f ") = dom f & rng (f ") c= COMPLEX ) by Def7, VALUED_0:def_1;
hence f " is PartFunc of C,COMPLEX by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
:: original: "
redefine funcf " -> PartFunc of C,REAL;
coherence
f " is PartFunc of C,REAL
proof
( dom (f ") = dom f & rng (f ") c= REAL ) by Def7, VALUED_0:def_3;
hence f " is PartFunc of C,REAL by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be rational-membered set ;
let f be PartFunc of C,D;
:: original: "
redefine funcf " -> PartFunc of C,RAT;
coherence
f " is PartFunc of C,RAT
proof
( dom (f ") = dom f & rng (f ") c= RAT ) by Def7, RELAT_1:def_19;
hence f " is PartFunc of C,RAT by RELSET_1:4; ::_thesis: verum
end;
end;
registration
let C be set ;
let D be non empty complex-membered set ;
let f be Function of C,D;
clusterf " -> total for PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = f " holds
b1 is total
proof
dom (f ") = dom f by Def7
.= C by FUNCT_2:def_1 ;
hence for b1 being PartFunc of C,COMPLEX st b1 = f " holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D be non empty real-membered set ;
let f be Function of C,D;
clusterf " -> total for PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = f " holds
b1 is total
proof
dom (f ") = dom f by Def7
.= C by FUNCT_2:def_1 ;
hence for b1 being PartFunc of C,REAL st b1 = f " holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D be non empty rational-membered set ;
let f be Function of C,D;
clusterf " -> total for PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = f " holds
b1 is total
proof
dom (f ") = dom f by Def7
.= C by FUNCT_2:def_1 ;
hence for b1 being PartFunc of C,RAT st b1 = f " holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let f be complex-valued FinSequence;
clusterf " -> complex-valued FinSequence-like ;
coherence
f " is FinSequence-like
proof
dom (f ") = dom f by Def7;
hence f " is FinSequence-like by Lm1; ::_thesis: verum
end;
end;
begin
definition
let f be complex-valued Function;
funcf ^2 -> Function equals :: VALUED_1:def 8
f (#) f;
coherence
f (#) f is Function ;
end;
:: deftheorem defines ^2 VALUED_1:def_8_:_
for f being complex-valued Function holds f ^2 = f (#) f;
theorem Th11: :: VALUED_1:11
for f being complex-valued Function holds
( dom (f ^2) = dom f & ( for c being set holds (f ^2) . c = (f . c) ^2 ) )
proof
let f be complex-valued Function; ::_thesis: ( dom (f ^2) = dom f & ( for c being set holds (f ^2) . c = (f . c) ^2 ) )
thus A1: dom (f ^2) = (dom f) /\ (dom f) by Def4
.= dom f ; ::_thesis: for c being set holds (f ^2) . c = (f . c) ^2
let c be set ; ::_thesis: (f ^2) . c = (f . c) ^2
percases ( c in dom f or not c in dom f ) ;
suppose c in dom f ; ::_thesis: (f ^2) . c = (f . c) ^2
hence (f ^2) . c = (f . c) ^2 by A1, Def4; ::_thesis: verum
end;
supposeA2: not c in dom f ; ::_thesis: (f ^2) . c = (f . c) ^2
hence (f ^2) . c = 0 ^2 by A1, FUNCT_1:def_2
.= (f . c) ^2 by A2, FUNCT_1:def_2 ;
::_thesis: verum
end;
end;
end;
registration
let f be complex-valued Function;
clusterf ^2 -> complex-valued ;
coherence
f ^2 is complex-valued ;
end;
registration
let f be real-valued Function;
clusterf ^2 -> real-valued ;
coherence
f ^2 is real-valued ;
end;
registration
let f be RAT -valued Function;
clusterf ^2 -> RAT -valued ;
coherence
f ^2 is RAT -valued ;
end;
registration
let f be INT -valued Function;
clusterf ^2 -> INT -valued ;
coherence
f ^2 is INT -valued ;
end;
registration
let f be natural-valued Function;
clusterf ^2 -> natural-valued ;
coherence
f ^2 is natural-valued ;
end;
definition
let C be set ;
let D be complex-membered set ;
let f be PartFunc of C,D;
:: original: ^2
redefine funcf ^2 -> PartFunc of C,COMPLEX;
coherence
f ^2 is PartFunc of C,COMPLEX
proof
( dom (f ^2) = dom f & rng (f ^2) c= COMPLEX ) by Th11, VALUED_0:def_1;
hence f ^2 is PartFunc of C,COMPLEX by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
:: original: ^2
redefine funcf ^2 -> PartFunc of C,REAL;
coherence
f ^2 is PartFunc of C,REAL
proof
( dom (f ^2) = dom f & rng (f ^2) c= REAL ) by Th11, VALUED_0:def_3;
hence f ^2 is PartFunc of C,REAL by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be rational-membered set ;
let f be PartFunc of C,D;
:: original: ^2
redefine funcf ^2 -> PartFunc of C,RAT;
coherence
f ^2 is PartFunc of C,RAT
proof
( dom (f ^2) = dom f & rng (f ^2) c= RAT ) by Th11, RELAT_1:def_19;
hence f ^2 is PartFunc of C,RAT by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be integer-membered set ;
let f be PartFunc of C,D;
:: original: ^2
redefine funcf ^2 -> PartFunc of C,INT;
coherence
f ^2 is PartFunc of C,INT
proof
( dom (f ^2) = dom f & rng (f ^2) c= INT ) by Th11, RELAT_1:def_19;
hence f ^2 is PartFunc of C,INT by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be natural-membered set ;
let f be PartFunc of C,D;
:: original: ^2
redefine funcf ^2 -> PartFunc of C,NAT;
coherence
f ^2 is PartFunc of C,NAT
proof
( dom (f ^2) = dom f & rng (f ^2) c= NAT ) by Th11, VALUED_0:def_6;
hence f ^2 is PartFunc of C,NAT by RELSET_1:4; ::_thesis: verum
end;
end;
registration
let C be set ;
let D be non empty complex-membered set ;
let f be Function of C,D;
clusterf ^2 -> total for PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = f ^2 holds
b1 is total ;
end;
registration
let C be set ;
let D be non empty real-membered set ;
let f be Function of C,D;
clusterf ^2 -> total for PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = f ^2 holds
b1 is total ;
end;
registration
let C be set ;
let D be non empty rational-membered set ;
let f be Function of C,D;
clusterf ^2 -> total for PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = f ^2 holds
b1 is total ;
end;
registration
let C be set ;
let D be non empty integer-membered set ;
let f be Function of C,D;
clusterf ^2 -> total for PartFunc of C,INT;
coherence
for b1 being PartFunc of C,INT st b1 = f ^2 holds
b1 is total ;
end;
registration
let C be set ;
let D be non empty natural-membered set ;
let f be Function of C,D;
clusterf ^2 -> total for PartFunc of C,NAT;
coherence
for b1 being PartFunc of C,NAT st b1 = f ^2 holds
b1 is total ;
end;
registration
let f be complex-valued FinSequence;
clusterf ^2 -> FinSequence-like ;
coherence
f ^2 is FinSequence-like ;
end;
begin
definition
let f1, f2 be complex-valued Function;
funcf1 - f2 -> Function equals :: VALUED_1:def 9
f1 + (- f2);
coherence
f1 + (- f2) is Function ;
end;
:: deftheorem defines - VALUED_1:def_9_:_
for f1, f2 being complex-valued Function holds f1 - f2 = f1 + (- f2);
registration
let f1, f2 be complex-valued Function;
clusterf1 - f2 -> complex-valued ;
coherence
f1 - f2 is complex-valued ;
end;
registration
let f1, f2 be real-valued Function;
clusterf1 - f2 -> real-valued ;
coherence
f1 - f2 is real-valued ;
end;
registration
let f1, f2 be RAT -valued Function;
clusterf1 - f2 -> RAT -valued ;
coherence
f1 - f2 is RAT -valued ;
end;
registration
let f1, f2 be INT -valued Function;
clusterf1 - f2 -> INT -valued ;
coherence
f1 - f2 is INT -valued ;
end;
theorem Th12: :: VALUED_1:12
for f1, f2 being complex-valued Function holds dom (f1 - f2) = (dom f1) /\ (dom f2)
proof
let f1, f2 be complex-valued Function; ::_thesis: dom (f1 - f2) = (dom f1) /\ (dom f2)
thus dom (f1 - f2) = (dom f1) /\ (dom (- f2)) by Def1
.= (dom f1) /\ (dom f2) by Def5 ; ::_thesis: verum
end;
theorem :: VALUED_1:13
for f1, f2 being complex-valued Function
for c being set st c in dom (f1 - f2) holds
(f1 - f2) . c = (f1 . c) - (f2 . c)
proof
let f1, f2 be complex-valued Function; ::_thesis: for c being set st c in dom (f1 - f2) holds
(f1 - f2) . c = (f1 . c) - (f2 . c)
let c be set ; ::_thesis: ( c in dom (f1 - f2) implies (f1 - f2) . c = (f1 . c) - (f2 . c) )
assume c in dom (f1 - f2) ; ::_thesis: (f1 - f2) . c = (f1 . c) - (f2 . c)
hence (f1 - f2) . c = (f1 . c) + ((- f2) . c) by Def1
.= (f1 . c) - (f2 . c) by Th8 ;
::_thesis: verum
end;
theorem :: VALUED_1:14
for f1, f2 being complex-valued Function
for f being Function st dom f = dom (f1 - f2) & ( for c being set st c in dom f holds
f . c = (f1 . c) - (f2 . c) ) holds
f = f1 - f2
proof
let f1, f2 be complex-valued Function; ::_thesis: for f being Function st dom f = dom (f1 - f2) & ( for c being set st c in dom f holds
f . c = (f1 . c) - (f2 . c) ) holds
f = f1 - f2
let f be Function; ::_thesis: ( dom f = dom (f1 - f2) & ( for c being set st c in dom f holds
f . c = (f1 . c) - (f2 . c) ) implies f = f1 - f2 )
assume that
A1: dom f = dom (f1 - f2) and
A2: for c being set st c in dom f holds
f . c = (f1 . c) - (f2 . c) ; ::_thesis: f = f1 - f2
thus dom f = dom (f1 - f2) by A1; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in dom f or f . b1 = (f1 - f2) . b1 )
let c be set ; ::_thesis: ( not c in dom f or f . c = (f1 - f2) . c )
assume A3: c in dom f ; ::_thesis: f . c = (f1 - f2) . c
hence f . c = (f1 . c) - (f2 . c) by A2
.= (f1 . c) + ((- f2) . c) by Th8
.= (f1 - f2) . c by A1, A3, Def1 ;
::_thesis: verum
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;
:: original: -
redefine funcf1 - f2 -> PartFunc of C,COMPLEX;
coherence
f1 - f2 is PartFunc of C,COMPLEX
proof
( dom (f1 - f2) = (dom f1) /\ (dom f2) & rng (f1 - f2) c= COMPLEX ) by Th12, VALUED_0:def_1;
hence f1 - f2 is PartFunc of C,COMPLEX by RELSET_1:4; ::_thesis: verum
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;
:: original: -
redefine funcf1 - f2 -> PartFunc of C,REAL;
coherence
f1 - f2 is PartFunc of C,REAL
proof
( dom (f1 - f2) = (dom f1) /\ (dom f2) & rng (f1 - f2) c= REAL ) by Th12, VALUED_0:def_3;
hence f1 - f2 is PartFunc of C,REAL by RELSET_1:4; ::_thesis: verum
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;
:: original: -
redefine funcf1 - f2 -> PartFunc of C,RAT;
coherence
f1 - f2 is PartFunc of C,RAT
proof
( dom (f1 - f2) = (dom f1) /\ (dom f2) & rng (f1 - f2) c= RAT ) by Th12, RELAT_1:def_19;
hence f1 - f2 is PartFunc of C,RAT by RELSET_1:4; ::_thesis: verum
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;
:: original: -
redefine funcf1 - f2 -> PartFunc of C,INT;
coherence
f1 - f2 is PartFunc of C,INT
proof
( dom (f1 - f2) = (dom f1) /\ (dom f2) & rng (f1 - f2) c= INT ) by Th12, RELAT_1:def_19;
hence f1 - f2 is PartFunc of C,INT by RELSET_1:4; ::_thesis: verum
end;
end;
Lm3: for C being set
for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for f2 being Function of C,D2 holds dom (f1 - f2) = C
proof
let C be set ; ::_thesis: for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for f2 being Function of C,D2 holds dom (f1 - f2) = C
let D1, D2 be non empty complex-membered set ; ::_thesis: for f1 being Function of C,D1
for f2 being Function of C,D2 holds dom (f1 - f2) = C
let f1 be Function of C,D1; ::_thesis: for f2 being Function of C,D2 holds dom (f1 - f2) = C
let f2 be Function of C,D2; ::_thesis: dom (f1 - f2) = C
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 ; ::_thesis: verum
end;
registration
let C be set ;
let D1, D2 be non empty complex-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
clusterf1 - f2 -> total for PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = f1 - f2 holds
b1 is total
proof
dom (f1 - f2) = C by Lm3;
hence for b1 being PartFunc of C,COMPLEX st b1 = f1 - f2 holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D1, D2 be non empty real-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
clusterf1 - f2 -> total for PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = f1 - f2 holds
b1 is total
proof
dom (f1 - f2) = C by Lm3;
hence for b1 being PartFunc of C,REAL st b1 = f1 - f2 holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D1, D2 be non empty rational-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
clusterf1 - f2 -> total for PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = f1 - f2 holds
b1 is total
proof
dom (f1 - f2) = C by Lm3;
hence for b1 being PartFunc of C,RAT st b1 = f1 - f2 holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D1, D2 be non empty integer-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
clusterf1 - f2 -> total for PartFunc of C,INT;
coherence
for b1 being PartFunc of C,INT st b1 = f1 - f2 holds
b1 is total
proof
dom (f1 - f2) = C by Lm3;
hence for b1 being PartFunc of C,INT st b1 = f1 - f2 holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
theorem :: VALUED_1:15
for C being set
for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for 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 ; ::_thesis: for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for f2 being Function of C,D2
for c being Element of C holds (f1 - f2) . c = (f1 . c) - (f2 . c)
let D1, D2 be non empty complex-membered set ; ::_thesis: for f1 being Function of C,D1
for f2 being Function of C,D2
for c being Element of C holds (f1 - f2) . c = (f1 . c) - (f2 . c)
let f1 be Function of C,D1; ::_thesis: for f2 being Function of C,D2
for c being Element of C holds (f1 - f2) . c = (f1 . c) - (f2 . c)
let f2 be Function of C,D2; ::_thesis: for c being Element of C holds (f1 - f2) . c = (f1 . c) - (f2 . c)
let c be Element of C; ::_thesis: (f1 - f2) . c = (f1 . c) - (f2 . c)
A1: dom (f1 - f2) = C by FUNCT_2:def_1;
percases ( not C is empty or C is empty ) ;
suppose not C is empty ; ::_thesis: (f1 - f2) . c = (f1 . c) - (f2 . c)
hence (f1 - f2) . c = (f1 . c) + ((- f2) . c) by A1, Def1
.= (f1 . c) - (f2 . c) by Th8 ;
::_thesis: verum
end;
supposeA2: C is empty ; ::_thesis: (f1 - f2) . c = (f1 . c) - (f2 . c)
then dom f2 = {} ;
then f2 . c = 0 by FUNCT_1:def_2;
hence (f1 - f2) . c = (f1 . c) - (f2 . c) by A2; ::_thesis: verum
end;
end;
end;
registration
let f1, f2 be complex-valued FinSequence;
clusterf1 - f2 -> FinSequence-like ;
coherence
f1 - f2 is FinSequence-like ;
end;
begin
definition
let f1, f2 be complex-valued Function;
funcf1 /" f2 -> Function equals :: VALUED_1:def 10
f1 (#) (f2 ");
coherence
f1 (#) (f2 ") is Function ;
end;
:: deftheorem defines /" VALUED_1:def_10_:_
for f1, f2 being complex-valued Function holds f1 /" f2 = f1 (#) (f2 ");
theorem Th16: :: VALUED_1:16
for f1, f2 being complex-valued Function holds dom (f1 /" f2) = (dom f1) /\ (dom f2)
proof
let f1, f2 be complex-valued Function; ::_thesis: dom (f1 /" f2) = (dom f1) /\ (dom f2)
thus dom (f1 /" f2) = (dom f1) /\ (dom (f2 ")) by Def4
.= (dom f1) /\ (dom f2) by Def7 ; ::_thesis: verum
end;
theorem :: VALUED_1:17
for f1, f2 being complex-valued Function
for c being set holds (f1 /" f2) . c = (f1 . c) / (f2 . c)
proof
let f1, f2 be complex-valued Function; ::_thesis: for c being set holds (f1 /" f2) . c = (f1 . c) / (f2 . c)
let c be set ; ::_thesis: (f1 /" f2) . c = (f1 . c) / (f2 . c)
A1: dom (f1 /" f2) = (dom f1) /\ (dom f2) by Th16;
percases ( c in dom (f1 /" f2) or not c in dom (f1 /" f2) ) ;
suppose c in dom (f1 /" f2) ; ::_thesis: (f1 /" f2) . c = (f1 . c) / (f2 . c)
hence (f1 /" f2) . c = (f1 . c) * ((f2 ") . c) by Def4
.= (f1 . c) / (f2 . c) by Th10 ;
::_thesis: verum
end;
supposeA2: not c in dom (f1 /" f2) ; ::_thesis: (f1 /" f2) . c = (f1 . c) / (f2 . c)
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 ; ::_thesis: verum
end;
end;
end;
registration
let f1, f2 be complex-valued Function;
clusterf1 /" f2 -> complex-valued ;
coherence
f1 /" f2 is complex-valued ;
end;
registration
let f1, f2 be real-valued Function;
clusterf1 /" f2 -> real-valued ;
coherence
f1 /" f2 is real-valued ;
end;
registration
let f1, f2 be RAT -valued Function;
clusterf1 /" f2 -> RAT -valued ;
coherence
f1 /" f2 is RAT -valued ;
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;
:: original: /"
redefine funcf1 /" f2 -> PartFunc of C,COMPLEX;
coherence
f1 /" f2 is PartFunc of C,COMPLEX
proof
( dom (f1 /" f2) = (dom f1) /\ (dom f2) & rng (f1 /" f2) c= COMPLEX ) by Th16, VALUED_0:def_1;
hence f1 /" f2 is PartFunc of C,COMPLEX by RELSET_1:4; ::_thesis: verum
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;
:: original: /"
redefine funcf1 /" f2 -> PartFunc of C,REAL;
coherence
f1 /" f2 is PartFunc of C,REAL
proof
( dom (f1 /" f2) = (dom f1) /\ (dom f2) & rng (f1 /" f2) c= REAL ) by Th16, VALUED_0:def_3;
hence f1 /" f2 is PartFunc of C,REAL by RELSET_1:4; ::_thesis: verum
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;
:: original: /"
redefine funcf1 /" f2 -> PartFunc of C,RAT;
coherence
f1 /" f2 is PartFunc of C,RAT
proof
( dom (f1 /" f2) = (dom f1) /\ (dom f2) & rng (f1 /" f2) c= RAT ) by Th16, RELAT_1:def_19;
hence f1 /" f2 is PartFunc of C,RAT by RELSET_1:4; ::_thesis: verum
end;
end;
Lm4: for C being set
for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for f2 being Function of C,D2 holds dom (f1 /" f2) = C
proof
let C be set ; ::_thesis: for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for f2 being Function of C,D2 holds dom (f1 /" f2) = C
let D1, D2 be non empty complex-membered set ; ::_thesis: for f1 being Function of C,D1
for f2 being Function of C,D2 holds dom (f1 /" f2) = C
let f1 be Function of C,D1; ::_thesis: for f2 being Function of C,D2 holds dom (f1 /" f2) = C
let f2 be Function of C,D2; ::_thesis: dom (f1 /" f2) = C
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 ; ::_thesis: verum
end;
registration
let C be set ;
let D1, D2 be non empty complex-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
clusterf1 /" f2 -> total for PartFunc of C,COMPLEX;
coherence
for b1 being PartFunc of C,COMPLEX st b1 = f1 /" f2 holds
b1 is total
proof
dom (f1 /" f2) = C by Lm4;
hence for b1 being PartFunc of C,COMPLEX st b1 = f1 /" f2 holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D1, D2 be non empty real-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
clusterf1 /" f2 -> total for PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = f1 /" f2 holds
b1 is total
proof
dom (f1 /" f2) = C by Lm4;
hence for b1 being PartFunc of C,REAL st b1 = f1 /" f2 holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D1, D2 be non empty rational-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
clusterf1 /" f2 -> total for PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = f1 /" f2 holds
b1 is total
proof
dom (f1 /" f2) = C by Lm4;
hence for b1 being PartFunc of C,RAT st b1 = f1 /" f2 holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let f1, f2 be complex-valued FinSequence;
clusterf1 /" f2 -> FinSequence-like ;
coherence
f1 /" f2 is FinSequence-like ;
end;
begin
definition
let f be complex-valued Function;
deffunc H1( set ) -> Element of REAL = |.(f . $1).|;
func|.f.| -> real-valued Function means :Def11: :: VALUED_1:def 11
( dom it = dom f & ( for c being set st c in dom it holds
it . c = |.(f . c).| ) );
existence
ex b1 being real-valued Function st
( dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = |.(f . c).| ) )
proof
consider g being Function such that
A1: ( dom g = dom f & ( for x being set st x in dom f holds
g . x = H1(x) ) ) from FUNCT_1:sch_3();
g is real-valued
proof
let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom g or g . x is real )
assume x in dom g ; ::_thesis: g . x is real
then g . x = |.(f . x).| by A1;
hence g . x is real ; ::_thesis: verum
end;
hence ex b1 being real-valued Function st
( dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = |.(f . c).| ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being real-valued Function st dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 . c = |.(f . c).| ) & dom b2 = dom f & ( for c being set st c in dom b2 holds
b2 . c = |.(f . c).| ) holds
b1 = b2
proof
let h, g be real-valued Function; ::_thesis: ( dom h = dom f & ( for c being set st c in dom h holds
h . c = |.(f . c).| ) & dom g = dom f & ( for c being set st c in dom g holds
g . c = |.(f . c).| ) implies h = g )
assume that
A2: dom h = dom f and
A3: for c being set st c in dom h holds
h . c = H1(c) and
A4: dom g = dom f and
A5: for c being set st c in dom g holds
g . c = H1(c) ; ::_thesis: h = g
now__::_thesis:_for_x_being_set_st_x_in_dom_h_holds_
h_._x_=_g_._x
let x be set ; ::_thesis: ( x in dom h implies h . x = g . x )
assume A6: x in dom h ; ::_thesis: h . x = g . x
hence h . x = H1(x) by A3
.= g . x by A2, A4, A5, A6 ;
::_thesis: verum
end;
hence h = g by A2, A4, FUNCT_1:2; ::_thesis: verum
end;
projectivity
for b1 being real-valued Function
for b2 being complex-valued Function st dom b1 = dom b2 & ( for c being set st c in dom b1 holds
b1 . c = |.(b2 . c).| ) holds
( dom b1 = dom b1 & ( for c being set st c in dom b1 holds
b1 . c = |.(b1 . c).| ) )
proof
let r be real-valued Function; ::_thesis: for b1 being complex-valued Function st dom r = dom b1 & ( for c being set st c in dom r holds
r . c = |.(b1 . c).| ) holds
( dom r = dom r & ( for c being set st c in dom r holds
r . c = |.(r . c).| ) )
let h be complex-valued Function; ::_thesis: ( dom r = dom h & ( for c being set st c in dom r holds
r . c = |.(h . c).| ) implies ( dom r = dom r & ( for c being set st c in dom r holds
r . c = |.(r . c).| ) ) )
assume that
dom r = dom h and
A7: for c being set st c in dom r holds
r . c = |.(h . c).| ; ::_thesis: ( dom r = dom r & ( for c being set st c in dom r holds
r . c = |.(r . c).| ) )
thus dom r = dom r ; ::_thesis: for c being set st c in dom r holds
r . c = |.(r . c).|
let c be set ; ::_thesis: ( c in dom r implies r . c = |.(r . c).| )
assume A8: c in dom r ; ::_thesis: r . c = |.(r . c).|
hence r . c = |.|.(h . c).|.| by A7
.= |.(r . c).| by A7, A8 ;
::_thesis: verum
end;
end;
:: deftheorem Def11 defines |. VALUED_1:def_11_:_
for f being complex-valued Function
for b2 being real-valued Function holds
( b2 = |.f.| iff ( dom b2 = dom f & ( for c being set st c in dom b2 holds
b2 . c = |.(f . c).| ) ) );
notation
let f be complex-valued Function;
synonym abs f for |.f.|;
end;
theorem :: VALUED_1:18
for f being complex-valued Function
for c being set holds |.f.| . c = |.(f . c).|
proof
let f be complex-valued Function; ::_thesis: for c being set holds |.f.| . c = |.(f . c).|
let c be set ; ::_thesis: |.f.| . c = |.(f . c).|
A1: dom |.f.| = dom f by Def11;
percases ( c in dom f or not c in dom f ) ;
suppose c in dom f ; ::_thesis: |.f.| . c = |.(f . c).|
hence |.f.| . c = |.(f . c).| by A1, Def11; ::_thesis: verum
end;
supposeA2: not c in dom f ; ::_thesis: |.f.| . c = |.(f . c).|
hence |.f.| . c = |.0.| by A1, COMPLEX1:44, FUNCT_1:def_2
.= |.(f . c).| by A2, FUNCT_1:def_2 ;
::_thesis: verum
end;
end;
end;
registration
let f be RAT -valued Function;
cluster|.f.| -> RAT -valued real-valued ;
coherence
|.f.| is RAT -valued
proof
let y be set ; :: according to TARSKI:def_3,RELAT_1:def_19 ::_thesis: ( not y in rng |.f.| or y in RAT )
assume y in rng |.f.| ; ::_thesis: y in RAT
then consider x being set 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 y in RAT by A2, RAT_1:def_2; ::_thesis: verum
end;
end;
registration
let f be INT -valued Function;
cluster|.f.| -> real-valued natural-valued ;
coherence
|.f.| is natural-valued
proof
let x be set ; :: according to VALUED_0:def_12 ::_thesis: ( not x in dom |.f.| or |.f.| . x is natural )
abs (f . x) is natural ;
hence ( not x in dom |.f.| or |.f.| . x is natural ) by Def11; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be complex-membered set ;
let f be PartFunc of C,D;
:: original: |.
redefine func|.f.| -> PartFunc of C,REAL;
coherence
|.f.| is PartFunc of C,REAL
proof
( dom |.f.| = dom f & rng |.f.| c= REAL ) by Def11, VALUED_0:def_3;
hence |.f.| is PartFunc of C,REAL by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be complex-membered set ;
let f be PartFunc of C,D;
:: original: |.
redefine func abs f -> PartFunc of C,REAL;
coherence
|.f.| is PartFunc of C,REAL
proof
abs f = |.f.| ;
hence |.f.| is PartFunc of C,REAL ; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be rational-membered set ;
let f be PartFunc of C,D;
:: original: |.
redefine func|.f.| -> PartFunc of C,RAT;
coherence
|.f.| is PartFunc of C,RAT
proof
( dom |.f.| = dom f & rng |.f.| c= RAT ) by Def11, RELAT_1:def_19;
hence |.f.| is PartFunc of C,RAT by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be rational-membered set ;
let f be PartFunc of C,D;
:: original: |.
redefine func abs f -> PartFunc of C,RAT;
coherence
|.f.| is PartFunc of C,RAT
proof
abs f = |.f.| ;
hence |.f.| is PartFunc of C,RAT ; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be integer-membered set ;
let f be PartFunc of C,D;
:: original: |.
redefine func|.f.| -> PartFunc of C,NAT;
coherence
|.f.| is PartFunc of C,NAT
proof
( dom |.f.| = dom f & rng |.f.| c= NAT ) by Def11, VALUED_0:def_6;
hence |.f.| is PartFunc of C,NAT by RELSET_1:4; ::_thesis: verum
end;
end;
definition
let C be set ;
let D be integer-membered set ;
let f be PartFunc of C,D;
:: original: |.
redefine func abs f -> PartFunc of C,NAT;
coherence
|.f.| is PartFunc of C,NAT
proof
abs f = |.f.| ;
hence |.f.| is PartFunc of C,NAT ; ::_thesis: verum
end;
end;
registration
let C be set ;
let D be non empty complex-membered set ;
let f be Function of C,D;
cluster|.f.| -> total for PartFunc of C,REAL;
coherence
for b1 being PartFunc of C,REAL st b1 = |.f.| holds
b1 is total
proof
dom |.f.| = dom f by Def11
.= C by FUNCT_2:def_1 ;
hence for b1 being PartFunc of C,REAL st b1 = |.f.| holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D be non empty rational-membered set ;
let f be Function of C,D;
cluster|.f.| -> total for PartFunc of C,RAT;
coherence
for b1 being PartFunc of C,RAT st b1 = |.f.| holds
b1 is total
proof
dom |.f.| = dom f by Def11
.= C by FUNCT_2:def_1 ;
hence for b1 being PartFunc of C,RAT st b1 = |.f.| holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let C be set ;
let D be non empty integer-membered set ;
let f be Function of C,D;
cluster|.f.| -> total for PartFunc of C,NAT;
coherence
for b1 being PartFunc of C,NAT st b1 = |.f.| holds
b1 is total
proof
dom |.f.| = dom f by Def11
.= C by FUNCT_2:def_1 ;
hence for b1 being PartFunc of C,NAT st b1 = |.f.| holds
b1 is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let f be complex-valued FinSequence;
cluster|.f.| -> real-valued FinSequence-like ;
coherence
|.f.| is FinSequence-like
proof
dom (abs f) = dom f by Def11;
hence |.f.| is FinSequence-like by Lm1; ::_thesis: verum
end;
end;
theorem :: VALUED_1:19
for f, g being FinSequence
for h being Function st dom h = (dom f) /\ (dom g) holds
h is FinSequence by Lm2;
begin
definition
let p be Function;
let k be Nat;
func Shift (p,k) -> Function means :Def12: :: VALUED_1:def 12
( dom it = { (m + k) where m is Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds
it . (m + k) = p . m ) );
existence
ex b1 being Function st
( dom b1 = { (m + k) where m is Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds
b1 . (m + k) = p . m ) )
proof
defpred S1[ set , set ] means ex m being Element of NAT st
( $1 = m + k & $2 = p . m );
set A = { (m + k) where m is Element of NAT : m in dom p } ;
A1: for e being set st e in { (m + k) where m is Element of NAT : m in dom p } holds
ex u being set st S1[e,u]
proof
let e be set ; ::_thesis: ( e in { (m + k) where m is Element of NAT : m in dom p } implies ex u being set st S1[e,u] )
assume e in { (m + k) where m is Element of NAT : m in dom p } ; ::_thesis: ex u being set st S1[e,u]
then consider m being Element of NAT such that
A2: e = m + k and
m in dom p ;
take p . m ; ::_thesis: S1[e,p . m]
thus S1[e,p . m] by A2; ::_thesis: verum
end;
consider f being Function such that
A3: dom f = { (m + k) where m is Element of NAT : m in dom p } and
A4: for e being set st e in { (m + k) where m is Element of NAT : m in dom p } holds
S1[e,f . e] from CLASSES1:sch_1(A1);
take f ; ::_thesis: ( dom f = { (m + k) where m is Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds
f . (m + k) = p . m ) )
thus dom f = { (m + k) where m is Element of NAT : m in dom p } by A3; ::_thesis: for m being Element of NAT st m in dom p holds
f . (m + k) = p . m
let m be Element of NAT ; ::_thesis: ( m in dom p implies f . (m + k) = p . m )
assume m in dom p ; ::_thesis: f . (m + k) = p . m
then m + k in { (m + k) where m is Element of NAT : m in dom p } ;
then ex j being Element of NAT st
( m + k = j + k & f . (m + k) = p . j ) by A4;
hence f . (m + k) = p . m ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function st dom b1 = { (m + k) where m is Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds
b1 . (m + k) = p . m ) & dom b2 = { (m + k) where m is Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds
b2 . (m + k) = p . m ) holds
b1 = b2
proof
let IT1, IT2 be Function; ::_thesis: ( dom IT1 = { (m + k) where m is Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds
IT1 . (m + k) = p . m ) & dom IT2 = { (m + k) where m is Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds
IT2 . (m + k) = p . m ) implies IT1 = IT2 )
assume that
A5: dom IT1 = { (m + k) where m is Element of NAT : m in dom p } and
A6: for m being Element of NAT st m in dom p holds
IT1 . (m + k) = p . m and
A7: dom IT2 = { (m + k) where m is Element of NAT : m in dom p } and
A8: for m being Element of NAT st m in dom p holds
IT2 . (m + k) = p . m ; ::_thesis: IT1 = IT2
for x being set st x in dom IT1 holds
IT1 . x = IT2 . x
proof
let x be set ; ::_thesis: ( x in dom IT1 implies IT1 . x = IT2 . x )
assume x in dom IT1 ; ::_thesis: IT1 . x = IT2 . x
then consider m being Element of 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 ; ::_thesis: verum
end;
hence IT1 = IT2 by A5, A7, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines Shift VALUED_1:def_12_:_
for p being Function
for k being Nat
for b3 being Function holds
( b3 = Shift (p,k) iff ( dom b3 = { (m + k) where m is Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds
b3 . (m + k) = p . m ) ) );
registration
let p be Function;
let k be Nat;
cluster Shift (p,k) -> NAT -defined ;
coherence
Shift (p,k) is NAT -defined
proof
A1: dom (Shift (p,k)) = { (m + k) where m is Element of NAT : m in dom p } by Def12;
Shift (p,k) is NAT -defined
proof
let x be set ; :: according to TARSKI:def_3,RELAT_1:def_18 ::_thesis: ( not x in dom (Shift (p,k)) or x in NAT )
assume x in dom (Shift (p,k)) ; ::_thesis: x in NAT
then ex m being Element of NAT st
( x = m + k & m in dom p ) by A1;
hence x in NAT ; ::_thesis: verum
end;
hence Shift (p,k) is NAT -defined ; ::_thesis: verum
end;
end;
theorem :: VALUED_1:20
for P, Q being Function
for k being Nat st P c= Q holds
Shift (P,k) c= Shift (Q,k)
proof
let P, Q be Function; ::_thesis: for k being Nat st P c= Q holds
Shift (P,k) c= Shift (Q,k)
let k be Nat; ::_thesis: ( P c= Q implies Shift (P,k) c= Shift (Q,k) )
assume A1: P c= Q ; ::_thesis: Shift (P,k) c= Shift (Q,k)
then A2: dom P c= dom Q by GRFUNC_1:2;
A3: dom (Shift (P,k)) = { (m + k) where m is Element of NAT : m in dom P } by Def12;
A4: dom (Shift (Q,k)) = { (m + k) where m is Element of NAT : m in dom Q } by Def12;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Shift_(P,k))_holds_
x_in_dom_(Shift_(Q,k))
let x be set ; ::_thesis: ( x in dom (Shift (P,k)) implies x in dom (Shift (Q,k)) )
assume x in dom (Shift (P,k)) ; ::_thesis: x in dom (Shift (Q,k))
then ex m1 being Element of NAT st
( x = m1 + k & m1 in dom P ) by A3;
hence x in dom (Shift (Q,k)) by A2, A4; ::_thesis: verum
end;
then A5: dom (Shift (P,k)) c= dom (Shift (Q,k)) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Shift_(P,k))_holds_
(Shift_(P,k))_._x_=_(Shift_(Q,k))_._x
let x be set ; ::_thesis: ( x in dom (Shift (P,k)) implies (Shift (P,k)) . x = (Shift (Q,k)) . x )
assume x in dom (Shift (P,k)) ; ::_thesis: (Shift (P,k)) . x = (Shift (Q,k)) . x
then consider m1 being Element of 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 ; ::_thesis: verum
end;
hence Shift (P,k) c= Shift (Q,k) by A5, GRFUNC_1:2; ::_thesis: verum
end;
theorem :: VALUED_1:21
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; ::_thesis: for I being Function holds Shift ((Shift (I,m)),n) = Shift (I,(m + n))
let I be Function; ::_thesis: Shift ((Shift (I,m)),n) = Shift (I,(m + n))
set A = { (l + m) where l is Element of NAT : l in dom I } ;
A1: dom (Shift (I,m)) = { (l + m) where l is Element of NAT : l in dom I } by Def12;
A2: now__::_thesis:_for_l_being_Element_of_NAT_st_l_in_dom_I_holds_
(Shift_((Shift_(I,m)),n))_._(l_+_(m_+_n))_=_I_._l
let l be Element of NAT ; ::_thesis: ( l in dom I implies (Shift ((Shift (I,m)),n)) . (l + (m + n)) = I . l )
assume A3: l in dom I ; ::_thesis: (Shift ((Shift (I,m)),n)) . (l + (m + n)) = I . l
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 ; ::_thesis: verum
end;
{ (p + n) where p is Element of NAT : p in { (l + m) where l is Element of NAT : l in dom I } } = { (q + (m + n)) where q is Element of NAT : q in dom I }
proof
thus { (p + n) where p is Element of NAT : p in { (l + m) where l is Element of NAT : l in dom I } } c= { (q + (m + n)) where q is Element of NAT : q in dom I } :: according to XBOOLE_0:def_10 ::_thesis: { (q + (m + n)) where q is Element of NAT : q in dom I } c= { (p + n) where p is Element of NAT : p in { (l + m) where l is Element of NAT : l in dom I } }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (p + n) where p is Element of NAT : p in { (l + m) where l is Element of NAT : l in dom I } } or x in { (q + (m + n)) where q is Element of NAT : q in dom I } )
assume x in { (p + n) where p is Element of NAT : p in { (l + m) where l is Element of NAT : l in dom I } } ; ::_thesis: x in { (q + (m + n)) where q is Element of NAT : q in dom I }
then consider p being Element of NAT such that
A5: x = p + n and
A6: p in { (l + m) where l is Element of NAT : l in dom I } ;
consider l being Element of NAT such that
A7: p = l + m and
A8: l in dom I by A6;
x = l + (m + n) by A5, A7;
hence x in { (q + (m + n)) where q is Element of NAT : q in dom I } by A8; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (q + (m + n)) where q is Element of NAT : q in dom I } or x in { (p + n) where p is Element of NAT : p in { (l + m) where l is Element of NAT : l in dom I } } )
assume x in { (q + (m + n)) where q is Element of NAT : q in dom I } ; ::_thesis: x in { (p + n) where p is Element of NAT : p in { (l + m) where l is Element of NAT : l in dom I } }
then consider q being Element of NAT such that
A9: ( x = q + (m + n) & q in dom I ) ;
( x = (q + m) + n & q + m in { (l + m) where l is Element of NAT : l in dom I } ) by A9;
hence x in { (p + n) where p is Element of NAT : p in { (l + m) where l is Element of NAT : l in dom I } } ; ::_thesis: verum
end;
then dom (Shift ((Shift (I,m)),n)) = { (l + (m + n)) where l is Element of NAT : l in dom I } by A1, Def12;
hence Shift ((Shift (I,m)),n) = Shift (I,(m + n)) by A2, Def12; ::_thesis: verum
end;
theorem :: VALUED_1:22
for s, f being Function
for n being Nat holds Shift ((f * s),n) = f * (Shift (s,n))
proof
let s, f be Function; ::_thesis: for n being Nat holds Shift ((f * s),n) = f * (Shift (s,n))
let n be Nat; ::_thesis: Shift ((f * s),n) = f * (Shift (s,n))
A1: dom (f * s) c= dom s by RELAT_1:25;
A2: dom (Shift (s,n)) = { (m + n) where m is Element of NAT : m in dom s } by Def12;
now__::_thesis:_for_e_being_set_holds_
(_(_e_in__{__(m_+_n)_where_m_is_Element_of_NAT_:_m_in_dom_(f_*_s)__}__implies_(_e_in_dom_(Shift_(s,n))_&_(Shift_(s,n))_._e_in_dom_f_)_)_&_(_e_in_dom_(Shift_(s,n))_&_(Shift_(s,n))_._e_in_dom_f_implies_e_in__{__(m_+_n)_where_m_is_Element_of_NAT_:_m_in_dom_(f_*_s)__}__)_)
let e be set ; ::_thesis: ( ( e in { (m + n) where m is Element of NAT : m in dom (f * s) } implies ( e in dom (Shift (s,n)) & (Shift (s,n)) . e in dom f ) ) & ( e in dom (Shift (s,n)) & (Shift (s,n)) . e in dom f implies e in { (m + n) where m is Element of NAT : m in dom (f * s) } ) )
thus ( e in { (m + n) where m is Element of NAT : m in dom (f * s) } implies ( e in dom (Shift (s,n)) & (Shift (s,n)) . e in dom f ) ) ::_thesis: ( e in dom (Shift (s,n)) & (Shift (s,n)) . e in dom f implies e in { (m + n) where m is Element of NAT : m in dom (f * s) } )
proof
assume e in { (m + n) where m is Element of NAT : m in dom (f * s) } ; ::_thesis: ( e in dom (Shift (s,n)) & (Shift (s,n)) . e in dom f )
then consider m being Element of 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; ::_thesis: (Shift (s,n)) . e in dom f
(Shift (s,n)) . e = s . m by A1, A3, A4, Def12;
hence (Shift (s,n)) . e in dom f by A4, FUNCT_1:11; ::_thesis: verum
end;
assume e in dom (Shift (s,n)) ; ::_thesis: ( (Shift (s,n)) . e in dom f implies e in { (m + n) where m is Element of NAT : m in dom (f * s) } )
then consider m0 being Element of NAT such that
A5: e = m0 + n and
A6: m0 in dom s by A2;
assume (Shift (s,n)) . e in dom f ; ::_thesis: e in { (m + n) where m is Element of NAT : m in dom (f * s) }
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 Element of NAT : m in dom (f * s) } by A5; ::_thesis: verum
end;
then (Shift (s,n)) " (dom f) = { (m + n) where m is Element of NAT : m in dom (f * s) } by FUNCT_1:def_7;
then A7: dom (f * (Shift (s,n))) = { (m + n) where m is Element of NAT : m in dom (f * s) } by RELAT_1:147;
now__::_thesis:_for_m_being_Element_of_NAT_st_m_in_dom_(f_*_s)_holds_
(f_*_(Shift_(s,n)))_._(m_+_n)_=_(f_*_s)_._m
let m be Element of NAT ; ::_thesis: ( m in dom (f * s) implies (f * (Shift (s,n))) . (m + n) = (f * s) . m )
assume A8: m in dom (f * s) ; ::_thesis: (f * (Shift (s,n))) . (m + n) = (f * s) . m
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 ;
::_thesis: verum
end;
hence Shift ((f * s),n) = f * (Shift (s,n)) by A7, Def12; ::_thesis: verum
end;
theorem :: VALUED_1:23
for I, J being Function
for n being Nat holds Shift ((I +* J),n) = (Shift (I,n)) +* (Shift (J,n))
proof
let I, J be Function; ::_thesis: for n being Nat holds Shift ((I +* J),n) = (Shift (I,n)) +* (Shift (J,n))
let n be Nat; ::_thesis: Shift ((I +* J),n) = (Shift (I,n)) +* (Shift (J,n))
A1: dom (Shift (J,n)) = { (m + n) where m is Element of NAT : m in dom J } by Def12;
A2: now__::_thesis:_for_m_being_Element_of_NAT_st_m_in_dom_(I_+*_J)_holds_
((Shift_(I,n))_+*_(Shift_(J,n)))_._(m_+_n)_=_(I_+*_J)_._m
let m be Element of NAT ; ::_thesis: ( m in dom (I +* J) implies ((Shift (I,n)) +* (Shift (J,n))) . (b1 + n) = (I +* J) . b1 )
assume A3: m in dom (I +* J) ; ::_thesis: ((Shift (I,n)) +* (Shift (J,n))) . (b1 + n) = (I +* J) . b1
percases ( m in dom J or not m in dom J ) ;
supposeA4: m in dom J ; ::_thesis: ((Shift (I,n)) +* (Shift (J,n))) . (b1 + n) = (I +* J) . b1
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 ;
::_thesis: verum
end;
supposeA5: not m in dom J ; ::_thesis: ((Shift (I,n)) +* (Shift (J,n))) . (b1 + n) = (I +* J) . b1
m in (dom I) \/ (dom J) by A3, FUNCT_4:def_1;
then A6: m in dom I by A5, XBOOLE_0:def_3;
for l being Element of NAT holds
( not m + n = l + n or not 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 ;
::_thesis: verum
end;
end;
end;
A7: dom (Shift (I,n)) = { (m + n) where m is Element of NAT : m in dom I } by Def12;
A8: (dom (Shift (I,n))) \/ (dom (Shift (J,n))) = { (m + n) where m is Element of NAT : m in (dom I) \/ (dom J) }
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { (m + n) where m is Element of NAT : m in (dom I) \/ (dom J) } c= (dom (Shift (I,n))) \/ (dom (Shift (J,n)))
let x be set ; ::_thesis: ( x in (dom (Shift (I,n))) \/ (dom (Shift (J,n))) implies x in { (l + n) where l is Element of NAT : l in (dom I) \/ (dom J) } )
assume x in (dom (Shift (I,n))) \/ (dom (Shift (J,n))) ; ::_thesis: x in { (l + n) where l is Element of NAT : l in (dom I) \/ (dom J) }
then ( x in dom (Shift (I,n)) or x in dom (Shift (J,n)) ) by XBOOLE_0:def_3;
then consider m being Element of 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 Element of NAT : l in (dom I) \/ (dom J) } by A9; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (m + n) where m is Element of NAT : m in (dom I) \/ (dom J) } or x in (dom (Shift (I,n))) \/ (dom (Shift (J,n))) )
assume x in { (m + n) where m is Element of NAT : m in (dom I) \/ (dom J) } ; ::_thesis: x in (dom (Shift (I,n))) \/ (dom (Shift (J,n)))
then consider m being Element of 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 x in (dom (Shift (I,n))) \/ (dom (Shift (J,n))) by XBOOLE_0:def_3; ::_thesis: verum
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 Element of NAT : m in dom (I +* J) } by A8, FUNCT_4:def_1;
hence Shift ((I +* J),n) = (Shift (I,n)) +* (Shift (J,n)) by A2, Def12; ::_thesis: verum
end;
theorem Th24: :: VALUED_1:24
for p being Function
for k, il being Nat st il in dom p holds
il + k in dom (Shift (p,k))
proof
let p be Function; ::_thesis: for k, il being Nat st il in dom p holds
il + k in dom (Shift (p,k))
let k, il be Nat; ::_thesis: ( il in dom p implies il + k in dom (Shift (p,k)) )
assume A1: il in dom p ; ::_thesis: il + k in dom (Shift (p,k))
A2: dom (Shift (p,k)) = { (loc + k) where loc is Element of NAT : loc in dom p } by Def12;
reconsider loc = il as Element of NAT by ORDINAL1:def_12;
loc + k in dom (Shift (p,k)) by A2, A1;
hence il + k in dom (Shift (p,k)) ; ::_thesis: verum
end;
theorem Th25: :: VALUED_1:25
for p being Function
for k being Nat holds rng (Shift (p,k)) c= rng p
proof
let p be Function; ::_thesis: for k being Nat holds rng (Shift (p,k)) c= rng p
let k be Nat; ::_thesis: rng (Shift (p,k)) c= rng p
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (Shift (p,k)) or y in rng p )
assume y in rng (Shift (p,k)) ; ::_thesis: y in rng p
then consider x being set 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 Element of NAT : m in dom p } by A1, Def12;
then consider m being Element of NAT such that
A3: x = m + k and
A4: m in dom p ;
p . m = (Shift (p,k)) . x by A3, A4, Def12;
hence y in rng p by A2, A4, FUNCT_1:def_3; ::_thesis: verum
end;
theorem :: VALUED_1:26
for p being Function st dom p c= NAT holds
for k being Nat holds rng (Shift (p,k)) = rng p
proof
let p be Function; ::_thesis: ( dom p c= NAT implies for k being Nat holds rng (Shift (p,k)) = rng p )
assume A1: dom p c= NAT ; ::_thesis: for k being Nat holds rng (Shift (p,k)) = rng p
let k be Nat; ::_thesis: rng (Shift (p,k)) = rng p
thus rng (Shift (p,k)) c= rng p by Th25; :: according to XBOOLE_0:def_10 ::_thesis: rng p c= rng (Shift (p,k))
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in rng (Shift (p,k)) )
assume y in rng p ; ::_thesis: y in rng (Shift (p,k))
then consider x being set such that
A2: x in dom p and
A3: y = p . x by FUNCT_1:def_3;
reconsider x = 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 y in rng (Shift (p,k)) by FUNCT_1:def_3; ::_thesis: verum
end;
registration
let p be finite Function;
let k be Nat;
cluster Shift (p,k) -> finite ;
coherence
Shift (p,k) is finite
proof
deffunc H1( Element of NAT ) -> Element of NAT = p + k;
A1: dom p is finite ;
{ H1(w) where w is Element of NAT : w in dom p } is finite from FRAENKEL:sch_21(A1);
then dom (Shift (p,k)) is finite by Def12;
hence Shift (p,k) is finite by FINSET_1:10; ::_thesis: verum
end;
end;
definition
let X be non empty ext-real-membered set ;
let s be sequence of X;
:: original: increasing
redefine attrs is increasing means :: VALUED_1:def 13
for n being Nat holds s . n < s . (n + 1);
compatibility
( s is increasing iff for n being Nat holds s . n < s . (n + 1) )
proof
thus ( s is increasing implies for n being Nat holds s . n < s . (n + 1) ) ::_thesis: ( ( for n being Nat holds s . n < s . (n + 1) ) implies s is increasing )
proof
assume A1: s is increasing ; ::_thesis: for n being Nat holds s . n < s . (n + 1)
let n be Nat; ::_thesis: s . n < s . (n + 1)
A2: n < n + 1 by NAT_1:13;
( dom s = NAT & n in NAT ) by FUNCT_2:def_1, ORDINAL1:def_12;
hence s . n < s . (n + 1) by A1, A2, VALUED_0:def_13; ::_thesis: verum
end;
assume A3: for n being Nat holds s . n < s . (n + 1) ; ::_thesis: s is increasing
let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for b1 being set holds
( not e1 in dom s or not b1 in dom s or b1 <= e1 or not s . b1 <= s . e1 )
let e2 be ext-real number ; ::_thesis: ( not e1 in dom s or not e2 in dom s or e2 <= e1 or not s . e2 <= s . e1 )
assume ( e1 in dom s & e2 in dom s ) ; ::_thesis: ( e2 <= e1 or not s . e2 <= s . e1 )
then reconsider m = e1, n = e2 as Nat ;
defpred S1[ Nat] means ( m < $1 implies s . m < s . $1 );
A4: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; ::_thesis: ( S1[j] implies S1[j + 1] )
assume A5: S1[j] ; ::_thesis: S1[j + 1]
assume m < j + 1 ; ::_thesis: s . m < s . (j + 1)
then m <= j by NAT_1:13;
then ( s . m < s . j or m = j ) by A5, XXREAL_0:1;
hence s . m < s . (j + 1) by A3, XXREAL_0:2; ::_thesis: verum
end;
assume A6: e1 < e2 ; ::_thesis: not s . e2 <= s . e1
A7: S1[ 0 ] ;
for j being Nat holds S1[j] from NAT_1:sch_2(A7, A4);
then s . m < s . n by A6;
hence not s . e2 <= s . e1 ; ::_thesis: verum
end;
:: original: decreasing
redefine attrs is decreasing means :: VALUED_1:def 14
for n being Nat holds s . n > s . (n + 1);
compatibility
( s is decreasing iff for n being Nat holds s . n > s . (n + 1) )
proof
thus ( s is decreasing implies for n being Nat holds s . n > s . (n + 1) ) ::_thesis: ( ( for n being Nat holds s . n > s . (n + 1) ) implies s is decreasing )
proof
assume A8: s is decreasing ; ::_thesis: for n being Nat holds s . n > s . (n + 1)
let n be Nat; ::_thesis: s . n > s . (n + 1)
A9: n < n + 1 by NAT_1:13;
( dom s = NAT & n in NAT ) by FUNCT_2:def_1, ORDINAL1:def_12;
hence s . n > s . (n + 1) by A8, A9, VALUED_0:def_14; ::_thesis: verum
end;
assume A10: for n being Nat holds s . n > s . (n + 1) ; ::_thesis: s is decreasing
let e1 be ext-real number ; :: according to VALUED_0:def_14 ::_thesis: for b1 being set holds
( not e1 in dom s or not b1 in dom s or b1 <= e1 or not s . e1 <= s . b1 )
let e2 be ext-real number ; ::_thesis: ( not e1 in dom s or not e2 in dom s or e2 <= e1 or not s . e1 <= s . e2 )
assume ( e1 in dom s & e2 in dom s ) ; ::_thesis: ( e2 <= e1 or not s . e1 <= s . e2 )
then reconsider m = e1, n = e2 as Nat ;
defpred S1[ Nat] means ( m < $1 implies s . m > s . $1 );
A11: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; ::_thesis: ( S1[j] implies S1[j + 1] )
assume A12: S1[j] ; ::_thesis: S1[j + 1]
assume m < j + 1 ; ::_thesis: s . m > s . (j + 1)
then m <= j by NAT_1:13;
then ( s . m > s . j or m = j ) by A12, XXREAL_0:1;
hence s . m > s . (j + 1) by A10, XXREAL_0:2; ::_thesis: verum
end;
assume A13: e1 < e2 ; ::_thesis: not s . e1 <= s . e2
A14: S1[ 0 ] ;
for j being Nat holds S1[j] from NAT_1:sch_2(A14, A11);
then s . m > s . n by A13;
hence not s . e1 <= s . e2 ; ::_thesis: verum
end;
:: original: non-decreasing
redefine attrs is non-decreasing means :: VALUED_1:def 15
for n being Nat holds s . n <= s . (n + 1);
compatibility
( s is non-decreasing iff for n being Nat holds s . n <= s . (n + 1) )
proof
thus ( s is non-decreasing implies for n being Nat holds s . n <= s . (n + 1) ) ::_thesis: ( ( for n being Nat holds s . n <= s . (n + 1) ) implies s is non-decreasing )
proof
assume A15: s is non-decreasing ; ::_thesis: for n being Nat holds s . n <= s . (n + 1)
let n be Nat; ::_thesis: s . n <= s . (n + 1)
A16: n < n + 1 by NAT_1:13;
( dom s = NAT & n in NAT ) by FUNCT_2:def_1, ORDINAL1:def_12;
hence s . n <= s . (n + 1) by A15, A16, VALUED_0:def_15; ::_thesis: verum
end;
assume A17: for n being Nat holds s . n <= s . (n + 1) ; ::_thesis: s is non-decreasing
let e1 be ext-real number ; :: according to VALUED_0:def_15 ::_thesis: for b1 being set holds
( not e1 in dom s or not b1 in dom s or not e1 <= b1 or s . e1 <= s . b1 )
let e2 be ext-real number ; ::_thesis: ( not e1 in dom s or not e2 in dom s or not e1 <= e2 or s . e1 <= s . e2 )
assume ( e1 in dom s & e2 in dom s ) ; ::_thesis: ( not e1 <= e2 or s . e1 <= s . e2 )
then reconsider m = e1, n = e2 as Nat ;
defpred S1[ Nat] means ( m <= $1 implies s . m <= s . $1 );
A18: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; ::_thesis: ( S1[j] implies S1[j + 1] )
assume A19: S1[j] ; ::_thesis: S1[j + 1]
assume m <= j + 1 ; ::_thesis: s . m <= s . (j + 1)
then A20: ( m < j + 1 or m = j + 1 ) by XXREAL_0:1;
s . j <= s . (j + 1) by A17;
hence s . m <= s . (j + 1) by A19, A20, NAT_1:13, XXREAL_0:2; ::_thesis: verum
end;
assume A21: e1 <= e2 ; ::_thesis: s . e1 <= s . e2
A22: S1[ 0 ] ;
for j being Nat holds S1[j] from NAT_1:sch_2(A22, A18);
then s . m <= s . n by A21;
hence s . e1 <= s . e2 ; ::_thesis: verum
end;
:: original: non-increasing
redefine attrs is non-increasing means :: VALUED_1:def 16
for n being Nat holds s . n >= s . (n + 1);
compatibility
( s is non-increasing iff for n being Nat holds s . n >= s . (n + 1) )
proof
thus ( s is non-increasing implies for n being Nat holds s . n >= s . (n + 1) ) ::_thesis: ( ( for n being Nat holds s . n >= s . (n + 1) ) implies s is non-increasing )
proof
assume A23: s is non-increasing ; ::_thesis: for n being Nat holds s . n >= s . (n + 1)
let n be Nat; ::_thesis: s . n >= s . (n + 1)
A24: n < n + 1 by NAT_1:13;
( dom s = NAT & n in NAT ) by FUNCT_2:def_1, ORDINAL1:def_12;
hence s . n >= s . (n + 1) by A23, A24, VALUED_0:def_16; ::_thesis: verum
end;
assume A25: for n being Nat holds s . n >= s . (n + 1) ; ::_thesis: s is non-increasing
let e1 be ext-real number ; :: according to VALUED_0:def_16 ::_thesis: for b1 being set holds
( not e1 in dom s or not b1 in dom s or not e1 <= b1 or s . b1 <= s . e1 )
let e2 be ext-real number ; ::_thesis: ( not e1 in dom s or not e2 in dom s or not e1 <= e2 or s . e2 <= s . e1 )
assume ( e1 in dom s & e2 in dom s ) ; ::_thesis: ( not e1 <= e2 or s . e2 <= s . e1 )
then reconsider m = e1, n = e2 as Nat ;
defpred S1[ Nat] means ( m <= $1 implies s . m >= s . $1 );
A26: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; ::_thesis: ( S1[j] implies S1[j + 1] )
assume A27: S1[j] ; ::_thesis: S1[j + 1]
assume m <= j + 1 ; ::_thesis: s . m >= s . (j + 1)
then A28: ( m < j + 1 or m = j + 1 ) by XXREAL_0:1;
s . j >= s . (j + 1) by A25;
hence s . m >= s . (j + 1) by A27, A28, NAT_1:13, XXREAL_0:2; ::_thesis: verum
end;
assume A29: e1 <= e2 ; ::_thesis: s . e2 <= s . e1
A30: S1[ 0 ] ;
for j being Nat holds S1[j] from NAT_1:sch_2(A30, A26);
then s . m >= s . n by A29;
hence s . e2 <= s . e1 ; ::_thesis: verum
end;
end;
:: deftheorem defines increasing VALUED_1:def_13_:_
for X being non empty ext-real-membered set
for s being sequence of X holds
( s is increasing iff for n being Nat holds s . n < s . (n + 1) );
:: deftheorem defines decreasing VALUED_1:def_14_:_
for X being non empty ext-real-membered set
for s being sequence of X holds
( s is decreasing iff for n being Nat holds s . n > s . (n + 1) );
:: deftheorem defines non-decreasing VALUED_1:def_15_:_
for X being non empty ext-real-membered set
for s being sequence of X holds
( s is non-decreasing iff for n being Nat holds s . n <= s . (n + 1) );
:: deftheorem defines non-increasing VALUED_1:def_16_:_
for X being non empty ext-real-membered set
for s being sequence of X holds
( s is non-increasing iff for n being Nat holds s . n >= s . (n + 1) );
scheme :: VALUED_1:sch 1
SubSeqChoice{ F1() -> non empty set , F2() -> sequence of F1(), P1[ set ] } :
ex S1 being subsequence of F2() st
for n being Element of NAT holds P1[S1 . n]
provided
A1: for n being Element of NAT ex m being Element of NAT st
( n <= m & P1[F2() . m] )
proof
defpred S1[ set , set , set ] means ( $3 in NAT & ( for m, k being Element of NAT st m = $2 & k = $3 holds
( m < k & P1[F2() . k] ) ) );
consider n0 being Element of NAT such that
0 <= n0 and
A2: P1[F2() . n0] by A1;
A3: for n being Element of NAT
for x being set ex y being set st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being set ex y being set st S1[n,x,y]
let x be set ; ::_thesis: ex y being set st S1[n,x,y]
percases ( x in NAT or not x in NAT ) ;
suppose x in NAT ; ::_thesis: ex y being set st S1[n,x,y]
then reconsider mx = x as Element of NAT ;
consider my being Element of NAT such that
A4: ( mx + 1 <= my & P1[F2() . my] ) by A1;
take my ; ::_thesis: S1[n,x,my]
thus my in NAT ; ::_thesis: for m, k being Element of NAT st m = x & k = my holds
( m < k & P1[F2() . k] )
thus for m, k being Element of NAT st m = x & k = my holds
( m < k & P1[F2() . k] ) by A4, NAT_1:13; ::_thesis: verum
end;
supposeA5: not x in NAT ; ::_thesis: ex y being set st S1[n,x,y]
take 0 ; ::_thesis: S1[n,x, 0 ]
set y = 0 ;
thus 0 in NAT ; ::_thesis: for m, k being Element of NAT st m = x & k = 0 holds
( m < k & P1[F2() . k] )
let m, k be Element of NAT ; ::_thesis: ( m = x & k = 0 implies ( m < k & P1[F2() . k] ) )
assume that
A6: m = x and
k = 0 ; ::_thesis: ( m < k & P1[F2() . k] )
thus ( m < k & P1[F2() . k] ) by A5, A6; ::_thesis: verum
end;
end;
end;
consider g being Function such that
A7: dom g = NAT and
A8: g . 0 = n0 and
A9: for n being Element of NAT holds S1[n,g . n,g . (n + 1)] from RECDEF_1:sch_1(A3);
rng g c= NAT
proof
defpred S2[ Element of NAT ] means g . $1 in NAT ;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in NAT )
assume y in rng g ; ::_thesis: y in NAT
then consider x being set 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 Element of NAT st S2[k] holds
S2[k + 1] by A9;
A13: S2[ 0 ] by A8;
for k being Element of NAT holds S2[k] from NAT_1:sch_1(A13, A12);
then g . n in NAT ;
hence y in NAT by A11; ::_thesis: verum
end;
then reconsider g = g as sequence of NAT by A7, FUNCT_2:2;
g is V39()
proof
let n be Nat; :: according to VALUED_1:def_13 ::_thesis: g . n < g . (n + 1)
reconsider n = n as Element of NAT by ORDINAL1:def_12;
g . n < g . (n + 1) by A9;
hence g . n < g . (n + 1) ; ::_thesis: verum
end;
then reconsider g = g as V39() sequence of NAT ;
reconsider S1 = F2() * g as sequence of F1() ;
A14: dom S1 = NAT by FUNCT_2:def_1;
reconsider S1 = S1 as subsequence of F2() ;
take S1 ; ::_thesis: for n being Element of NAT holds P1[S1 . n]
thus for n being Element of NAT holds P1[S1 . n] ::_thesis: verum
proof
let n be Element of NAT ; ::_thesis: P1[S1 . n]
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: P1[S1 . n]
hence P1[S1 . n] by A2, A8, A14, FUNCT_1:12; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: P1[S1 . n]
then n >= 0 + 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
P1[F2() . k] by A9;
then P1[F2() . k] ;
hence P1[S1 . n] by A14, FUNCT_1:12; ::_thesis: verum
end;
end;
end;
end;
theorem :: VALUED_1:27
for k being Nat
for F being NAT -defined Function holds dom F, dom (Shift (F,k)) are_equipotent
proof
let k be Nat; ::_thesis: for F being NAT -defined Function holds dom F, dom (Shift (F,k)) are_equipotent
let F be NAT -defined Function; ::_thesis: dom F, dom (Shift (F,k)) are_equipotent
defpred S1[ set , set ] means ex il being Element of NAT st
( $1 = il & $2 = k + il );
A1: for e being set st e in dom F holds
ex u being set st S1[e,u]
proof
let e be set ; ::_thesis: ( e in dom F implies ex u being set st S1[e,u] )
assume e in dom F ; ::_thesis: ex u being set st S1[e,u]
then reconsider e = e as Element of NAT ;
take k + e ; ::_thesis: S1[e,k + e]
take e ; ::_thesis: ( e = e & k + e = k + e )
thus ( e = e & k + e = k + e ) ; ::_thesis: verum
end;
consider f being Function such that
A2: dom f = dom F and
A3: for x being set st x in dom F holds
S1[x,f . x] from CLASSES1:sch_1(A1);
take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = dom F & rng f = dom (Shift (F,k)) )
hereby :: according to FUNCT_1:def_4 ::_thesis: ( dom f = dom F & rng f = dom (Shift (F,k)) )
let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A4: x1 in dom f and
A5: x2 in dom f and
A6: f . x1 = f . x2 ; ::_thesis: x1 = 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; ::_thesis: verum
end;
thus dom f = dom F by A2; ::_thesis: rng f = dom (Shift (F,k))
A11: dom (Shift (F,k)) = { (m + k) where m is Element of NAT : m in dom F } by Def12;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: dom (Shift (F,k)) c= rng f
let y be set ; ::_thesis: ( y in rng f implies y in dom (Shift (F,k)) )
assume y in rng f ; ::_thesis: y in dom (Shift (F,k))
then consider x being set 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; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dom (Shift (F,k)) or y in rng f )
assume y in dom (Shift (F,k)) ; ::_thesis: y in rng f
then consider m being Element of 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 y in rng f by A2, A16, A17, A18, A19, FUNCT_1:def_3; ::_thesis: verum
end;
registration
let F be NAT -defined Function;
reduce Shift (F,0) to F;
reducibility
Shift (F,0) = F
proof
A1: dom F = { (m + 0) where m is Element of NAT : m in dom F }
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { (m + 0) where m is Element of NAT : m in dom F } c= dom F
let a be set ; ::_thesis: ( a in dom F implies a in { (m + 0) where m is Element of NAT : m in dom F } )
assume A2: a in dom F ; ::_thesis: a in { (m + 0) where m is Element of NAT : m in dom F }
then reconsider l = a as Element of NAT ;
a = l + 0 ;
hence a in { (m + 0) where m is Element of NAT : m in dom F } by A2; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (m + 0) where m is Element of NAT : m in dom F } or a in dom F )
assume a in { (m + 0) where m is Element of NAT : m in dom F } ; ::_thesis: a in dom F
then ex m being Element of NAT st
( a = m + 0 & m in dom F ) ;
hence a in dom F ; ::_thesis: verum
end;
for m being Element of NAT st m in dom F holds
F . (m + 0) = F . m ;
hence Shift (F,0) = F by A1, Def12; ::_thesis: verum
end;
end;
theorem :: VALUED_1:28
for F being NAT -defined Function holds Shift (F,0) = F ;
registration
let X be non empty set ;
let F be X -valued Function;
let k be Nat;
cluster Shift (F,k) -> X -valued ;
coherence
Shift (F,k) is X -valued
proof
A1: dom (Shift (F,k)) = { (m + k) where m is Element of NAT : m in dom F } by Def12;
thus rng (Shift (F,k)) c= X :: according to RELAT_1:def_19 ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (Shift (F,k)) or x in X )
assume x in rng (Shift (F,k)) ; ::_thesis: x in X
then consider y being set such that
A2: y in dom (Shift (F,k)) and
A3: x = (Shift (F,k)) . y by FUNCT_1:def_3;
consider m being Element of 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; ::_thesis: verum
end;
end;
end;
registration
cluster Relation-like NAT -defined Function-like non empty for set ;
existence
ex b1 being Function st
( not b1 is empty & b1 is NAT -defined )
proof
take id NAT ; ::_thesis: ( not id NAT is empty & id NAT is NAT -defined )
thus ( not id NAT is empty & id NAT is NAT -defined ) ; ::_thesis: verum
end;
end;
registration
let F be empty Function;
let k be Nat;
cluster Shift (F,k) -> empty ;
coherence
Shift (F,k) is empty
proof
A1: dom (Shift (F,k)) = { (m + k) where m is Element of NAT : m in dom F } by Def12;
assume not Shift (F,k) is empty ; ::_thesis: contradiction
then reconsider f = Shift (F,k) as non empty Function ;
not dom f is empty ;
then consider a being set such that
A2: a in dom (Shift (F,k)) by XBOOLE_0:def_1;
ex m being Element of NAT st
( a = m + k & m in dom F ) by A1, A2;
hence contradiction ; ::_thesis: verum
end;
end;
registration
let F be NAT -defined non empty Function;
let k be Nat;
cluster Shift (F,k) -> non empty ;
coherence
not Shift (F,k) is empty
proof
A1: dom (Shift (F,k)) = { (m + k) where m is Element of NAT : m in dom F } by Def12;
consider a being set such that
A2: a in dom F by XBOOLE_0:def_1;
reconsider a = a as Element of NAT by A2;
consider m being Nat such that
A3: a = m ;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
m + k in dom (Shift (F,k)) by A1, A2, A3;
hence not Shift (F,k) is empty ; ::_thesis: verum
end;
end;
theorem :: VALUED_1:29
for F being Function
for k being Nat st k > 0 holds
not 0 in dom (Shift (F,k))
proof
let F be Function; ::_thesis: for k being Nat st k > 0 holds
not 0 in dom (Shift (F,k))
let k be Nat; ::_thesis: ( k > 0 implies not 0 in dom (Shift (F,k)) )
assume that
A1: k > 0 and
A2: 0 in dom (Shift (F,k)) ; ::_thesis: contradiction
dom (Shift (F,k)) = { (m + k) where m is Element of NAT : m in dom F } by Def12;
then ex m being Element of NAT st
( 0 = m + k & m in dom F ) by A2;
hence contradiction by A1; ::_thesis: verum
end;
registration
cluster Relation-like NAT -defined Function-like non empty finite for set ;
existence
ex b1 being Function st
( b1 is NAT -defined & b1 is finite & not b1 is empty )
proof
take f = 0 .--> 0; ::_thesis: ( f is NAT -defined & f is finite & not f is empty )
dom f = {0} by FUNCOP_1:13;
hence dom f c= NAT by ZFMISC_1:31; :: according to RELAT_1:def_18 ::_thesis: ( f is finite & not f is empty )
thus ( f is finite & not f is empty ) ; ::_thesis: verum
end;
end;
registration
let F be NAT -defined Relation;
cluster dom F -> natural-membered ;
coherence
dom F is natural-membered ;
end;
definition
let F be NAT -defined non empty finite Function;
func LastLoc F -> Element of NAT equals :: VALUED_1:def 17
max (dom F);
coherence
max (dom F) is Element of NAT by ORDINAL1:def_12;
end;
:: deftheorem defines LastLoc VALUED_1:def_17_:_
for F being NAT -defined non empty finite Function holds LastLoc F = max (dom F);
definition
let F be NAT -defined non empty finite Function;
func CutLastLoc F -> Function equals :: VALUED_1:def 18
F \ ((LastLoc F) .--> (F . (LastLoc F)));
coherence
F \ ((LastLoc F) .--> (F . (LastLoc F))) is Function ;
end;
:: deftheorem defines CutLastLoc VALUED_1:def_18_:_
for F being NAT -defined non empty finite Function holds CutLastLoc F = F \ ((LastLoc F) .--> (F . (LastLoc F)));
registration
let F be NAT -defined non empty finite Function;
cluster CutLastLoc F -> NAT -defined finite ;
coherence
( CutLastLoc F is NAT -defined & CutLastLoc F is finite ) ;
end;
theorem Th30: :: VALUED_1:30
for F being NAT -defined non empty finite Function holds LastLoc F in dom F by XXREAL_2:def_8;
theorem :: VALUED_1:31
for F, G being NAT -defined non empty finite Function st F c= G holds
LastLoc F <= LastLoc G by RELAT_1:11, XXREAL_2:59;
theorem :: VALUED_1:32
for F being NAT -defined non empty finite Function
for l being Element of NAT st l in dom F holds
l <= LastLoc F by XXREAL_2:def_8;
definition
let F be NAT -defined non empty Function;
func FirstLoc F -> Element of NAT equals :: VALUED_1:def 19
min (dom F);
coherence
min (dom F) is Element of NAT by ORDINAL1:def_12;
end;
:: deftheorem defines FirstLoc VALUED_1:def_19_:_
for F being NAT -defined non empty Function holds FirstLoc F = min (dom F);
theorem :: VALUED_1:33
for F being NAT -defined non empty finite Function holds FirstLoc F in dom F by XXREAL_2:def_7;
theorem :: VALUED_1:34
for F, G being NAT -defined non empty finite Function st F c= G holds
FirstLoc G <= FirstLoc F by RELAT_1:11, XXREAL_2:60;
theorem :: VALUED_1:35
for l1 being Element of NAT
for F being NAT -defined non empty finite Function st l1 in dom F holds
FirstLoc F <= l1 by XXREAL_2:def_7;
theorem Th36: :: VALUED_1:36
for F being NAT -defined non empty finite Function holds dom (CutLastLoc F) = (dom F) \ {(LastLoc F)}
proof
let F be NAT -defined non empty finite Function; ::_thesis: dom (CutLastLoc F) = (dom F) \ {(LastLoc F)}
A1: dom ((LastLoc F) .--> (F . (LastLoc F))) = {(LastLoc F)} by FUNCOP_1:13;
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)} by FUNCOP_1:13;
thus dom (CutLastLoc F) c= (dom F) \ {(LastLoc F)} :: according to XBOOLE_0:def_10 ::_thesis: (dom F) \ {(LastLoc F)} c= dom (CutLastLoc F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (CutLastLoc F) or x in (dom F) \ {(LastLoc F)} )
assume x in dom (CutLastLoc F) ; ::_thesis: x in (dom F) \ {(LastLoc F)}
then consider y being set 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;
percases ( x <> LastLoc F or y <> F . (LastLoc F) ) by A5, TARSKI:def_1;
suppose x <> LastLoc F ; ::_thesis: x in (dom F) \ {(LastLoc F)}
then not x in dom R by A3, TARSKI:def_1;
hence x in (dom F) \ {(LastLoc F)} by A1, A2, A6, XBOOLE_0:def_5; ::_thesis: verum
end;
supposeA7: y <> F . (LastLoc F) ; ::_thesis: x in (dom F) \ {(LastLoc F)}
now__::_thesis:_not_x_in_dom_R
assume x in dom R ; ::_thesis: contradiction
then x = LastLoc F by A3, TARSKI:def_1;
hence contradiction by A4, A7, FUNCT_1:1; ::_thesis: verum
end;
hence x in (dom F) \ {(LastLoc F)} by A1, A2, A6, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
thus (dom F) \ {(LastLoc F)} c= dom (CutLastLoc F) by A1, RELAT_1:3; ::_thesis: verum
end;
theorem :: VALUED_1:37
for F being NAT -defined non empty finite Function holds dom F = (dom (CutLastLoc F)) \/ {(LastLoc F)}
proof
let F be NAT -defined non empty finite Function; ::_thesis: dom F = (dom (CutLastLoc F)) \/ {(LastLoc F)}
LastLoc F in dom F by Th30;
then A1: {(LastLoc F)} c= dom F by ZFMISC_1:31;
dom (CutLastLoc F) = (dom F) \ {(LastLoc F)} by Th36;
hence dom F = (dom (CutLastLoc F)) \/ {(LastLoc F)} by A1, XBOOLE_1:45; ::_thesis: verum
end;
registration
cluster Relation-like NAT -defined Function-like finite 1 -element for set ;
existence
ex b1 being Function st
( b1 is 1 -element & b1 is NAT -defined & b1 is finite )
proof
take 0 .--> 0 ; ::_thesis: ( 0 .--> 0 is 1 -element & 0 .--> 0 is NAT -defined & 0 .--> 0 is finite )
thus ( 0 .--> 0 is 1 -element & 0 .--> 0 is NAT -defined & 0 .--> 0 is finite ) ; ::_thesis: verum
end;
end;
registration
let F be NAT -defined finite 1 -element Function;
cluster CutLastLoc F -> empty ;
coherence
CutLastLoc F is empty
proof
LastLoc F in dom F by Th30;
then A1: [(LastLoc F),(F . (LastLoc F))] in F by FUNCT_1:def_2;
assume not CutLastLoc F is empty ; ::_thesis: contradiction
then consider a being set such that
A2: a in CutLastLoc F by XBOOLE_0:def_1;
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 contradiction by A3, TARSKI:def_1; ::_thesis: verum
end;
end;
theorem :: VALUED_1:38
for F being NAT -defined non empty finite Function holds card (CutLastLoc F) = (card F) - 1
proof
let F be NAT -defined non empty finite Function; ::_thesis: card (CutLastLoc F) = (card F) - 1
(LastLoc F) .--> (F . (LastLoc F)) c= F
proof
let a, b be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [a,b] in (LastLoc F) .--> (F . (LastLoc F)) or [a,b] in F )
assume [a,b] in (LastLoc F) .--> (F . (LastLoc F)) ; ::_thesis: [a,b] in 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 Th30;
hence [a,b] in F by A1, FUNCT_1:def_2; ::_thesis: verum
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 ;
::_thesis: verum
end;
begin
registration
let X be set ;
let f be X -defined complex-valued Function;
cluster - f -> X -defined complex-valued ;
coherence
- f is X -defined
proof
A1: dom (- f) = dom f by Def5;
thus dom (- f) c= X by A1; :: according to RELAT_1:def_18 ::_thesis: verum
end;
clusterf " -> X -defined complex-valued ;
coherence
f " is X -defined
proof
A2: dom (f ") = dom f by Def7;
thus dom (f ") c= X by A2; :: according to RELAT_1:def_18 ::_thesis: verum
end;
clusterf ^2 -> X -defined ;
coherence
f ^2 is X -defined
proof
A3: dom (f ^2) = dom f by Th11;
thus dom (f ^2) c= X by A3; :: according to RELAT_1:def_18 ::_thesis: verum
end;
cluster|.f.| -> X -defined real-valued ;
coherence
|.f.| is X -defined
proof
A4: dom |.f.| = dom f by Def11;
thus dom |.f.| c= X by A4; :: according to RELAT_1:def_18 ::_thesis: verum
end;
end;
registration
let X be set ;
cluster Relation-like X -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued for set ;
existence
ex b1 being X -defined natural-valued Function st b1 is total
proof
take the total PartFunc of X,NAT ; ::_thesis: the total PartFunc of X,NAT is total
thus the total PartFunc of X,NAT is total ; ::_thesis: verum
end;
end;
registration
let X be set ;
let f be X -defined total complex-valued Function;
cluster - f -> total complex-valued ;
coherence
- f is total
proof
A1: dom (- f) = dom f by Def5;
dom f = X by PARTFUN1:def_2;
hence - f is total by A1, PARTFUN1:def_2; ::_thesis: verum
end;
clusterf " -> total complex-valued ;
coherence
f " is total
proof
A2: dom (f ") = dom f by Def7;
dom f = X by PARTFUN1:def_2;
hence f " is total by A2, PARTFUN1:def_2; ::_thesis: verum
end;
clusterf ^2 -> total ;
coherence
f ^2 is total
proof
A3: dom (f ^2) = dom f by Th11;
dom f = X by PARTFUN1:def_2;
hence f ^2 is total by A3, PARTFUN1:def_2; ::_thesis: verum
end;
cluster|.f.| -> total real-valued ;
coherence
|.f.| is total
proof
A4: dom |.f.| = dom f by Def11;
dom f = X by PARTFUN1:def_2;
hence |.f.| is total by A4, PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let X be set ;
let f be X -defined complex-valued Function;
let r be complex number ;
clusterr + f -> X -defined ;
coherence
r + f is X -defined
proof
A1: dom (r + f) = dom f by Def2;
thus dom (r + f) c= X by A1; :: according to RELAT_1:def_18 ::_thesis: verum
end;
clusterf - r -> X -defined ;
coherence
f - r is X -defined ;
clusterr (#) f -> X -defined ;
coherence
r (#) f is X -defined
proof
A2: dom (r (#) f) = dom f by Def5;
thus dom (r (#) f) c= X by A2; :: according to RELAT_1:def_18 ::_thesis: verum
end;
end;
registration
let X be set ;
let f be X -defined total complex-valued Function;
let r be complex number ;
clusterr + f -> total ;
coherence
r + f is total
proof
A1: dom (r + f) = dom f by Def2;
dom f = X by PARTFUN1:def_2;
hence r + f is total by A1, PARTFUN1:def_2; ::_thesis: verum
end;
clusterf - r -> total ;
coherence
f - r is total ;
clusterr (#) f -> total ;
coherence
r (#) f is total
proof
A2: dom (r (#) f) = dom f by Def5;
dom f = X by PARTFUN1:def_2;
hence r (#) f is total by A2, PARTFUN1:def_2; ::_thesis: verum
end;
end;
registration
let X be set ;
let f1 be complex-valued Function;
let f2 be X -defined complex-valued Function;
clusterf1 + f2 -> X -defined ;
coherence
f1 + f2 is X -defined
proof
dom (f1 + f2) = (dom f1) /\ (dom f2) by Def1;
then A1: dom (f1 + f2) c= dom f2 by XBOOLE_1:17;
thus dom (f1 + f2) c= X by A1, XBOOLE_1:1; :: according to RELAT_1:def_18 ::_thesis: verum
end;
clusterf1 - f2 -> X -defined ;
coherence
f1 - f2 is X -defined ;
clusterf1 (#) f2 -> X -defined ;
coherence
f1 (#) f2 is X -defined
proof
dom (f1 (#) f2) = (dom f1) /\ (dom f2) by Def4;
then A2: dom (f1 (#) f2) c= dom f2 by XBOOLE_1:17;
thus dom (f1 (#) f2) c= X by A2, XBOOLE_1:1; :: according to RELAT_1:def_18 ::_thesis: verum
end;
clusterf1 /" f2 -> X -defined ;
coherence
f1 /" f2 is X -defined ;
end;
registration
let X be set ;
let f1, f2 be X -defined total complex-valued Function;
clusterf1 + f2 -> total ;
coherence
f1 + f2 is total
proof
A1: dom (f1 + f2) = (dom f1) /\ (dom f2) by Def1;
( dom f1 = X & dom f2 = X ) by PARTFUN1:def_2;
hence f1 + f2 is total by A1, PARTFUN1:def_2; ::_thesis: verum
end;
clusterf1 - f2 -> total ;
coherence
f1 - f2 is total ;
clusterf1 (#) f2 -> total ;
coherence
f1 (#) f2 is total
proof
A2: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by Def4;
( dom f1 = X & dom f2 = X ) by PARTFUN1:def_2;
hence f1 (#) f2 is total by A2, PARTFUN1:def_2; ::_thesis: verum
end;
clusterf1 /" f2 -> total ;
coherence
f1 /" f2 is total ;
end;
registration
let X be non empty set ;
let F be NAT -defined X -valued non empty finite Function;
cluster CutLastLoc F -> X -valued ;
coherence
CutLastLoc F is X -valued ;
end;
theorem :: VALUED_1:39
for f being Function
for i, n being Nat st i in dom (Shift (f,n)) holds
ex j being Nat st
( j in dom f & i = j + n )
proof
let f be Function; ::_thesis: for i, n being Nat st i in dom (Shift (f,n)) holds
ex j being Nat st
( j in dom f & i = j + n )
let i, n be Nat; ::_thesis: ( i in dom (Shift (f,n)) implies ex j being Nat st
( j in dom f & i = j + n ) )
A: dom (Shift (f,n)) = { (m + n) where m is Element of NAT : m in dom f } by Def12;
assume i in dom (Shift (f,n)) ; ::_thesis: ex j being Nat st
( j in dom f & i = j + n )
then ex m being Element of NAT st
( i = m + n & m in dom f ) by A;
hence ex j being Nat st
( j in dom f & i = j + n ) ; ::_thesis: verum
end;