:: Basic Properties and Concept of Selected Subsequence of Zero Based Finite Sequences
:: by Yatsuka Nakamura and Hisashi Ito
::
:: Received June 27, 2008
:: Copyright (c) 2008-2011 Association of Mizar Users

begin

Lm1: for X, Y being finite set st X c= Y & card X = card Y holds
X = Y

proof end;

Lm2: for X, Y being finite set
for F being Function of X,Y st card X = card Y holds
( F is onto iff F is one-to-one )

proof end;

theorem Th1: :: AFINSQ_2:1

for i being Nat
for x being set st x in i holds
x is Element of NAT

proof end;

registration

cluster natural -> natural-membered set ;
coherence
for b₁ being Nat holds b₁ is natural-membered

proof end;

end;

begin

theorem Th2: :: AFINSQ_2:2

for X0 being finite natural-membered set ex n being Nat st X0 c= n

proof end;

theorem Th3: :: AFINSQ_2:3

for x being set
for p being XFinSequence st x in rng p holds
ex i being Element of NAT st
( i in dom p & p . i = x )

proof end;

theorem Th4: :: AFINSQ_2:4

for D being set
for p being XFinSequence st ( for i being Nat st i in dom p holds
p . i in D ) holds
p is XFinSequence of D

proof end;

scheme :: AFINSQ_2:sch 1
XSeqLambdaD{ F₁() -> Nat, F₂() -> non empty set , F₃( set ) -> Element of F₂() } :

ex p being XFinSequence of F₂() st
( len p = F₁() & ( for j being Nat st j in F₁() holds
p . j = F₃(j) ) )

proof end;

theorem :: AFINSQ_2:5

canceled;

registration

cluster Relation-like NAT -defined Function-like empty T-Sequence-like natural-valued finite V176() set ;
existence
ex b₁ being XFinSequence st
( b₁ is empty & b₁ is natural-valued )

proof end;

let p be T-Sequence-like complex-valued Function;
cluster - p -> T-Sequence-like ;
coherence
- p is T-Sequence-like

proof end;

cluster p " -> T-Sequence-like ;
coherence
p " is T-Sequence-like

proof end;

cluster p ^2 -> T-Sequence-like ;
coherence
p ^2 is T-Sequence-like

proof end;

cluster |.p.| -> T-Sequence-like ;
coherence
abs p is T-Sequence-like

proof end;

let q be T-Sequence-like complex-valued Function;
cluster p + q -> T-Sequence-like ;
coherence
p + q is T-Sequence-like

proof end;

cluster p - q -> T-Sequence-like ;
coherence
p - q is T-Sequence-like

proof end;

