:: by Jaros{\l}aw Kotowicz

::

:: Received July 4, 1989

:: Copyright (c) 1990-2016 Association of Mizar Users

theorem Th1: :: SEQ_1:1

for f being Function holds

( f is Real_Sequence iff ( dom f = NAT & ( for x being object st x in NAT holds

f . x is real ) ) )

( f is Real_Sequence iff ( dom f = NAT & ( for x being object st x in NAT holds

f . x is real ) ) )

proof end;

theorem Th2: :: SEQ_1:2

for f being Function holds

( f is Real_Sequence iff ( dom f = NAT & ( for n being Nat holds f . n is real ) ) )

( f is Real_Sequence iff ( dom f = NAT & ( for n being Nat holds f . n is real ) ) )

proof end;

registration

ex b_{1} being PartFunc of NAT,REAL st b_{1} is non-zero
end;

cluster Relation-like NAT -defined REAL -valued Function-like non-zero complex-valued ext-real-valued real-valued for Element of K19(K20(NAT,REAL));

existence ex b

proof end;

theorem :: SEQ_1:3

theorem Th4: :: SEQ_1:4

for seq being Real_Sequence holds

( seq is non-zero iff for x being object st x in NAT holds

seq . x <> 0 )

( seq is non-zero iff for x being object st x in NAT holds

seq . x <> 0 )

proof end;

scheme :: SEQ_1:sch 2

PartFuncExD9{ F_{1}() -> non empty set , F_{2}() -> non empty set , P_{1}[ object , object ] } :

