:: by Library Committee

::

:: Received December 18, 2007

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

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;

registration

ex b_{1} being FinSequence st b_{1} is complex-valued
end;

cluster Relation-like omega -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like for FinSequence;

existence ex b

proof end;

:: move somewhere

registration
end;

definition

let f1, f2 be complex-valued Function;

deffunc H_{1}( object ) -> 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 object 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 object st c in dom b_{1} holds

b_{1} . c = (f1 . c) + (f2 . c) ) & dom b_{2} = (dom f1) /\ (dom f2) & ( for c being object 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 object 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 object 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 object st c in dom it holds

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

existence ( dom it = (dom f1) /\ (dom f2) & ( for c being object 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 object 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;

definition

let f be complex-valued Function;

let r be Complex;

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

ex b_{1} being Function st

( dom b_{1} = dom f & ( for c being object 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 object st c in dom b_{1} holds

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

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

b_{1} = b_{2}

end;
let r be Complex;

deffunc H

func r + f -> Function means :Def2: :: VALUED_1:def 2

( dom it = dom f & ( for c being object st c in dom it holds

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

existence ( dom it = dom f & ( for c being object 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

for b_{3} being Function holds

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

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

for f being complex-valued Function

for r being Complex

for b

( b

b

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

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

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

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

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

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

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

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

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

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;

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;

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;

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;

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;

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;

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;

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

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

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;

coherence

r + f is FinSequence-like

end;
let r be Complex;

coherence

r + f is FinSequence-like

proof end;

definition
end;

:: deftheorem defines - VALUED_1:def 3 :

for f being complex-valued Function

for r being Complex holds f - r = (- r) + f;

for f being complex-valued Function

for r being Complex holds f - r = (- r) + f;

theorem :: VALUED_1:3

for f being complex-valued Function

for r being Complex holds

( dom (f - r) = dom f & ( for c being object st c in dom f holds

(f - r) . c = (f . c) - r ) )

for r being Complex holds

( dom (f - r) = dom f & ( for c being object st c in dom f holds

(f - r) . c = (f . c) - r ) )

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

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

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

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

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

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

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

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

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

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;

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;

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;

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;

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;

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;

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;

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

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

for c being Element of C holds (f - r) . c = (f . c) - r

proof end;

registration
end;

definition

let f1, f2 be complex-valued Function;

deffunc H_{1}( object ) -> 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 object 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 object st c in dom b_{1} holds

b_{1} . c = (f1 . c) * (f2 . c) ) & dom b_{2} = (dom f1) /\ (dom f2) & ( for c being object 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 object 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 object 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 object st c in dom it holds

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

existence ( dom it = (dom f1) /\ (dom f2) & ( for c being object 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 object 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 object holds (f1 (#) f2) . c = (f1 . c) * (f2 . c)

for c being object 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;

definition

let f be complex-valued Function;

let r be Complex;

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

ex b_{1} being Function st

( dom b_{1} = dom f & ( for c being object 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 object st c in dom b_{1} holds

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

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

b_{1} = b_{2}

end;
let r be Complex;

deffunc H

func r (#) f -> Function means :Def5: :: VALUED_1:def 5

( dom it = dom f & ( for c being object st c in dom it holds

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

existence ( dom it = dom f & ( for c being object 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

for b_{3} being Function holds

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

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

for f being complex-valued Function

for r being Complex

for b

( b

b

theorem Th6: :: VALUED_1:6

for f being complex-valued Function

for r being Complex

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

for r being Complex

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

proof end;

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

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

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

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

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

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

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

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

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

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;

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;

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;

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;

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;

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;

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;

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

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

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;

coherence

r (#) f is FinSequence-like

end;
let r be Complex;

coherence

r (#) f is FinSequence-like

proof end;

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 object holds (- f) . c = - (f . c) ) )

( dom (- f) = dom f & ( for c being object 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 object 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 object 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

definition

let f be complex-valued Function;

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

ex b_{1} being complex-valued Function st

( dom b_{1} = dom f & ( for c being object 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 object st c in dom b_{1} holds

b_{1} . c = (f . c) " ) & dom b_{2} = dom f & ( for c being object 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 object st c in dom b_{1} holds

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

( dom b_{2} = dom b_{1} & ( for c being object 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 object st c in dom it holds

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

existence ( dom it = dom f & ( for c being object 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 object 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;

theorem Th11: :: VALUED_1:11

for f being complex-valued Function holds

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

( dom (f ^2) = dom f & ( for c being object 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

:: 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 object st c in dom (f1 - f2) holds

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

for c being object 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 object 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 object 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
by Lm3, PARTFUN1:def 2;

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

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
by Lm3, PARTFUN1:def 2;

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

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
by Lm3, PARTFUN1:def 2;

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

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
by Lm3, PARTFUN1:def 2;

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

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;

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

theorem :: VALUED_1:17

for f1, f2 being complex-valued Function

for c being object holds (f1 /" f2) . c = (f1 . c) / (f2 . c)

for c being object holds (f1 /" f2) . c = (f1 . c) / (f2 . c)

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;

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
by Lm4, PARTFUN1:def 2;

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

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
by Lm4, PARTFUN1:def 2;

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

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
by Lm4, PARTFUN1:def 2;

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

registration
end;

definition

let f be complex-valued Function;

deffunc H_{1}( object ) -> object = |.(f . $1).|;

ex b_{1} being real-valued Function st

( dom b_{1} = dom f & ( for c being object 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 object st c in dom b_{1} holds

b_{1} . c = |.(f . c).| ) & dom b_{2} = dom f & ( for c being object 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 object st c in dom b_{1} holds

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

( dom b_{1} = dom b_{1} & ( for c being object 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 object st c in dom it holds

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

existence ( dom it = dom f & ( for c being object 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 object 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;

definition

let p be Function;

let k be Nat;

ex b_{1} being Function st

( dom b_{1} = { (m + k) where m is Nat : m in dom p } & ( for m being 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 Nat : m in dom p } & ( for m being Nat st m in dom p holds

b_{1} . (m + k) = p . m ) & dom b_{2} = { (m + k) where m is Nat : m in dom p } & ( for m being 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 Nat : m in dom p } & ( for m being Nat st m in dom p holds

it . (m + k) = p . m ) );

existence ( dom it = { (m + k) where m is Nat : m in dom p } & ( for m being Nat st m in dom p holds

it . (m + k) = p . m ) );

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 Nat : m in dom p } & ( for m being 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;

::$CT

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:30

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

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

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;

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;

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;

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;

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;

:: from PNPROC_1, 2012.02.20, A.T.

registration
end;

theorem Th39: :: VALUED_1:40

for i being Nat

for p being FinSequence holds dom (Shift (p,i)) = { j1 where j1 is Nat : ( i + 1 <= j1 & j1 <= i + (len p) ) }

for p being FinSequence holds dom (Shift (p,i)) = { j1 where j1 is Nat : ( i + 1 <= j1 & j1 <= i + (len p) ) }

proof end;

theorem Th40: :: VALUED_1:41

for i being Nat

for q being FinSubsequence ex ss being FinSubsequence st

( dom ss = dom q & rng ss = dom (Shift (q,i)) & ( for k being Element of NAT st k in dom q holds

ss . k = i + k ) & ss is one-to-one )

for q being FinSubsequence ex ss being FinSubsequence st

( dom ss = dom q & rng ss = dom (Shift (q,i)) & ( for k being Element of NAT st k in dom q holds

ss . k = i + k ) & ss is one-to-one )

proof end;

Lm5: for i being Nat

for p being FinSequence ex fs being FinSequence st

( dom fs = dom p & rng fs = dom (Shift (p,i)) & ( for k being Element of NAT st k in dom p holds

fs . k = i + k ) & fs is one-to-one )

proof end;

theorem Th43: :: VALUED_1:44

for i being Nat

for k being Element of NAT

for p being FinSequence st k in dom p holds

(Sgm (dom (Shift (p,i)))) . k = i + k

for k being Element of NAT

for p being FinSequence st k in dom p holds

(Sgm (dom (Shift (p,i)))) . k = i + k

proof end;

theorem Th44: :: VALUED_1:45

for i being Nat

for k being Element of NAT

for p being FinSequence st k in dom p holds

(Seq (Shift (p,i))) . k = p . k

for k being Element of NAT

for p being FinSequence st k in dom p holds

(Seq (Shift (p,i))) . k = p . k

proof end;

Lm6: for j, k, l being Nat st ( ( 1 <= j & j <= l ) or ( l + 1 <= j & j <= l + k ) ) holds

( 1 <= j & j <= l + k )

proof end;

theorem Th47: :: VALUED_1:48

for i being Nat

for p1 being FinSequence

for p2 being FinSubsequence st len p1 <= i holds

dom p1 misses dom (Shift (p2,i))

for p1 being FinSequence

for p2 being FinSubsequence st len p1 <= i holds

dom p1 misses dom (Shift (p2,i))

proof end;

theorem :: VALUED_1:50

for i being Nat

for p1 being FinSequence

for p2 being FinSubsequence st i >= len p1 holds

p1 misses Shift (p2,i)

for p1 being FinSequence

for p2 being FinSubsequence st i >= len p1 holds

p1 misses Shift (p2,i)

proof end;

theorem :: VALUED_1:51

for F being NAT -defined total Function

for p being NAT -defined Function

for n being Element of NAT st Shift (p,n) c= F holds

for i being Element of NAT st i in dom p holds

F . (n + i) = p . i

for p being NAT -defined Function

for n being Element of NAT st Shift (p,n) c= F holds

for i being Element of NAT st i in dom p holds

F . (n + i) = p . i

proof end;

theorem Th53: :: VALUED_1:54

for i being Nat

for q1, q2 being FinSubsequence st dom q1 misses dom q2 holds

dom (Shift (q1,i)) misses dom (Shift (q2,i))

for q1, q2 being FinSubsequence st dom q1 misses dom q2 holds

dom (Shift (q1,i)) misses dom (Shift (q2,i))

proof end;

theorem :: VALUED_1:55

for i being Nat

for q, q1, q2 being FinSubsequence st q = q1 \/ q2 & q1 misses q2 holds

(Shift (q1,i)) \/ (Shift (q2,i)) = Shift (q,i)

for q, q1, q2 being FinSubsequence st q = q1 \/ q2 & q1 misses q2 holds

(Shift (q1,i)) \/ (Shift (q2,i)) = Shift (q,i)

proof end;

theorem Th56: :: VALUED_1:57

for i being Nat

for k being Element of NAT

for q being FinSubsequence st k in dom (Seq q) holds

ex j being Element of NAT st

( j = (Sgm (dom q)) . k & (Sgm (dom (Shift (q,i)))) . k = i + j )

for k being Element of NAT

for q being FinSubsequence st k in dom (Seq q) holds

ex j being Element of NAT st

( j = (Sgm (dom q)) . k & (Sgm (dom (Shift (q,i)))) . k = i + j )

proof end;

theorem Th57: :: VALUED_1:58

for i being Nat

for k being Element of NAT

for q being FinSubsequence st k in dom (Seq q) holds

(Seq (Shift (q,i))) . k = (Seq q) . k

for k being Element of NAT

for q being FinSubsequence st k in dom (Seq q) holds

(Seq (Shift (q,i))) . k = (Seq q) . k

proof end;

theorem Th59: :: VALUED_1:60

for i being Nat

for k being Element of NAT

for q being FinSubsequence st dom q c= Seg k holds

dom (Shift (q,i)) c= Seg (i + k)

for k being Element of NAT

for q being FinSubsequence st dom q c= Seg k holds

dom (Shift (q,i)) c= Seg (i + k)

proof end;

theorem Th60: :: VALUED_1:61

for p being FinSequence

for q1, q2 being FinSubsequence st q1 c= p holds

ex ss being FinSubsequence st ss = q1 \/ (Shift (q2,(len p)))

for q1, q2 being FinSubsequence st q1 c= p holds

ex ss being FinSubsequence st ss = q1 \/ (Shift (q2,(len p)))

proof end;

Lm7: for i being Nat

for p, q being FinSubsequence st q c= p holds

dom (Shift (q,i)) c= dom (Shift (p,i))

proof end;

Lm8: for p1, p2 being FinSequence

for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds

Sgm ((dom q1) \/ (dom (Shift (q2,(len p1))))) = (Sgm (dom q1)) ^ (Sgm (dom (Shift (q2,(len p1)))))

proof end;

theorem Th61: :: VALUED_1:62

for p1, p2 being FinSequence

for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds

ex ss being FinSubsequence st

( ss = q1 \/ (Shift (q2,(len p1))) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) )

for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds

ex ss being FinSubsequence st

( ss = q1 \/ (Shift (q2,(len p1))) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) )

proof end;

theorem Th62: :: VALUED_1:63

for p1, p2 being FinSequence

for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds

ex ss being FinSubsequence st

( ss = q1 \/ (Shift (q2,(len p1))) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) & Seq ss = (Seq q1) \/ (Shift ((Seq q2),(len (Seq q1)))) )

for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds

ex ss being FinSubsequence st

( ss = q1 \/ (Shift (q2,(len p1))) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) & Seq ss = (Seq q1) \/ (Shift ((Seq q2),(len (Seq q1)))) )

proof end;

theorem :: VALUED_1:64

for p1, p2 being FinSequence

for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds

ex ss being FinSubsequence st

( ss = q1 \/ (Shift (q2,(len p1))) & (Seq q1) ^ (Seq q2) = Seq ss )

for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds

ex ss being FinSubsequence st

( ss = q1 \/ (Shift (q2,(len p1))) & (Seq q1) ^ (Seq q2) = Seq ss )

proof end;

theorem :: VALUED_1:66

theorem :: VALUED_1:67

for i being Nat

for x, y being set

for f being NAT -defined non empty finite Function holds Shift ((f +~ (x,y)),i) = (Shift (f,i)) +~ (x,y)

for x, y being set

for f being NAT -defined non empty finite Function holds Shift ((f +~ (x,y)),i) = (Shift (f,i)) +~ (x,y)

proof end;

theorem :: VALUED_1:68