cluster p (#) q -> T-Sequence-like ;
coherence
p (#) q is T-Sequence-like

proof end;

cluster p /" q -> T-Sequence-like ;
coherence
p /" q is T-Sequence-like

proof end;

end;

registration

let p be complex-valued finite Function;
cluster - p -> finite ;
coherence
- p is finite

proof end;

cluster p " -> finite ;
coherence
p " is finite

proof end;

cluster p ^2 -> finite ;
coherence
p ^2 is finite

proof end;

cluster |.p.| -> finite ;
coherence
abs p is finite

proof end;

let q be complex-valued Function;
cluster p + q -> finite ;
coherence
p + q is finite

proof end;

cluster p - q -> finite ;
coherence
p - q is finite

proof end;

cluster p (#) q -> finite ;
coherence
p (#) q is finite

proof end;

cluster p /" q -> finite ;
coherence
p /" q is finite

proof end;

cluster q /" p -> finite ;
coherence
q /" p is finite

proof end;

end;

registration

let p be T-Sequence-like complex-valued Function;
let c be complex number ;
cluster c + p -> T-Sequence-like ;
coherence
c + p is T-Sequence-like

proof end;

cluster p - c -> T-Sequence-like ;
coherence
p - c is T-Sequence-like

proof end;

cluster c (#) p -> T-Sequence-like ;
coherence
c (#) p is T-Sequence-like

proof end;

end;

registration

let p be complex-valued finite Function;
let c be complex number ;
cluster c + p -> finite ;
coherence
c + p is finite

proof end;

cluster p - c -> finite ;
coherence
p - c is finite

proof end;

cluster c (#) p -> finite ;
coherence
c (#) p is finite

proof end;

end;

theorem :: AFINSQ_2:6

canceled;

theorem :: AFINSQ_2:7

canceled;

definition

let p be XFinSequence;
func Rev p -> XFinSequence means :Def1: :: AFINSQ_2:def 1
( len it = len p & ( for i being Nat st i in dom it holds
it . i = p . ((len p) - (i + 1)) ) );
existence
ex b₁ being XFinSequence st
( len b₁ = len p & ( for i being Nat st i in dom b₁ holds
b₁ . i = p . ((len p) - (i + 1)) ) )

proof end;

uniqueness
for b₁, b₂ being XFinSequence st len b₁ = len p & ( for i being Nat st i in dom b₁ holds
b₁ . i = p . ((len p) - (i + 1)) ) & len b₂ = len p & ( for i being Nat st i in dom b₂ holds
b₂ . i = p . ((len p) - (i + 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Rev AFINSQ_2:def 1 :
for p, b₂ being XFinSequence holds
( b₂ = Rev p iff ( len b₂ = len p & ( for i being Nat st i in dom b₂ holds
b₂ . i = p . ((len p) - (i + 1)) ) ) );

theorem Th8: :: AFINSQ_2:8

for p being XFinSequence holds
( dom p = dom (Rev p) & rng p = rng (Rev p) )

proof end;

registration

let D be set ;
let f be XFinSequence of D;
cluster Rev f -> D -valued ;
coherence
Rev f is D -valued

proof end;

end;

theorem :: AFINSQ_2:9

canceled;

theorem :: AFINSQ_2:10

canceled;

theorem :: AFINSQ_2:11

canceled;

theorem :: AFINSQ_2:12

canceled;

theorem :: AFINSQ_2:13

canceled;

theorem :: AFINSQ_2:14

canceled;

definition

let p be XFinSequence;
let n be Nat;
func p /^ n -> XFinSequence means :Def2: :: AFINSQ_2:def 2
( len it = (len p) -' n & ( for m being Nat st m in dom it holds
it . m = p . (m + n) ) );
existence
ex b₁ being XFinSequence st
( len b₁ = (len p) -' n & ( for m being Nat st m in dom b₁ holds
b₁ . m = p . (m + n) ) )

proof end;

uniqueness
for b₁, b₂ being XFinSequence st len b₁ = (len p) -' n & ( for m being Nat st m in dom b₁ holds
b₁ . m = p . (m + n) ) & len b₂ = (len p) -' n & ( for m being Nat st m in dom b₂ holds
b₂ . m = p . (m + n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines /^ AFINSQ_2:def 2 :
for p being XFinSequence
for n being Nat
for b₃ being XFinSequence holds
( b₃ = p /^ n iff ( len b₃ = (len p) -' n & ( for m being Nat st m in dom b₃ holds
b₃ . m = p . (m + n) ) ) );

theorem Th15: :: AFINSQ_2:15

for n being Nat
for p being XFinSequence st n >= len p holds
p /^ n = {}

proof end;

theorem Th16: :: AFINSQ_2:16

for n being Nat
for p being XFinSequence st n < len p holds
len (p /^ n) = (len p) - n

proof end;

theorem Th17: :: AFINSQ_2:17

for m, n being Nat
for p being XFinSequence st m + n < len p holds
(p /^ n) . m = p . (m + n)

proof end;

registration

let f be one-to-one XFinSequence;
let n be Nat;
cluster f /^ n -> one-to-one ;
coherence
f /^ n is one-to-one

proof end;

end;

theorem Th18: :: AFINSQ_2:18

for n being Nat
for p being XFinSequence holds rng (p /^ n) c= rng p

proof end;

theorem Th19: :: AFINSQ_2:19

for p being XFinSequence holds p /^ 0 = p

proof end;

theorem Th20: :: AFINSQ_2:20

for i being Nat
for p, q being XFinSequence holds (p ^ q) /^ ((len p) + i) = q /^ i

proof end;

theorem Th21: :: AFINSQ_2:21

for p, q being XFinSequence holds (p ^ q) /^ (len p) = q

proof end;

theorem :: AFINSQ_2:22

for n being Nat
for p being XFinSequence holds (p | n) ^ (p /^ n) = p

proof end;

registration

let D be set ;
let f be XFinSequence of D;
let n be Nat;
cluster f /^ n -> D -valued ;
coherence
f /^ n is D -valued

proof end;

end;

definition

let p be XFinSequence;
let k1, k2 be Nat;
func mid (p,k1,k2) -> XFinSequence equals :: AFINSQ_2:def 3
(p | k2) /^ (k1 -' 1);
coherence
(p | k2) /^ (k1 -' 1) is XFinSequence ;

end;

:: deftheorem defines mid AFINSQ_2:def 3 :
for p being XFinSequence
for k1, k2 being Nat holds mid (p,k1,k2) = (p | k2) /^ (k1 -' 1);

theorem Th23: :: AFINSQ_2:23

for p being XFinSequence
for k1, k2 being Nat st k1 > k2 holds
mid (p,k1,k2) = {}

proof end;

theorem :: AFINSQ_2:24

for p being XFinSequence
for k1, k2 being Nat st 1 <= k1 & k2 <= len p holds
mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1)

proof end;

theorem Th25: :: AFINSQ_2:25

for k being Nat
for p being XFinSequence holds mid (p,1,k) = p | k

proof end;

theorem :: AFINSQ_2:26

for k being Nat
for p being XFinSequence st len p <= k holds
mid (p,1,k) = p

proof end;

theorem :: AFINSQ_2:27

for k being Nat
for p being XFinSequence holds mid (p,0,k) = mid (p,1,k)

proof end;

theorem :: AFINSQ_2:28

for p, q being XFinSequence holds mid ((p ^ q),((len p) + 1),((len p) + (len q))) = q

proof end;

registration

let D be set ;
let f be XFinSequence of D;
let k1, k2 be Nat;
cluster mid (f,k1,k2) -> D -valued ;
coherence
mid (f,k1,k2) is D -valued ;

end;

definition

canceled;

end;

:: deftheorem AFINSQ_2:def 4 :
canceled;

theorem :: AFINSQ_2:29

canceled;

theorem :: AFINSQ_2:30

canceled;

begin

definition

let X be finite natural-membered set ;
func Sgm0 X -> XFinSequence of NAT means :Def5: :: AFINSQ_2:def 5
( rng it = X & ( for l, m, k1, k2 being Nat st l < m & m < len it & k1 = it . l & k2 = it . m holds
k1 < k2 ) );
existence
ex b₁ being XFinSequence of NAT st
( rng b₁ = X & ( for l, m, k1, k2 being Nat st l < m & m < len b₁ & k1 = b₁ . l & k2 = b₁ . m holds
k1 < k2 ) )

proof end;

uniqueness
for b₁, b₂ being XFinSequence of NAT st rng b₁ = X & ( for l, m, k1, k2 being Nat st l < m & m < len b₁ & k1 = b₁ . l & k2 = b₁ . m holds
k1 < k2 ) & rng b₂ = X & ( for l, m, k1, k2 being Nat st l < m & m < len b₂ & k1 = b₂ . l & k2 = b₂ . m holds
k1 < k2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines Sgm0 AFINSQ_2:def 5 :
for X being finite natural-membered set
for b₂ being XFinSequence of NAT holds
( b₂ = Sgm0 X iff ( rng b₂ = X & ( for l, m, k1, k2 being Nat st l < m & m < len b₂ & k1 = b₂ . l & k2 = b₂ . m holds
k1 < k2 ) ) );

registration

let A be finite natural-membered set ;
cluster Sgm0 A -> one-to-one ;
coherence
Sgm0 A is one-to-one

proof end;

end;

theorem Th31: :: AFINSQ_2:31

for A being finite natural-membered set holds len (Sgm0 A) = card A

proof end;

theorem Th32: :: AFINSQ_2:32

for X, Y being finite natural-membered set st X c= Y & X <> {} holds
(Sgm0 Y) . 0 <= (Sgm0 X) . 0

proof end;

theorem Th33: :: AFINSQ_2:33

for n being Nat holds (Sgm0 {n}) . 0 = n

proof end;

definition

let B1, B2 be set ;
pred B1 <N< B2 means :Def6: :: AFINSQ_2:def 6
for n, m being Nat st n in B1 & m in B2 holds
n < m;

end;

:: deftheorem Def6 defines <N< AFINSQ_2:def 6 :
for B1, B2 being set holds
( B1 <N< B2 iff for n, m being Nat st n in B1 & m in B2 holds
n < m );

definition

let B1, B2 be set ;
pred B1 <N= B2 means :Def7: :: AFINSQ_2:def 7
for n, m being Nat st n in B1 & m in B2 holds
n <= m;

end;

:: deftheorem Def7 defines <N= AFINSQ_2:def 7 :
for B1, B2 being set holds
( B1 <N= B2 iff for n, m being Nat st n in B1 & m in B2 holds
n <= m );

theorem Th34: :: AFINSQ_2:34

for B1, B2 being set st B1 <N< B2 holds
(B1 /\ B2) /\ NAT = {}

proof end;

theorem :: AFINSQ_2:35

for B1, B2 being finite natural-membered set st B1 <N< B2 holds
B1 misses B2

proof end;

theorem Th36: :: AFINSQ_2:36

for A, B1, B2 being set st B1 <N< B2 holds
A /\ B1 <N< A /\ B2

proof end;

theorem :: AFINSQ_2:37

for X, Y being finite natural-membered set st Y <> {} & ex x being set st
( x in X & {x} <N= Y ) holds
(Sgm0 X) . 0 <= (Sgm0 Y) . 0

proof end;

theorem Th38: :: AFINSQ_2:38

for i being Nat
for X0, Y0 being finite natural-membered set st X0 <N< Y0 & i < card X0 holds
( rng ((Sgm0 (X0 \/ Y0)) | (card X0)) = X0 & ((Sgm0 (X0 \/ Y0)) | (card X0)) . i = (Sgm0 (X0 \/ Y0)) . i )

proof end;

theorem :: AFINSQ_2:39

for i being Nat
for X, Y being finite natural-membered set st X <N< Y & i in card X holds
(Sgm0 (X \/ Y)) . i in X

proof end;

theorem Th40: :: AFINSQ_2:40

for i being Nat
for X, Y being finite natural-membered set st X <N< Y & i < len (Sgm0 X) holds
(Sgm0 X) . i = (Sgm0 (X \/ Y)) . i

proof end;

theorem Th41: :: AFINSQ_2:41

for i being Nat
for X0, Y0 being finite natural-membered set st X0 <N< Y0 & i < card Y0 holds
( rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = Y0 & ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . i = (Sgm0 (X0 \/ Y0)) . (i + (card X0)) )

proof end;

theorem Th42: :: AFINSQ_2:42

for i being Nat
for X, Y being finite natural-membered set st X <N< Y & i < len (Sgm0 Y) holds
(Sgm0 Y) . i = (Sgm0 (X \/ Y)) . (i + (len (Sgm0 X)))

proof end;

theorem Th43: :: AFINSQ_2:43

for X, Y being finite natural-membered set st Y <> {} & X <N< Y holds
(Sgm0 Y) . 0 = (Sgm0 (X \/ Y)) . (len (Sgm0 X))

proof end;

theorem Th44: :: AFINSQ_2:44

for l, m, n, k being Nat
for X being finite natural-membered set st k < l & m < len (Sgm0 X) & (Sgm0 X) . m = k & (Sgm0 X) . n = l holds
m < n

proof end;

theorem Th45: :: AFINSQ_2:45

for X, Y being finite natural-membered set st X <> {} & X <N< Y holds
(Sgm0 X) . 0 = (Sgm0 (X \/ Y)) . 0

proof end;

theorem Th46: :: AFINSQ_2:46

for X, Y being finite natural-membered set holds
( X <N< Y iff Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y) )

proof end;

definition

let f be XFinSequence;
let B be set ;
func SubXFinS (f,B) -> XFinSequence equals :: AFINSQ_2:def 8
f * (Sgm0 (B /\ (len f)));
coherence
f * (Sgm0 (B /\ (len f))) is XFinSequence

proof end;

end;

:: deftheorem defines SubXFinS AFINSQ_2:def 8 :
for f being XFinSequence
for B being set holds SubXFinS (f,B) = f * (Sgm0 (B /\ (len f)));

theorem Th47: :: AFINSQ_2:47

for p being XFinSequence
for B being set holds
( len (SubXFinS (p,B)) = card (B /\ (len p)) & ( for i being Nat st i < len (SubXFinS (p,B)) holds
(SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (len p))) . i) ) )

proof end;

registration

let D be set ;
let f be XFinSequence of D;
let B be set ;
cluster SubXFinS (f,B) -> D -valued ;
coherence
SubXFinS (f,B) is D -valued ;

end;

registration

let p be XFinSequence;
cluster SubXFinS (p,{}) -> empty ;
coherence
SubXFinS (p,{}) is empty

proof end;

end;

registration

let B be set ;
cluster SubXFinS ({},B) -> empty ;
coherence
SubXFinS ({},B) is empty ;

end;

theorem :: AFINSQ_2:48

canceled;

registration

let n be Nat;
let x be set ;
cluster n --> x -> T-Sequence-like ;
coherence
n --> x is T-Sequence-like

proof end;

end;

scheme :: AFINSQ_2:sch 2
Sch5{ F₁() -> set , P₁[ set ] } :

for F being XFinSequence of F₁() holds P₁[F]

provided

A1: P₁[ <%> F₁()] and
A2: for F being XFinSequence of F₁()
for d being Element of F₁() st P₁[F] holds
P₁[F ^ <%d%>]

proof end;

definition

let D be non empty set ;
let F be XFinSequence;
assume A1: F is D -valued ;
let b be BinOp of D;
assume A2: ( b is having_a_unity or len F >= 1 ) ;
func b "**" F -> Element of D means :Def9: :: AFINSQ_2:def 9
it = the_unity_wrt b if ( b is having_a_unity & len F = 0 )
otherwise ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & it = f . ((len F) - 1) );
existence
( ( b is having_a_unity & len F = 0 implies ex b₁ being Element of D st b₁ = the_unity_wrt b ) & ( ( not b is having_a_unity or not len F = 0 ) implies ex b₁ being Element of D ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b₁ = f . ((len F) - 1) ) ) )

proof end;

uniqueness
for b₁, b₂ being Element of D holds
( ( b is having_a_unity & len F = 0 & b₁ = the_unity_wrt b & b₂ = the_unity_wrt b implies b₁ = b₂ ) & ( ( not b is having_a_unity or not len F = 0 ) & ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b₁ = f . ((len F) - 1) ) & ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b₂ = f . ((len F) - 1) ) implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being Element of D holds verum ;

end;

:: deftheorem Def9 defines "**" AFINSQ_2:def 9 :
for D being non empty set
for F being XFinSequence st F is D -valued holds
for b being BinOp of D st ( b is having_a_unity or len F >= 1 ) holds
for b₄ being Element of D holds
( ( b is having_a_unity & len F = 0 implies ( b₄ = b "**" F iff b₄ = the_unity_wrt b ) ) & ( ( not b is having_a_unity or not len F = 0 ) implies ( b₄ = b "**" F iff ex f being Function of NAT,D st
( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b₄ = f . ((len F) - 1) ) ) ) );

theorem Th49: :: AFINSQ_2:49

for D being non empty set
for b being BinOp of D
for d being Element of D holds b "**" <%d%> = d

proof end;

theorem Th50: :: AFINSQ_2:50

for D being non empty set
for b being BinOp of D
for d1, d2 being Element of D holds b "**" <%d1,d2%> = b . (d1,d2)

proof end;

theorem Th51: :: AFINSQ_2:51

for D being non empty set
for b being BinOp of D
for d, d1, d2 being Element of D holds b "**" <%d,d1,d2%> = b . ((b . (d,d1)),d2)

proof end;

theorem Th52: :: AFINSQ_2:52

for D being non empty set
for F being XFinSequence of D
for b being BinOp of D
for d being Element of D st ( b is having_a_unity or len F > 0 ) holds
b "**" (F ^ <%d%>) = b . ((b "**" F),d)

proof end;

theorem Th53: :: AFINSQ_2:53

for D being non empty set
for F, G being XFinSequence of D
for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds
b "**" (F ^ G) = b . ((b "**" F),(b "**" G))

proof end;

theorem Th54: :: AFINSQ_2:54

for D being non empty set
for F, G being XFinSequence of D
for b being BinOp of D st b is associative & ( b is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds
b "**" (F ^ G) = b . ((b "**" F),(b "**" G))

proof end;

theorem Th55: :: AFINSQ_2:55

for n being Nat
for D being non empty set
for F being XFinSequence of D
for b being BinOp of D st n in dom F & ( b is having_a_unity or n <> 0 ) holds
b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1))

proof end;

theorem Th56: :: AFINSQ_2:56

for D being non empty set
for F being XFinSequence of D
for b being BinOp of D st ( b is having_a_unity or len F >= 1 ) holds
b "**" F = b "**" (XFS2FS F)

proof end;

theorem Th57: :: AFINSQ_2:57

for D being non empty set
for F, G being XFinSequence of D
for b being BinOp of D
for P being Permutation of (dom F) st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & G = F * P holds
b "**" F = b "**" G

proof end;

theorem :: AFINSQ_2:58

for D being non empty set
for F, G being XFinSequence of D
for b being BinOp of D
for bFG being XFinSequence of D st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & len F = len G & len F = len bFG & ( for n being Nat st n in dom bFG holds
bFG . n = b . ((F . n),(G . n)) ) holds
b "**" (F ^ G) = b "**" bFG

proof end;

theorem Th59: :: AFINSQ_2:59

for D being non empty set
for F being XFinSequence of D
for D1, D2 being non empty set
for b1 being BinOp of D1
for b2 being BinOp of D2 st len F >= 1 & D c= D1 /\ D2 & ( for x, y being set st x in D & y in D holds
( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ) holds
b1 "**" F = b2 "**" F

proof end;

Lm3: for cF being complex-valued XFinSequence holds cF is COMPLEX -valued

proof end;

Lm4: for rF being real-valued XFinSequence holds rF is REAL -valued

proof end;

definition

let F be XFinSequence;
func Sum F -> Element of COMPLEX equals :: AFINSQ_2:def 10
addcomplex "**" F;
coherence
addcomplex "**" F is Element of COMPLEX ;

end;

:: deftheorem defines Sum AFINSQ_2:def 10 :
for F being XFinSequence holds Sum F = addcomplex "**" F;

registration

let f be empty complex-valued XFinSequence;
cluster Sum f -> zero ;
coherence
Sum f is empty

proof end;

end;

theorem Th60: :: AFINSQ_2:60

for F being XFinSequence st F is real-valued holds
Sum F = addreal "**" F

proof end;

theorem Th61: :: AFINSQ_2:61

for F being XFinSequence st F is rational-valued holds
Sum F = addrat "**" F

proof end;

theorem Th62: :: AFINSQ_2:62

for F being XFinSequence st F is integer-valued holds
Sum F = addint "**" F

proof end;

theorem Th63: :: AFINSQ_2:63

for F being XFinSequence st F is natural-valued holds
Sum F = addnat "**" F

proof end;

registration

let F be real-valued XFinSequence;
cluster Sum F -> real ;
coherence
Sum F is real

proof end;

end;

registration

let F be rational-valued XFinSequence;
cluster Sum F -> rational ;
coherence
Sum F is rational

proof end;

end;

registration

let F be integer-valued XFinSequence;
cluster Sum F -> integer ;
coherence
Sum F is integer

proof end;

end;

registration

let F be natural-valued XFinSequence;
cluster Sum F -> natural ;
coherence
Sum F is natural

proof end;

end;

registration

cluster Relation-like natural-valued -> nonnegative-yielding set ;
coherence
for b₁ being Relation st b₁ is natural-valued holds
b₁ is nonnegative-yielding

proof end;

end;

theorem :: AFINSQ_2:64

for cF being complex-valued XFinSequence st cF = {} holds
Sum cF = 0 ;

theorem :: AFINSQ_2:65

for c being complex number holds Sum <%c%> = c

proof end;

theorem :: AFINSQ_2:66

for c1, c2 being complex number holds Sum <%c1,c2%> = c1 + c2

proof end;

theorem Th67: :: AFINSQ_2:67

for cF1, cF2 being complex-valued XFinSequence holds Sum (cF1 ^ cF2) = (Sum cF1) + (Sum cF2)

proof end;

theorem :: AFINSQ_2:68

for n being Nat
for rF being real-valued XFinSequence
for S being Real_Sequence st rF = S | (n + 1) holds
Sum rF = (Partial_Sums S) . n

proof end;

theorem Th69: :: AFINSQ_2:69

for rF1, rF2 being real-valued XFinSequence st len rF1 = len rF2 & ( for i being Nat st i in dom rF1 holds
rF1 . i <= rF2 . i ) holds
Sum rF1 <= Sum rF2

proof end;

theorem Th70: :: AFINSQ_2:70

for n being Nat
for c being complex number holds Sum (n --> c) = n * c

proof end;

theorem :: AFINSQ_2:71

for rF being real-valued XFinSequence
for r being real number st ( for n being Nat st n in dom rF holds
rF . n <= r ) holds
Sum rF <= (len rF) * r

proof end;

theorem :: AFINSQ_2:72

for rF being real-valued XFinSequence
for r being real number st ( for n being Nat st n in dom rF holds
rF . n >= r ) holds
Sum rF >= (len rF) * r

proof end;

theorem Th73: :: AFINSQ_2:73

for rF being real-valued XFinSequence
for r being real number st rF is nonnegative-yielding & len rF > 0 & ex x being set st
( x in dom rF & rF . x = r ) holds
Sum rF >= r

proof end;

theorem Th74: :: AFINSQ_2:74

for rF being real-valued XFinSequence st rF is nonnegative-yielding holds
( Sum rF = 0 iff ( len rF = 0 or rF = (len rF) --> 0 ) )

proof end;

theorem Th75: :: AFINSQ_2:75

for n being Nat
for cF being complex-valued XFinSequence
for c being complex number holds c (#) (cF | n) = (c (#) cF) | n

proof end;

theorem :: AFINSQ_2:76

for cF being complex-valued XFinSequence
for c being complex number holds c * (Sum cF) = Sum (c (#) cF)

proof end;

theorem Th77: :: AFINSQ_2:77

for n being Nat
for cF being complex-valued XFinSequence st n in dom cF holds
(Sum (cF | n)) + (cF . n) = Sum (cF | (n + 1))

proof end;

theorem Th78: :: AFINSQ_2:78

for y, x being set
for f being Function st f . y = x & y in dom f holds
{y} \/ ((f | ((dom f) \ {y})) " {x}) = f " {x}

proof end;

theorem Th79: :: AFINSQ_2:79

for y, x being set
for f being Function st f . y <> x holds
(f | ((dom f) \ {y})) " {x} = f " {x}

proof end;

theorem :: AFINSQ_2:80

for cF being complex-valued XFinSequence
for c being complex number st rng cF c= {0,c} holds
Sum cF = c * (card (cF " {c}))

proof end;

theorem :: AFINSQ_2:81

for cF being complex-valued XFinSequence holds Sum cF = Sum (Rev cF)

proof end;

theorem Th82: :: AFINSQ_2:82

for f being Function
for p, q, fp, fq being XFinSequence st rng p c= dom f & rng q c= dom f & fp = f * p & fq = f * q holds
fp ^ fq = f * (p ^ q)

proof end;

theorem :: AFINSQ_2:83

for cF being complex-valued XFinSequence
for B1, B2 being finite natural-membered set st B1 <N< B2 holds
Sum (SubXFinS (cF,(B1 \/ B2))) = (Sum (SubXFinS (cF,B1))) + (Sum (SubXFinS (cF,B2)))

proof end;

theorem Th84: :: AFINSQ_2:84

for D being non empty set
for b being BinOp of D st b is having_a_unity holds
b "**" (<%> D) = the_unity_wrt b

proof end;

definition

let D be set ;
let F be XFinSequence of D ^omega ;
func FlattenSeq F -> Element of D ^omega means :Def11: :: AFINSQ_2:def 11
ex g being BinOp of (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & it = g "**" F );
existence
ex b₁ being Element of D ^omega ex g being BinOp of (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b₁ = g "**" F )

proof end;

uniqueness
for b₁, b₂ being Element of D ^omega st ex g being BinOp of (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b₁ = g "**" F ) & ex g being BinOp of (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b₂ = g "**" F ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines FlattenSeq AFINSQ_2:def 11 :
for D being set
for F being XFinSequence of D ^omega
for b₃ being Element of D ^omega holds
( b₃ = FlattenSeq F iff ex g being BinOp of (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b₃ = g "**" F ) );

theorem :: AFINSQ_2:85

for D being set
for d being Element of D ^omega holds FlattenSeq <%d%> = d

proof end;

theorem :: AFINSQ_2:86

for D being set holds FlattenSeq (<%> (D ^omega)) = <%> D

proof end;

theorem Th87: :: AFINSQ_2:87

for D being set
for F, G being XFinSequence of D ^omega holds FlattenSeq (F ^ G) = (FlattenSeq F) ^ (FlattenSeq G)

proof end;

theorem :: AFINSQ_2:88

for D being set
for p, q being Element of D ^omega holds FlattenSeq <%p,q%> = p ^ q

proof end;

theorem :: AFINSQ_2:89

for D being set
for p, q, r being Element of D ^omega holds FlattenSeq <%p,q,r%> = (p ^ q) ^ r

proof end;

theorem Th90: :: AFINSQ_2:90

for p, q being XFinSequence st p c= q holds
p ^ (q /^ (len p)) = q

proof end;

theorem Th91: :: AFINSQ_2:91

for p, q being XFinSequence st p c= q holds
ex r being XFinSequence st p ^ r = q

proof end;

theorem Th92: :: AFINSQ_2:92

for D being non empty set
for p, q being XFinSequence of D st p c= q holds
ex r being XFinSequence of D st p ^ r = q

proof end;

theorem :: AFINSQ_2:93

for q, p, r being XFinSequence st q c= r holds
p ^ q c= p ^ r

proof end;

theorem :: AFINSQ_2:94

for D being set
for F, G being XFinSequence of D ^omega st F c= G holds
FlattenSeq F c= FlattenSeq G

proof end;