:: by Library Committee

::

:: Received December 18, 2007

:: Copyright (c) 2007-2012 Association of Mizar Users

begin

Lm1: for f being FinSequence

for h being Function st dom h = dom f holds

h is FinSequence

proof end;

Lm2: for f, g being FinSequence

for h being Function st dom h = (dom f) /\ (dom g) holds

h is FinSequence

proof end;

:: move somewhere

registration
end;

definition

let f1, f2 be complex-valued Function;

deffunc H_{1}( set ) -> set = (f1 . $1) + (f2 . $1);

set X = (dom f1) /\ (dom f2);

ex b_{1} being Function st

( dom b_{1} = (dom f1) /\ (dom f2) & ( for c being set st c in dom b_{1} holds

b_{1} . c = (f1 . c) + (f2 . c) ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom f1) /\ (dom f2) & ( for c being set st c in dom b_{1} holds

b_{1} . c = (f1 . c) + (f2 . c) ) & dom b_{2} = (dom f1) /\ (dom f2) & ( for c being set st c in dom b_{2} holds

b_{2} . c = (f1 . c) + (f2 . c) ) holds

b_{1} = b_{2}

for b_{1} being Function

for f1, f2 being complex-valued Function st dom b_{1} = (dom f1) /\ (dom f2) & ( for c being set st c in dom b_{1} holds

b_{1} . c = (f1 . c) + (f2 . c) ) holds

( dom b_{1} = (dom f2) /\ (dom f1) & ( for c being set st c in dom b_{1} holds

b_{1} . c = (f2 . c) + (f1 . c) ) )
;

end;
deffunc H

set X = (dom f1) /\ (dom f2);

func f1 + 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 ( dom it = (dom f1) /\ (dom f2) & ( for c being set st c in dom it holds

it . c = (f1 . c) + (f2 . c) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

commutativity for b

for f1, f2 being complex-valued Function st dom b

b

( dom b

b

:: deftheorem Def1 defines + VALUED_1:def 1 :

for f1, f2 being complex-valued Function

for b_{3} being Function holds

( b_{3} = f1 + f2 iff ( dom b_{3} = (dom f1) /\ (dom f2) & ( for c being set st c in dom b_{3} holds

b_{3} . c = (f1 . c) + (f2 . c) ) ) );

for f1, f2 being complex-valued Function

for b

( b

b

registration
end;

registration
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 func f1 + f2 -> PartFunc of C,COMPLEX;

coherence

f1 + f2 is PartFunc of C,COMPLEX

end;
let D1, D2 be complex-membered set ;

let f1 be PartFunc of C,D1;

let f2 be PartFunc of C,D2;

:: original: +

redefine func f1 + f2 -> PartFunc of C,COMPLEX;

coherence

f1 + f2 is PartFunc of C,COMPLEX

proof 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 func f1 + f2 -> PartFunc of C,REAL;

coherence

f1 + f2 is PartFunc of C,REAL

end;
let D1, D2 be real-membered set ;

let f1 be PartFunc of C,D1;

let f2 be PartFunc of C,D2;

:: original: +

redefine func f1 + f2 -> PartFunc of C,REAL;

coherence

f1 + f2 is PartFunc of C,REAL

proof 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 func f1 + f2 -> PartFunc of C,RAT;

coherence

f1 + f2 is PartFunc of C,RAT

end;
let D1, D2 be rational-membered set ;

let f1 be PartFunc of C,D1;

let f2 be PartFunc of C,D2;

:: original: +

redefine func f1 + f2 -> PartFunc of C,RAT;

coherence

f1 + f2 is PartFunc of C,RAT

proof 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 func f1 + f2 -> PartFunc of C,INT;

coherence

f1 + f2 is PartFunc of C,INT

end;
let D1, D2 be integer-membered set ;

let f1 be PartFunc of C,D1;

let f2 be PartFunc of C,D2;

:: original: +

redefine func f1 + f2 -> PartFunc of C,INT;

coherence

f1 + f2 is PartFunc of C,INT

proof 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 func f1 + f2 -> PartFunc of C,NAT;

coherence

f1 + f2 is PartFunc of C,NAT

end;
let D1, D2 be natural-membered set ;

let f1 be PartFunc of C,D1;

let f2 be PartFunc of C,D2;

:: original: +

redefine func f1 + f2 -> PartFunc of C,NAT;

coherence

f1 + f2 is PartFunc of C,NAT

proof 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;

coherence

for b_{1} being PartFunc of C,COMPLEX st b_{1} = f1 + f2 holds

b_{1} is total

end;
let D1, D2 be non empty complex-membered set ;

let f1 be Function of C,D1;

let f2 be Function of C,D2;

coherence

for b

b

proof 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;

coherence

for b_{1} being PartFunc of C,REAL st b_{1} = f1 + f2 holds

b_{1} is total

end;
let D1, D2 be non empty real-membered set ;

let f1 be Function of C,D1;

let f2 be Function of C,D2;

coherence

for b

b

proof 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;

coherence

for b_{1} being PartFunc of C,RAT st b_{1} = f1 + f2 holds

b_{1} is total

end;
let D1, D2 be non empty rational-membered set ;

let f1 be Function of C,D1;

let f2 be Function of C,D2;

coherence

for b

b

proof 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;

coherence

for b_{1} being PartFunc of C,INT st b_{1} = f1 + f2 holds

b_{1} is total

end;
let D1, D2 be non empty integer-membered set ;

let f1 be Function of C,D1;

let f2 be Function of C,D2;

coherence

for b

b

proof 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;

coherence

for b_{1} being PartFunc of C,NAT st b_{1} = f1 + f2 holds

b_{1} is total

end;
let D1, D2 be non empty natural-membered set ;

let f1 be Function of C,D1;

let f2 be Function of C,D2;

coherence

for b

b

proof 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)

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 end;

registration
end;

begin

definition

let f be complex-valued Function;

let r be complex number ;

deffunc H_{1}( set ) -> set = r + (f . $1);

ex b_{1} being Function st

( dom b_{1} = dom f & ( for c being set st c in dom b_{1} holds

b_{1} . c = r + (f . c) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for c being set st c in dom b_{1} holds

b_{1} . c = r + (f . c) ) & dom b_{2} = dom f & ( for c being set st c in dom b_{2} holds

b_{2} . c = r + (f . c) ) holds

b_{1} = b_{2}

end;
let r be complex number ;

deffunc H

func r + 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 ( dom it = dom f & ( for c being set st c in dom it holds

it . c = r + (f . c) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines + VALUED_1:def 2 :

for f being complex-valued Function

for r being complex number

for b_{3} being Function holds

( b_{3} = r + f iff ( dom b_{3} = dom f & ( for c being set st c in dom b_{3} holds

b_{3} . c = r + (f . c) ) ) );

for f being complex-valued Function

for r being complex number

for b

( b

b

registration

let f be complex-valued Function;

let r be complex number ;

coherence

r + f is complex-valued

end;
let r be complex number ;

coherence

r + f is complex-valued

proof end;

registration
end;

registration
end;

registration
end;

registration
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 func r + f -> PartFunc of C,COMPLEX;

coherence

r + f is PartFunc of C,COMPLEX

end;
let D be complex-membered set ;

let f be PartFunc of C,D;

let r be complex number ;

:: original: +

redefine func r + f -> PartFunc of C,COMPLEX;

coherence

r + f is PartFunc of C,COMPLEX

proof 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 func r + f -> PartFunc of C,REAL;

coherence

r + f is PartFunc of C,REAL

end;
let D be real-membered set ;

let f be PartFunc of C,D;

let r be real number ;

:: original: +

redefine func r + f -> PartFunc of C,REAL;

coherence

r + f is PartFunc of C,REAL

proof 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 func r + f -> PartFunc of C,RAT;

coherence

r + f is PartFunc of C,RAT

end;
let D be rational-membered set ;

let f be PartFunc of C,D;

let r be rational number ;

:: original: +

redefine func r + f -> PartFunc of C,RAT;

coherence

r + f is PartFunc of C,RAT

proof 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 func r + f -> PartFunc of C,INT;

coherence

r + f is PartFunc of C,INT

end;
let D be integer-membered set ;

let f be PartFunc of C,D;

let r be integer number ;

:: original: +

redefine func r + f -> PartFunc of C,INT;

coherence

r + f is PartFunc of C,INT

proof 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 func r + f -> PartFunc of C,NAT;

coherence

r + f is PartFunc of C,NAT

end;
let D be natural-membered set ;

let f be PartFunc of C,D;

let r be Nat;

:: original: +

redefine func r + f -> PartFunc of C,NAT;

coherence

r + f is PartFunc of C,NAT

proof 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 ;

coherence

for b_{1} being PartFunc of C,COMPLEX st b_{1} = r + f holds

b_{1} is total

end;
let D be non empty complex-membered set ;

let f be Function of C,D;

let r be complex number ;

coherence

for b

b

proof 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 ;

coherence

for b_{1} being PartFunc of C,REAL st b_{1} = r + f holds

b_{1} is total

end;
let D be non empty real-membered set ;

let f be Function of C,D;

let r be real number ;

coherence

for b

b

proof 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 ;

coherence

for b_{1} being PartFunc of C,RAT st b_{1} = r + f holds

b_{1} is total

end;
let D be non empty rational-membered set ;

let f be Function of C,D;

let r be rational number ;

coherence

for b

b

proof 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 ;

coherence

for b_{1} being PartFunc of C,INT st b_{1} = r + f holds

b_{1} is total

end;
let D be non empty integer-membered set ;

let f be Function of C,D;

let r be integer number ;

coherence

for b

b

proof 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;

coherence

for b_{1} being PartFunc of C,NAT st b_{1} = r + f holds

b_{1} is total

end;
let D be non empty natural-membered set ;

let f be Function of C,D;

let r be Nat;

coherence

for b

b

proof 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)

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 end;

registration

let f be complex-valued FinSequence;

let r be complex number ;

coherence

r + f is FinSequence-like

end;
let r be complex number ;

coherence

r + f is FinSequence-like

proof end;

begin

definition
end;

:: deftheorem defines - VALUED_1:def 3 :

for f being complex-valued Function

for r being complex number holds f - r = (- r) + f;

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 ) )

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 end;

registration
end;

registration
end;

registration
end;

registration
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 func f - r -> PartFunc of C,COMPLEX;

coherence

f - r is PartFunc of C,COMPLEX

end;
let D be complex-membered set ;

let f be PartFunc of C,D;

let r be complex number ;

:: original: -

redefine func f - r -> PartFunc of C,COMPLEX;

coherence

f - r is PartFunc of C,COMPLEX

proof 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 func f - r -> PartFunc of C,REAL;

coherence

f - r is PartFunc of C,REAL

end;
let D be real-membered set ;

let f be PartFunc of C,D;

let r be real number ;

:: original: -

redefine func f - r -> PartFunc of C,REAL;

coherence

f - r is PartFunc of C,REAL

proof 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 func f - r -> PartFunc of C,RAT;

coherence

f - r is PartFunc of C,RAT

end;
let D be rational-membered set ;

let f be PartFunc of C,D;

let r be rational number ;

:: original: -

redefine func f - r -> PartFunc of C,RAT;

coherence

f - r is PartFunc of C,RAT

proof 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 func f - r -> PartFunc of C,INT;

coherence

f - r is PartFunc of C,INT

end;
let D be integer-membered set ;

let f be PartFunc of C,D;

let r be integer number ;

:: original: -

redefine func f - r -> PartFunc of C,INT;

coherence

f - r is PartFunc of C,INT

proof 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 ;

coherence

for b_{1} being PartFunc of C,COMPLEX st b_{1} = f - r holds

b_{1} is total
;

end;
let D be non empty complex-membered set ;

let f be Function of C,D;

let r be complex number ;

coherence

for b

b

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 ;

coherence

for b_{1} being PartFunc of C,REAL st b_{1} = f - r holds

b_{1} is total
;

end;
let D be non empty real-membered set ;

let f be Function of C,D;

let r be real number ;

coherence

for b

b

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 ;

coherence

for b_{1} being PartFunc of C,RAT st b_{1} = f - r holds

b_{1} is total
;

end;
let D be non empty rational-membered set ;

let f be Function of C,D;

let r be rational number ;

coherence

for b

b

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 ;

coherence

for b_{1} being PartFunc of C,INT st b_{1} = f - r holds

b_{1} is total
;

end;
let D be non empty integer-membered set ;

let f be Function of C,D;

let r be integer number ;

coherence

for b

b

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

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 end;

registration
end;

begin

definition

let f1, f2 be complex-valued Function;

deffunc H_{1}( set ) -> set = (f1 . $1) * (f2 . $1);

set X = (dom f1) /\ (dom f2);

ex b_{1} being Function st

( dom b_{1} = (dom f1) /\ (dom f2) & ( for c being set st c in dom b_{1} holds

b_{1} . c = (f1 . c) * (f2 . c) ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom f1) /\ (dom f2) & ( for c being set st c in dom b_{1} holds

b_{1} . c = (f1 . c) * (f2 . c) ) & dom b_{2} = (dom f1) /\ (dom f2) & ( for c being set st c in dom b_{2} holds

b_{2} . c = (f1 . c) * (f2 . c) ) holds

b_{1} = b_{2}

for b_{1} being Function

for f1, f2 being complex-valued Function st dom b_{1} = (dom f1) /\ (dom f2) & ( for c being set st c in dom b_{1} holds

b_{1} . c = (f1 . c) * (f2 . c) ) holds

( dom b_{1} = (dom f2) /\ (dom f1) & ( for c being set st c in dom b_{1} holds

b_{1} . c = (f2 . c) * (f1 . c) ) )
;

end;
deffunc H

set X = (dom f1) /\ (dom f2);

func f1 (#) 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 ( dom it = (dom f1) /\ (dom f2) & ( for c being set st c in dom it holds

it . c = (f1 . c) * (f2 . c) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

commutativity for b

for f1, f2 being complex-valued Function st dom b

b

( dom b

b

:: deftheorem Def4 defines (#) VALUED_1:def 4 :

for f1, f2 being complex-valued Function

for b_{3} being Function holds

( b_{3} = f1 (#) f2 iff ( dom b_{3} = (dom f1) /\ (dom f2) & ( for c being set st c in dom b_{3} holds

b_{3} . c = (f1 . c) * (f2 . c) ) ) );

for f1, f2 being complex-valued Function

for b

( b

b

theorem :: VALUED_1:5

for f1, f2 being complex-valued Function

for c being set holds (f1 (#) f2) . c = (f1 . c) * (f2 . c)

for c being set holds (f1 (#) f2) . c = (f1 . c) * (f2 . c)

proof end;

registration
end;

registration
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 func f1 (#) f2 -> PartFunc of C,COMPLEX;

coherence

f1 (#) f2 is PartFunc of C,COMPLEX

end;
let D1, D2 be complex-membered set ;

let f1 be PartFunc of C,D1;

let f2 be PartFunc of C,D2;

:: original: (#)

redefine func f1 (#) f2 -> PartFunc of C,COMPLEX;

coherence

f1 (#) f2 is PartFunc of C,COMPLEX

proof 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 func f1 (#) f2 -> PartFunc of C,REAL;

coherence

f1 (#) f2 is PartFunc of C,REAL

end;
let D1, D2 be real-membered set ;

let f1 be PartFunc of C,D1;

let f2 be PartFunc of C,D2;

:: original: (#)

redefine func f1 (#) f2 -> PartFunc of C,REAL;

coherence

f1 (#) f2 is PartFunc of C,REAL

proof 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 func f1 (#) f2 -> PartFunc of C,RAT;

coherence

f1 (#) f2 is PartFunc of C,RAT

end;
let D1, D2 be rational-membered set ;

let f1 be PartFunc of C,D1;

let f2 be PartFunc of C,D2;

:: original: (#)

redefine func f1 (#) f2 -> PartFunc of C,RAT;

coherence

f1 (#) f2 is PartFunc of C,RAT

proof 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 func f1 (#) f2 -> PartFunc of C,INT;

coherence

f1 (#) f2 is PartFunc of C,INT

end;
let D1, D2 be integer-membered set ;

let f1 be PartFunc of C,D1;

let f2 be PartFunc of C,D2;

:: original: (#)

redefine func f1 (#) f2 -> PartFunc of C,INT;

coherence

f1 (#) f2 is PartFunc of C,INT

proof 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 func f1 (#) f2 -> PartFunc of C,NAT;

coherence

f1 (#) f2 is PartFunc of C,NAT

end;
let D1, D2 be natural-membered set ;

let f1 be PartFunc of C,D1;

let f2 be PartFunc of C,D2;

:: original: (#)

redefine func f1 (#) f2 -> PartFunc of C,NAT;

coherence

f1 (#) f2 is PartFunc of C,NAT

proof 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;

coherence

for b_{1} being PartFunc of C,COMPLEX st b_{1} = f1 (#) f2 holds

b_{1} is total

end;
let D1, D2 be non empty complex-membered set ;

let f1 be Function of C,D1;

let f2 be Function of C,D2;

coherence

for b

b

proof 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;

coherence

for b_{1} being PartFunc of C,REAL st b_{1} = f1 (#) f2 holds

b_{1} is total

end;
let D1, D2 be non empty real-membered set ;

let f1 be Function of C,D1;

let f2 be Function of C,D2;

coherence

for b

b

proof 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;

coherence

for b_{1} being PartFunc of C,RAT st b_{1} = f1 (#) f2 holds

b_{1} is total

end;
let D1, D2 be non empty rational-membered set ;

let f1 be Function of C,D1;

let f2 be Function of C,D2;

coherence

for b

b

proof 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;

coherence

for b_{1} being PartFunc of C,INT st b_{1} = f1 (#) f2 holds

b_{1} is total

end;
let D1, D2 be non empty integer-membered set ;

let f1 be Function of C,D1;

let f2 be Function of C,D2;

coherence

for b

b

proof 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;

coherence

for b_{1} being PartFunc of C,NAT st b_{1} = f1 (#) f2 holds

b_{1} is total

end;
let D1, D2 be non empty natural-membered set ;

let f1 be Function of C,D1;

let f2 be Function of C,D2;

coherence

for b

b

proof end;

registration
end;

begin

definition

let f be complex-valued Function;

let r be complex number ;

deffunc H_{1}( set ) -> set = r * (f . $1);

ex b_{1} being Function st

( dom b_{1} = dom f & ( for c being set st c in dom b_{1} holds

b_{1} . c = r * (f . c) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for c being set st c in dom b_{1} holds

b_{1} . c = r * (f . c) ) & dom b_{2} = dom f & ( for c being set st c in dom b_{2} holds

b_{2} . c = r * (f . c) ) holds

b_{1} = b_{2}

end;
let r be complex number ;

deffunc H

func r (#) 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 ( dom it = dom f & ( for c being set st c in dom it holds

it . c = r * (f . c) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines (#) VALUED_1:def 5 :

for f being complex-valued Function

for r being complex number

for b_{3} being Function holds

( b_{3} = r (#) f iff ( dom b_{3} = dom f & ( for c being set st c in dom b_{3} holds

b_{3} . c = r * (f . c) ) ) );

for f being complex-valued Function

for r being complex number

for b

( b

b

notation
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)

for r being complex number

for c being set holds (r (#) f) . c = r * (f . c)

proof end;

registration

let f be complex-valued Function;

let r be complex number ;

coherence

r (#) f is complex-valued

end;
let r be complex number ;

coherence

r (#) f is complex-valued

proof end;

registration
end;

registration

let f be RAT -valued Function;

let r be rational number ;

coherence

r (#) f is RAT -valued

end;
let r be rational number ;

coherence

r (#) f is RAT -valued

proof end;

registration
end;

registration
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 func r (#) f -> PartFunc of C,COMPLEX;

coherence

r (#) f is PartFunc of C,COMPLEX

end;
let D be complex-membered set ;

let f be PartFunc of C,D;

let r be complex number ;

:: original: (#)

redefine func r (#) f -> PartFunc of C,COMPLEX;

coherence

r (#) f is PartFunc of C,COMPLEX

proof 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 func r (#) f -> PartFunc of C,REAL;

coherence

r (#) f is PartFunc of C,REAL

end;
let D be real-membered set ;

let f be PartFunc of C,D;

let r be real number ;

:: original: (#)

redefine func r (#) f -> PartFunc of C,REAL;

coherence

r (#) f is PartFunc of C,REAL

proof 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 func r (#) f -> PartFunc of C,RAT;

coherence

r (#) f is PartFunc of C,RAT

end;
let D be rational-membered set ;

let f be PartFunc of C,D;

let r be rational number ;

:: original: (#)

redefine func r (#) f -> PartFunc of C,RAT;

coherence

r (#) f is PartFunc of C,RAT

proof 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 func r (#) f -> PartFunc of C,INT;

coherence

r (#) f is PartFunc of C,INT

end;
let D be integer-membered set ;

let f be PartFunc of C,D;

let r be integer number ;

:: original: (#)

redefine func r (#) f -> PartFunc of C,INT;

coherence

r (#) f is PartFunc of C,INT

proof 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 func r (#) f -> PartFunc of C,NAT;

coherence

r (#) f is PartFunc of C,NAT

end;
let D be natural-membered set ;

let f be PartFunc of C,D;

let r be Nat;

:: original: (#)

redefine func r (#) f -> PartFunc of C,NAT;

coherence

r (#) f is PartFunc of C,NAT

proof 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 ;

coherence

for b_{1} being PartFunc of C,COMPLEX st b_{1} = r (#) f holds

b_{1} is total

end;
let D be non empty complex-membered set ;

let f be Function of C,D;

let r be complex number ;

coherence

for b

b

proof 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 ;

coherence

for b_{1} being PartFunc of C,REAL st b_{1} = r (#) f holds

b_{1} is total

end;
let D be non empty real-membered set ;

let f be Function of C,D;

let r be real number ;

coherence

for b

b

proof 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 ;

coherence

for b_{1} being PartFunc of C,RAT st b_{1} = r (#) f holds

b_{1} is total

end;
let D be non empty rational-membered set ;

let f be Function of C,D;

let r be rational number ;

coherence

for b

b

proof 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 ;

coherence

for b_{1} being PartFunc of C,INT st b_{1} = r (#) f holds

b_{1} is total

end;
let D be non empty integer-membered set ;

let f be Function of C,D;

let r be integer number ;

coherence

for b

b

proof 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;

coherence

for b_{1} being PartFunc of C,NAT st b_{1} = r (#) f holds

b_{1} is total

end;
let D be non empty natural-membered set ;

let f be Function of C,D;

let r be Nat;

coherence

for b

b

proof 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

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 end;

registration

let f be complex-valued FinSequence;

let r be complex number ;

coherence

r (#) f is FinSequence-like

end;
let r be complex number ;

coherence

r (#) f is FinSequence-like

proof end;

begin

definition

let f be complex-valued Function;

coherence

(- 1) (#) f is complex-valued Function ;

involutiveness

for b_{1}, b_{2} being complex-valued Function st b_{1} = (- 1) (#) b_{2} holds

b_{2} = (- 1) (#) b_{1}

end;
coherence

(- 1) (#) f is complex-valued Function ;

involutiveness

for b

b

proof end;

:: deftheorem defines - VALUED_1:def 6 :

for f being complex-valued Function holds - f = (- 1) (#) f;

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) ) )

( dom (- f) = dom f & ( for c being set holds (- f) . c = - (f . c) ) )

proof 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

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 end;

registration
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

end;
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 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

end;
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 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

end;
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 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

end;
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 end;

registration

let C be set ;

let D be non empty complex-membered set ;

let f be Function of C,D;

coherence

for b_{1} being PartFunc of C,COMPLEX st b_{1} = - f holds

b_{1} is total
;

end;
let D be non empty complex-membered set ;

let f be Function of C,D;

coherence

for b

b

registration

let C be set ;

let D be non empty real-membered set ;

let f be Function of C,D;

coherence

for b_{1} being PartFunc of C,REAL st b_{1} = - f holds

b_{1} is total
;

end;
let D be non empty real-membered set ;

let f be Function of C,D;

coherence

for b

b

registration

let C be set ;

let D be non empty rational-membered set ;

let f be Function of C,D;

coherence

for b_{1} being PartFunc of C,RAT st b_{1} = - f holds

b_{1} is total
;

end;
let D be non empty rational-membered set ;

let f be Function of C,D;

coherence

for b

b

registration

let C be set ;

let D be non empty integer-membered set ;

let f be Function of C,D;

coherence

for b_{1} being PartFunc of C,INT st b_{1} = - f holds

b_{1} is total
;

end;
let D be non empty integer-membered set ;

let f be Function of C,D;

coherence

for b

b

begin

definition

let f be complex-valued Function;

deffunc H_{1}( set ) -> set = (f . $1) " ;

ex b_{1} being complex-valued Function st

( dom b_{1} = dom f & ( for c being set st c in dom b_{1} holds

b_{1} . c = (f . c) " ) )

for b_{1}, b_{2} being complex-valued Function st dom b_{1} = dom f & ( for c being set st c in dom b_{1} holds

b_{1} . c = (f . c) " ) & dom b_{2} = dom f & ( for c being set st c in dom b_{2} holds

b_{2} . c = (f . c) " ) holds

b_{1} = b_{2}

for b_{1}, b_{2} being complex-valued Function st dom b_{1} = dom b_{2} & ( for c being set st c in dom b_{1} holds

b_{1} . c = (b_{2} . c) " ) holds

( dom b_{2} = dom b_{1} & ( for c being set st c in dom b_{2} holds

b_{2} . c = (b_{1} . c) " ) )

end;
deffunc H

func f " -> 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 ( dom it = dom f & ( for c being set st c in dom it holds

it . c = (f . c) " ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

involutiveness for b

b

( dom b

b

proof end;

:: deftheorem Def7 defines " VALUED_1:def 7 :

for f, b_{2} being complex-valued Function holds

( b_{2} = f " iff ( dom b_{2} = dom f & ( for c being set st c in dom b_{2} holds

b_{2} . c = (f . c) " ) ) );

for f, b

( b

b

::better name

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

end;
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 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

end;
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 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

end;
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 end;

registration

let C be set ;

let D be non empty complex-membered set ;

let f be Function of C,D;

coherence

for b_{1} being PartFunc of C,COMPLEX st b_{1} = f " holds

b_{1} is total

end;
let D be non empty complex-membered set ;

let f be Function of C,D;

coherence

for b

b

proof end;

registration

let C be set ;

let D be non empty real-membered set ;

let f be Function of C,D;

coherence

for b_{1} being PartFunc of C,REAL st b_{1} = f " holds

b_{1} is total

end;
let D be non empty real-membered set ;

let f be Function of C,D;

coherence

for b

b

proof end;

registration

let C be set ;

let D be non empty rational-membered set ;

let f be Function of C,D;

coherence

for b_{1} being PartFunc of C,RAT st b_{1} = f " holds

b_{1} is total

end;
let D be non empty rational-membered set ;

let f be Function of C,D;

coherence

for b

b

proof end;

begin

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 ) )

( dom (f ^2) = dom f & ( for c being set holds (f ^2) . c = (f . c) ^2 ) )

proof end;

registration
end;

registration
end;

registration
end;

definition

let C be set ;

let D be complex-membered set ;

let f be PartFunc of C,D;

:: original: ^2

redefine func f ^2 -> PartFunc of C,COMPLEX;

coherence

f ^2 is PartFunc of C,COMPLEX

end;
let D be complex-membered set ;

let f be PartFunc of C,D;

:: original: ^2

redefine func f ^2 -> PartFunc of C,COMPLEX;

coherence

f ^2 is PartFunc of C,COMPLEX

proof end;

definition

let C be set ;

let D be real-membered set ;

let f be PartFunc of C,D;

:: original: ^2

redefine func f ^2 -> PartFunc of C,REAL;

coherence

f ^2 is PartFunc of C,REAL

end;
let D be real-membered set ;

let f be PartFunc of C,D;

:: original: ^2

redefine func f ^2 -> PartFunc of C,REAL;

coherence

f ^2 is PartFunc of C,REAL

proof end;

definition

let C be set ;

let D be rational-membered set ;

let f be PartFunc of C,D;

:: original: ^2

redefine func f ^2 -> PartFunc of C,RAT;

coherence

f ^2 is PartFunc of C,RAT

end;
let D be rational-membered set ;

let f be PartFunc of C,D;

:: original: ^2

redefine func f ^2 -> PartFunc of C,RAT;

coherence

f ^2 is PartFunc of C,RAT

proof end;

definition

let C be set ;

let D be integer-membered set ;

let f be PartFunc of C,D;

:: original: ^2

redefine func f ^2 -> PartFunc of C,INT;

coherence

f ^2 is PartFunc of C,INT

end;
let D be integer-membered set ;

let f be PartFunc of C,D;

:: original: ^2

redefine func f ^2 -> PartFunc of C,INT;

coherence

f ^2 is PartFunc of C,INT

proof end;

definition

let C be set ;

let D be natural-membered set ;

let f be PartFunc of C,D;

:: original: ^2

redefine func f ^2 -> PartFunc of C,NAT;

coherence

f ^2 is PartFunc of C,NAT

end;
let D be natural-membered set ;

let f be PartFunc of C,D;

:: original: ^2

redefine func f ^2 -> PartFunc of C,NAT;

coherence

f ^2 is PartFunc of C,NAT

proof end;

registration

let C be set ;

let D be non empty complex-membered set ;

let f be Function of C,D;

coherence

for b_{1} being PartFunc of C,COMPLEX st b_{1} = f ^2 holds

b_{1} is total
;

end;
let D be non empty complex-membered set ;

let f be Function of C,D;

coherence

for b

b

registration

let C be set ;

let D be non empty real-membered set ;

let f be Function of C,D;

coherence

for b_{1} being PartFunc of C,REAL st b_{1} = f ^2 holds

b_{1} is total
;

end;
let D be non empty real-membered set ;

let f be Function of C,D;

coherence

for b

b

registration

let C be set ;

let D be non empty rational-membered set ;

let f be Function of C,D;

coherence

for b_{1} being PartFunc of C,RAT st b_{1} = f ^2 holds

b_{1} is total
;

end;
let D be non empty rational-membered set ;

let f be Function of C,D;

coherence

for b

b

registration

let C be set ;

let D be non empty integer-membered set ;

let f be Function of C,D;

coherence

for b_{1} being PartFunc of C,INT st b_{1} = f ^2 holds

b_{1} is total
;

end;
let D be non empty integer-membered set ;

let f be Function of C,D;

coherence

for b

b

registration

let C be set ;

let D be non empty natural-membered set ;

let f be Function of C,D;

coherence

for b_{1} being PartFunc of C,NAT st b_{1} = f ^2 holds

b_{1} is total
;

end;
let D be non empty natural-membered set ;

let f be Function of C,D;

coherence

for b

b

begin

:: deftheorem defines - VALUED_1:def 9 :

for f1, f2 being complex-valued Function holds f1 - f2 = f1 + (- f2);

for f1, f2 being complex-valued Function holds f1 - f2 = f1 + (- f2);

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)

for c being set st c in dom (f1 - f2) holds

(f1 - f2) . c = (f1 . c) - (f2 . c)

proof 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

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 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 func f1 - f2 -> PartFunc of C,COMPLEX;

coherence

f1 - f2 is PartFunc of C,COMPLEX

end;
let D1, D2 be complex-membered set ;

let f1 be PartFunc of C,D1;

let f2 be PartFunc of C,D2;

:: original: -

redefine func f1 - f2 -> PartFunc of C,COMPLEX;

coherence

f1 - f2 is PartFunc of C,COMPLEX

proof 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 func f1 - f2 -> PartFunc of C,REAL;

coherence

f1 - f2 is PartFunc of C,REAL

end;
let D1, D2 be real-membered set ;

let f1 be PartFunc of C,D1;

let f2 be PartFunc of C,D2;

:: original: -

redefine func f1 - f2 -> PartFunc of C,REAL;

coherence

f1 - f2 is PartFunc of C,REAL

proof 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 func f1 - f2 -> PartFunc of C,RAT;

coherence

f1 - f2 is PartFunc of C,RAT

end;
let D1, D2 be rational-membered set ;

let f1 be PartFunc of C,D1;

let f2 be PartFunc of C,D2;

:: original: -

redefine func f1 - f2 -> PartFunc of C,RAT;

coherence

f1 - f2 is PartFunc of C,RAT

proof 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 func f1 - f2 -> PartFunc of C,INT;

coherence

f1 - f2 is PartFunc of C,INT

end;
let D1, D2 be integer-membered set ;

let f1 be PartFunc of C,D1;

let f2 be PartFunc of C,D2;

:: original: -

redefine func f1 - f2 -> PartFunc of C,INT;

coherence

f1 - f2 is PartFunc of C,INT

proof 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 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;

coherence

for b_{1} being PartFunc of C,COMPLEX st b_{1} = f1 - f2 holds

b_{1} is total

end;
let D1, D2 be non empty complex-membered set ;

let f1 be Function of C,D1;

let f2 be Function of C,D2;

coherence

for b

b

proof 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;

coherence

for b_{1} being PartFunc of C,REAL st b_{1} = f1 - f2 holds

b_{1} is total

end;
let D1, D2 be non empty real-membered set ;

let f1 be Function of C,D1;

let f2 be Function of C,D2;

coherence

for b

b

proof 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;

coherence

for b_{1} being PartFunc of C,RAT st b_{1} = f1 - f2 holds

b_{1} is total

end;
let D1, D2 be non empty rational-membered set ;

let f1 be Function of C,D1;

let f2 be Function of C,D2;

coherence

for b

b

proof 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;

coherence

for b_{1} being PartFunc of C,INT st b_{1} = f1 - f2 holds

b_{1} is total

end;
let D1, D2 be non empty integer-membered set ;

let f1 be Function of C,D1;

let f2 be Function of C,D2;

coherence

for b

b

proof 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)

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 end;

begin

:: deftheorem defines /" VALUED_1:def 10 :

for f1, f2 being complex-valued Function holds f1 /" f2 = f1 (#) (f2 ");

for f1, f2 being complex-valued Function holds f1 /" f2 = f1 (#) (f2 ");

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 func f1 /" f2 -> PartFunc of C,COMPLEX;

coherence

f1 /" f2 is PartFunc of C,COMPLEX

end;
let D1, D2 be complex-membered set ;

let f1 be PartFunc of C,D1;

let f2 be PartFunc of C,D2;

:: original: /"

redefine func f1 /" f2 -> PartFunc of C,COMPLEX;

coherence

f1 /" f2 is PartFunc of C,COMPLEX

proof 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 func f1 /" f2 -> PartFunc of C,REAL;

coherence

f1 /" f2 is PartFunc of C,REAL

end;
let D1, D2 be real-membered set ;

let f1 be PartFunc of C,D1;

let f2 be PartFunc of C,D2;

:: original: /"

redefine func f1 /" f2 -> PartFunc of C,REAL;

coherence

f1 /" f2 is PartFunc of C,REAL

proof 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 func f1 /" f2 -> PartFunc of C,RAT;

coherence

f1 /" f2 is PartFunc of C,RAT

end;
let D1, D2 be rational-membered set ;

let f1 be PartFunc of C,D1;

let f2 be PartFunc of C,D2;

:: original: /"

redefine func f1 /" f2 -> PartFunc of C,RAT;

coherence

f1 /" f2 is PartFunc of C,RAT

proof 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 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;

coherence

for b_{1} being PartFunc of C,COMPLEX st b_{1} = f1 /" f2 holds

b_{1} is total

end;
let D1, D2 be non empty complex-membered set ;

let f1 be Function of C,D1;

let f2 be Function of C,D2;

coherence

for b

b

proof 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;

coherence

for b_{1} being PartFunc of C,REAL st b_{1} = f1 /" f2 holds

b_{1} is total

end;
let D1, D2 be non empty real-membered set ;

let f1 be Function of C,D1;

let f2 be Function of C,D2;

coherence

for b

b

proof 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;

coherence

for b_{1} being PartFunc of C,RAT st b_{1} = f1 /" f2 holds

b_{1} is total

end;
let D1, D2 be non empty rational-membered set ;

let f1 be Function of C,D1;

let f2 be Function of C,D2;

coherence

for b

b

proof end;

registration
end;

begin

definition

let f be complex-valued Function;

deffunc H_{1}( set ) -> Element of REAL = |.(f . $1).|;

ex b_{1} being real-valued Function st

( dom b_{1} = dom f & ( for c being set st c in dom b_{1} holds

b_{1} . c = |.(f . c).| ) )

for b_{1}, b_{2} being real-valued Function st dom b_{1} = dom f & ( for c being set st c in dom b_{1} holds

b_{1} . c = |.(f . c).| ) & dom b_{2} = dom f & ( for c being set st c in dom b_{2} holds

b_{2} . c = |.(f . c).| ) holds

b_{1} = b_{2}

for b_{1} being real-valued Function

for b_{2} being complex-valued Function st dom b_{1} = dom b_{2} & ( for c being set st c in dom b_{1} holds

b_{1} . c = |.(b_{2} . c).| ) holds

( dom b_{1} = dom b_{1} & ( for c being set st c in dom b_{1} holds

b_{1} . c = |.(b_{1} . c).| ) )

end;
deffunc H

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 ( dom it = dom f & ( for c being set st c in dom it holds

it . c = |.(f . c).| ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

projectivity for b

for b

b

( dom b

b

proof end;

:: deftheorem Def11 defines |. VALUED_1:def 11 :

for f being complex-valued Function

for b_{2} being real-valued Function holds

( b_{2} = |.f.| iff ( dom b_{2} = dom f & ( for c being set st c in dom b_{2} holds

b_{2} . c = |.(f . c).| ) ) );

for f being complex-valued Function

for b

( b

b

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

end;
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 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

end;
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 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

end;
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 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

end;
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 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

end;
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 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

end;
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 end;

registration

let C be set ;

let D be non empty complex-membered set ;

let f be Function of C,D;

coherence

for b_{1} being PartFunc of C,REAL st b_{1} = |.f.| holds

b_{1} is total

end;
let D be non empty complex-membered set ;

let f be Function of C,D;

coherence

for b

b

proof end;

registration

let C be set ;

let D be non empty rational-membered set ;

let f be Function of C,D;

coherence

for b_{1} being PartFunc of C,RAT st b_{1} = |.f.| holds

b_{1} is total

end;
let D be non empty rational-membered set ;

let f be Function of C,D;

coherence

for b

b

proof end;

registration

let C be set ;

let D be non empty integer-membered set ;

let f be Function of C,D;

coherence

for b_{1} being PartFunc of C,NAT st b_{1} = |.f.| holds

b_{1} is total

end;
let D be non empty integer-membered set ;

let f be Function of C,D;

coherence

for b

b

proof end;

registration
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;

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;

ex b_{1} being Function st

( dom b_{1} = { (m + k) where m is Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds

b_{1} . (m + k) = p . m ) )

for b_{1}, b_{2} being Function st dom b_{1} = { (m + k) where m is Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds

b_{1} . (m + k) = p . m ) & dom b_{2} = { (m + k) where m is Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds

b_{2} . (m + k) = p . m ) holds

b_{1} = b_{2}

end;
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 ( 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 ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def12 defines Shift VALUED_1:def 12 :

for p being Function

for k being Nat

for b_{3} being Function holds

( b_{3} = Shift (p,k) iff ( dom b_{3} = { (m + k) where m is Element of NAT : m in dom p } & ( for m being Element of NAT st m in dom p holds

b_{3} . (m + k) = p . m ) ) );

for p being Function

for k being Nat

for b

( b

b

:: from SCMPDS_4, 2008.03.16, A.T.

:: missing, 2008.03.16, A.T.

definition

let X be non empty ext-real-membered set ;

let s be sequence of X;

( s is increasing iff for n being Nat holds s . n < s . (n + 1) )

( s is decreasing iff for n being Nat holds s . n > s . (n + 1) )

( s is non-decreasing iff for n being Nat holds s . n <= s . (n + 1) )

( s is non-increasing iff for n being Nat holds s . n >= s . (n + 1) )

end;
let s be sequence of X;

:: original: increasing

redefine attr s is increasing means :: VALUED_1:def 13

for n being Nat holds s . n < s . (n + 1);

compatibility redefine attr s is increasing means :: VALUED_1:def 13

for n being Nat holds s . n < s . (n + 1);

( s is increasing iff for n being Nat holds s . n < s . (n + 1) )

proof end;

:: original: decreasing

redefine attr s is decreasing means :: VALUED_1:def 14

for n being Nat holds s . n > s . (n + 1);

compatibility redefine attr s is decreasing means :: VALUED_1:def 14

for n being Nat holds s . n > s . (n + 1);

( s is decreasing iff for n being Nat holds s . n > s . (n + 1) )

proof end;

:: original: non-decreasing

redefine attr s is non-decreasing means :: VALUED_1:def 15

for n being Nat holds s . n <= s . (n + 1);

compatibility redefine attr s is non-decreasing means :: VALUED_1:def 15

for n being Nat holds s . n <= s . (n + 1);

( s is non-decreasing iff for n being Nat holds s . n <= s . (n + 1) )

proof end;

:: original: non-increasing

redefine attr s is non-increasing means :: VALUED_1:def 16

for n being Nat holds s . n >= s . (n + 1);

compatibility redefine attr s is non-increasing means :: VALUED_1:def 16

for n being Nat holds s . n >= s . (n + 1);

( s is non-increasing iff for n being Nat holds s . n >= s . (n + 1) )

proof 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) );

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) );

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) );

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) );

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) );

:: from KURATO_2, 2008.09.05, A.T.

:: from AMISTD_2, 2010.02.05, A.T.

registration
end;

registration

let X be non empty set ;

let F be X -valued Function;

let k be Nat;

coherence

Shift (F,k) is X -valued

end;
let F be X -valued Function;

let k be Nat;

coherence

Shift (F,k) is X -valued

proof end;

registration
end;

registration

let F be NAT -defined non empty Function;

let k be Nat;

coherence

not Shift (F,k) is empty

end;
let k be Nat;

coherence

not Shift (F,k) is empty

proof end;

registration

existence

ex b_{1} being Function st

( b_{1} is NAT -defined & b_{1} is finite & not b_{1} is empty )

end;
ex b

( b

proof end;

definition

let F be NAT -defined non empty finite Function;

coherence

max (dom F) is Element of NAT by ORDINAL1:def 12;

end;
coherence

max (dom F) is Element of NAT by ORDINAL1:def 12;

:: deftheorem defines LastLoc VALUED_1:def 17 :

for F being NAT -defined non empty finite Function holds LastLoc F = max (dom F);

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;

coherence

F \ ((LastLoc F) .--> (F . (LastLoc F))) is Function ;

end;
coherence

F \ ((LastLoc F) .--> (F . (LastLoc F))) is Function ;

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

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;

coherence

( CutLastLoc F is NAT -defined & CutLastLoc F is finite ) ;

end;
coherence

( CutLastLoc F is NAT -defined & CutLastLoc F is finite ) ;

theorem :: VALUED_1:31

theorem :: VALUED_1:32

definition

let F be NAT -defined non empty Function;

coherence

min (dom F) is Element of NAT by ORDINAL1:def 12;

end;
coherence

min (dom F) is Element of NAT by ORDINAL1:def 12;

:: deftheorem defines FirstLoc VALUED_1:def 19 :

for F being NAT -defined non empty Function holds FirstLoc F = min (dom F);

for F being NAT -defined non empty Function holds FirstLoc F = min (dom F);

theorem :: VALUED_1:33

theorem :: VALUED_1:34

theorem :: VALUED_1:35

theorem Th36: :: VALUED_1:36

for F being NAT -defined non empty finite Function holds dom (CutLastLoc F) = (dom F) \ {(LastLoc F)}

proof end;

theorem :: VALUED_1:37

for F being NAT -defined non empty finite Function holds dom F = (dom (CutLastLoc F)) \/ {(LastLoc F)}

proof end;

registration

existence

ex b_{1} being Function st

( b_{1} is 1 -element & b_{1} is NAT -defined & b_{1} is finite )

end;
ex b

( b

proof end;

registration
end;

begin

registration

let X be set ;

let f be X -defined complex-valued Function;

coherence

- f is X -defined

f " is X -defined

f ^2 is X -defined

|.f.| is X -defined

end;
let f be X -defined complex-valued Function;

coherence

- f is X -defined

proof end;

coherence f " is X -defined

proof end;

coherence f ^2 is X -defined

proof end;

coherence |.f.| is X -defined

proof end;

registration

let X be set ;

ex b_{1} being X -defined natural-valued Function st b_{1} is total

end;
cluster Relation-like X -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued for set ;

existence ex b

proof end;

registration

let X be set ;

let f be X -defined total complex-valued Function;

coherence

- f is total

f " is total

f ^2 is total

|.f.| is total

end;
let f be X -defined total complex-valued Function;

coherence

- f is total

proof end;

coherence f " is total

proof end;

coherence f ^2 is total

proof end;

coherence |.f.| is total

proof end;

registration

let X be set ;

let f be X -defined complex-valued Function;

let r be complex number ;

coherence

r + f is X -defined

f - r is X -defined ;

coherence

r (#) f is X -defined

end;
let f be X -defined complex-valued Function;

let r be complex number ;

coherence

r + f is X -defined

proof end;

coherence f - r is X -defined ;

coherence

r (#) f is X -defined

proof end;

registration

let X be set ;

let f be X -defined total complex-valued Function;

let r be complex number ;

coherence

r + f is total

f - r is total ;

coherence

r (#) f is total

end;
let f be X -defined total complex-valued Function;

let r be complex number ;

coherence

r + f is total

proof end;

coherence f - r is total ;

coherence

r (#) f is total

proof end;

registration

let X be set ;

let f1 be complex-valued Function;

let f2 be X -defined complex-valued Function;

coherence

f1 + f2 is X -defined

f1 - f2 is X -defined ;

coherence

f1 (#) f2 is X -defined

f1 /" f2 is X -defined ;

end;
let f1 be complex-valued Function;

let f2 be X -defined complex-valued Function;

coherence

f1 + f2 is X -defined

proof end;

coherence f1 - f2 is X -defined ;

coherence

f1 (#) f2 is X -defined

proof end;

coherence f1 /" f2 is X -defined ;

registration

let X be set ;

let f1, f2 be X -defined total complex-valued Function;

coherence

f1 + f2 is total

f1 - f2 is total ;

coherence

f1 (#) f2 is total

f1 /" f2 is total ;

end;
let f1, f2 be X -defined total complex-valued Function;

coherence

f1 + f2 is total

proof end;

coherence f1 - f2 is total ;

coherence

f1 (#) f2 is total

proof end;

coherence f1 /" f2 is total ;

registration

let X be non empty set ;

let F be NAT -defined X -valued non empty finite Function;

coherence

CutLastLoc F is X -valued ;

end;
let F be NAT -defined X -valued non empty finite Function;

coherence

CutLastLoc F is X -valued ;

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 )

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 end;