begin
Lm1:
for f being FinSequence
for h being Function st dom h = dom f holds
h is FinSequence
Lm2:
for f, g being FinSequence
for h being Function st dom h = (dom f) /\ (dom g) holds
h is FinSequence
:: deftheorem Def1 defines + VALUED_1:def 1 :
theorem
begin
:: deftheorem Def2 defines + VALUED_1:def 2 :
theorem
begin
:: deftheorem defines - VALUED_1:def 3 :
theorem
theorem
begin
:: deftheorem Def4 defines (#) VALUED_1:def 4 :
theorem
begin
:: deftheorem Def5 defines (#) VALUED_1:def 5 :
theorem Th6:
theorem
begin
:: deftheorem defines - VALUED_1:def 6 :
theorem Th8:
theorem
begin
:: deftheorem Def7 defines " VALUED_1:def 7 :
theorem Th10:
begin
:: deftheorem defines ^2 VALUED_1:def 8 :
theorem Th11:
begin
:: deftheorem defines - VALUED_1:def 9 :
theorem Th12:
theorem
theorem
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
theorem
begin
:: deftheorem defines /" VALUED_1:def 10 :
theorem Th16:
theorem
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
begin
:: deftheorem Def11 defines |. VALUED_1:def 11 :
theorem
theorem
begin
:: deftheorem Def12 defines Shift VALUED_1:def 12 :
theorem
canceled;
theorem
theorem
theorem
theorem
theorem Th25:
theorem Th26:
theorem
:: deftheorem defines increasing VALUED_1:def 13 :
:: deftheorem defines decreasing VALUED_1:def 14 :
:: deftheorem defines non-decreasing VALUED_1:def 15 :
:: deftheorem defines non-increasing VALUED_1:def 16 :