PartFuncExD9{ F

ex f being PartFunc of F_{1}(),F_{2}() st

( ( for d being Element of F_{1}() holds

( d in dom f iff ex c being Element of F_{2}() st P_{1}[d,c] ) ) & ( for d being Element of F_{1}() st d in dom f holds

P_{1}[d,f . d] ) )

( ( for d being Element of F

( d in dom f iff ex c being Element of F

P

proof end;

scheme :: SEQ_1:sch 3

LambdaPFD9{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}( object ) -> Element of F_{2}(), P_{1}[ object ] } :

LambdaPFD9{ F

ex f being PartFunc of F_{1}(),F_{2}() st

( ( for d being Element of F_{1}() holds

( d in dom f iff P_{1}[d] ) ) & ( for d being Element of F_{1}() st d in dom f holds

f . d = F_{3}(d) ) )

( ( for d being Element of F

( d in dom f iff P

f . d = F

proof end;

scheme :: SEQ_1:sch 4

UnPartFuncD9{ F_{1}() -> set , F_{2}() -> set , F_{3}() -> set , F_{4}( object ) -> object } :

UnPartFuncD9{ F

for f, g being PartFunc of F_{1}(),F_{2}() st dom f = F_{3}() & ( for c being Element of F_{1}() st c in dom f holds

f . c = F_{4}(c) ) & dom g = F_{3}() & ( for c being Element of F_{1}() st c in dom g holds

g . c = F_{4}(c) ) holds

f = g

f . c = F

g . c = F

f = g

proof end;

theorem Th7: :: SEQ_1:7

for seq, seq1, seq2 being Real_Sequence holds

( seq = seq1 + seq2 iff for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) )

( seq = seq1 + seq2 iff for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) )

proof end;

theorem Th8: :: SEQ_1:8

for seq, seq1, seq2 being Real_Sequence holds

( seq = seq1 (#) seq2 iff for n being Nat holds seq . n = (seq1 . n) * (seq2 . n) )

( seq = seq1 (#) seq2 iff for n being Nat holds seq . n = (seq1 . n) * (seq2 . n) )

proof end;

theorem Th9: :: SEQ_1:9

for r being Real

for seq1, seq2 being Real_Sequence holds

( seq1 = r (#) seq2 iff for n being Nat holds seq1 . n = r * (seq2 . n) )

for seq1, seq2 being Real_Sequence holds

( seq1 = r (#) seq2 iff for n being Nat holds seq1 . n = r * (seq2 . n) )

proof end;

theorem :: SEQ_1:10

for seq1, seq2 being Real_Sequence holds

( seq1 = - seq2 iff for n being Nat holds seq1 . n = - (seq2 . n) )

( seq1 = - seq2 iff for n being Nat holds seq1 . n = - (seq2 . n) )

proof end;

theorem Th12: :: SEQ_1:12

for seq, seq1 being Real_Sequence holds

( seq1 = abs seq iff for n being Nat holds seq1 . n = |.(seq . n).| )

( seq1 = abs seq iff for n being Nat holds seq1 . n = |.(seq . n).| )

proof end;

theorem Th15: :: SEQ_1:15

for seq1, seq2, seq3 being Real_Sequence holds (seq1 + seq2) (#) seq3 = (seq1 (#) seq3) + (seq2 (#) seq3)

proof end;

theorem :: SEQ_1:16

theorem Th18: :: SEQ_1:18

for r being Real

for seq1, seq2 being Real_Sequence holds r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2

for seq1, seq2 being Real_Sequence holds r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2

proof end;

theorem Th19: :: SEQ_1:19

for r being Real

for seq1, seq2 being Real_Sequence holds r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2)

for seq1, seq2 being Real_Sequence holds r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2)

proof end;

theorem Th20: :: SEQ_1:20

for seq1, seq2, seq3 being Real_Sequence holds (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) - (seq2 (#) seq3)

proof end;

theorem :: SEQ_1:21

theorem Th22: :: SEQ_1:22

for r being Real

for seq1, seq2 being Real_Sequence holds r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2)

for seq1, seq2 being Real_Sequence holds r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2)

proof end;

theorem Th24: :: SEQ_1:24

for r being Real

for seq1, seq2 being Real_Sequence holds r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2)

for seq1, seq2 being Real_Sequence holds r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2)

proof end;

::$CT

theorem :: SEQ_1:32

::$CT

theorem Th33: :: SEQ_1:35

for seq, seq1 being Real_Sequence holds

( ( seq is non-zero & seq1 is non-zero ) iff seq (#) seq1 is non-zero )

( ( seq is non-zero & seq1 is non-zero ) iff seq (#) seq1 is non-zero )

proof end;

theorem :: SEQ_1:38

for seq, seq1, seq9, seq19 being Real_Sequence holds (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1)

proof end;

theorem :: SEQ_1:39

for seq, seq1 being Real_Sequence st seq is non-zero & seq1 is non-zero holds

seq /" seq1 is non-zero

seq /" seq1 is non-zero

proof end;

theorem Th41: :: SEQ_1:43

for seq, seq1, seq2 being Real_Sequence st seq1 is non-zero holds

seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1)

seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1)

proof end;

theorem Th42: :: SEQ_1:44

for r being Real

for seq being Real_Sequence st r <> 0 & seq is non-zero holds

r (#) seq is non-zero

for seq being Real_Sequence st r <> 0 & seq is non-zero holds

r (#) seq is non-zero

proof end;

Lm1: (- 1) " = - 1

;

theorem :: SEQ_1:48

for seq, seq1 being Real_Sequence holds

( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) )

( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) )

proof end;

theorem :: SEQ_1:49

for seq, seq1, seq19 being Real_Sequence holds

( (seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) /" seq & (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq )

( (seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) /" seq & (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq )

proof end;

theorem :: SEQ_1:50

for seq, seq1, seq9, seq19 being Real_Sequence st seq is non-zero & seq9 is non-zero holds

( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) & (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) )

( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) & (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) )

proof end;

theorem :: SEQ_1:51

for seq, seq1, seq9, seq19 being Real_Sequence holds (seq19 /" seq) /" (seq9 /" seq1) = (seq19 (#) seq1) /" (seq (#) seq9)

proof end;

registration
end;

registration

ex b_{1} being Real_Sequence st b_{1} is constant
end;

cluster Relation-like NAT -defined REAL -valued Function-like constant non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued for Element of K19(K20(NAT,REAL));

existence ex b

proof end;

theorem :: SEQ_1:57