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

Lm1: 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 object st x in i holds
x is Element of NAT
proof end;

theorem Th2: :: AFINSQ_2:2
for X0 being finite natural-membered set ex n being Nat st X0 c= Segm n
proof end;

theorem Th3: :: AFINSQ_2:3
for x being object
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{ F1() -> Nat, F2() -> non empty set , F3( set ) -> Element of F2() } :
ex p being XFinSequence of F2() st
( len p = F1() & ( for j being Nat st j in F1() holds
p . j = F3(j) ) )
proof end;

registration
existence
ex b1 being XFinSequence st
( b1 is empty & b1 is natural-valued )
proof end;
let p be Sequence-like complex-valued Function;
coherence
proof end;
coherence
proof end;
coherence
proof end;
coherence
proof end;
let q be Sequence-like complex-valued Function;
coherence
p + q is Sequence-like
proof end;
coherence
p - q is Sequence-like
;
coherence
p (#) q is Sequence-like
proof end;
coherence
p /" q is Sequence-like
;
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;
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
;
cluster p (#) q -> finite ;
coherence
p (#) q is finite
proof end;
cluster p /" q -> finite ;
coherence
p /" q is finite
;
cluster q /" p -> finite ;
coherence
q /" p is finite
;
end;

registration
let p be Sequence-like complex-valued Function;
let c be Complex;
coherence
c + p is Sequence-like
proof end;
coherence
p - c is Sequence-like
;
coherence
c (#) p is Sequence-like
proof end;
end;

registration
let p be complex-valued finite Function;
let c be Complex;
cluster c + p -> finite ;
coherence
c + p is finite
proof end;
cluster p - c -> finite ;
coherence
p - c is finite
;
cluster c (#) p -> finite ;
coherence
c (#) p is finite
proof end;
end;

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 b1 being XFinSequence st
( len b1 = len p & ( for i being Nat st i in dom b1 holds
b1 . i = p . ((len p) - (i + 1)) ) )
proof end;
uniqueness
for b1, b2 being XFinSequence st len b1 = len p & ( for i being Nat st i in dom b1 holds
b1 . i = p . ((len p) - (i + 1)) ) & len b2 = len p & ( for i being Nat st i in dom b2 holds
b2 . i = p . ((len p) - (i + 1)) ) holds
b1 = b2
proof end;
end;

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

theorem Th5: :: AFINSQ_2:5
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;

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 b1 being XFinSequence st
( len b1 = (len p) -' n & ( for m being Nat st m in dom b1 holds
b1 . m = p . (m + n) ) )
proof end;
uniqueness
for b1, b2 being XFinSequence st len b1 = (len p) -' n & ( for m being Nat st m in dom b1 holds
b1 . m = p . (m + n) ) & len b2 = (len p) -' n & ( for m being Nat st m in dom b2 holds
b2 . m = p . (m + n) ) holds
b1 = b2
proof end;
end;

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

theorem Th6: :: AFINSQ_2:6
for n being Nat
for p being XFinSequence st n >= len p holds
p /^ n = {}
proof end;

theorem Th7: :: AFINSQ_2:7
for n being Nat
for p being XFinSequence st n < len p holds
len (p /^ n) = (len p) - n
proof end;

theorem Th8: :: AFINSQ_2:8
for n, m 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 Th9: :: AFINSQ_2:9
for n being Nat
for p being XFinSequence holds rng (p /^ n) c= rng p
proof end;

theorem Th10: :: AFINSQ_2:10
for p being XFinSequence holds p /^ 0 = p
proof end;

theorem Th11: :: AFINSQ_2:11
for i being Nat
for p, q being XFinSequence holds (p ^ q) /^ ((len p) + i) = q /^ i
proof end;

theorem Th12: :: AFINSQ_2:12
for p, q being XFinSequence holds (p ^ q) /^ (len p) = q
proof end;

theorem Th13: :: AFINSQ_2:13
for n being Nat
for p being XFinSequence holds (p | n) ^ (p /^ n) = p
proof end;

registration
let f be XFinSequence;
cluster f | 0 -> empty ;
coherence
f | 0 is empty
;
let n be Nat;
cluster f /^ ((dom f) + n) -> empty ;
coherence
f /^ ((dom f) + n) is empty
proof end;
reduce f | ((len f) + n) to f;
reducibility
f | ((len f) + n) = f
proof end;
reduce (f | n) ^ (f /^ n) to f;
reducibility
(f | n) ^ (f /^ n) = f
by Th13;
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 Th14: :: AFINSQ_2:14
for p being XFinSequence
for k1, k2 being Nat st k1 > k2 holds
mid (p,k1,k2) = {}
proof end;

theorem :: AFINSQ_2:15
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 Th16: :: AFINSQ_2:16
for k being Nat
for p being XFinSequence holds mid (p,1,k) = p | k
proof end;

theorem :: AFINSQ_2:17
for k being Nat
for p being XFinSequence st len p <= k holds
mid (p,1,k) = p
proof end;

theorem :: AFINSQ_2:18
for k being Nat
for p being XFinSequence holds mid (p,0,k) = mid (p,1,k)
proof end;

theorem :: AFINSQ_2:19
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
let X be finite natural-membered set ;
func Sgm0 X -> XFinSequence of NAT means :Def4: :: AFINSQ_2:def 4
( 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 b1 being XFinSequence of NAT st
( rng b1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) )
proof end;
uniqueness
for b1, b2 being XFinSequence of NAT st rng b1 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) & rng b2 = X & ( for l, m, k1, k2 being Nat st l < m & m < len b2 & k1 = b2 . l & k2 = b2 . m holds
k1 < k2 ) holds
b1 = b2
proof end;
end;

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

registration
let A be finite natural-membered set ;
coherence
proof end;
end;

theorem Th20: :: AFINSQ_2:20
for A being finite natural-membered set holds len (Sgm0 A) = card A
proof end;

theorem Th21: :: AFINSQ_2:21
for X, Y being finite natural-membered set st X c= Y & X <> {} holds
(Sgm0 Y) . 0 <= (Sgm0 X) . 0
proof end;

theorem Th22: :: AFINSQ_2:22
for n being Nat holds () . 0 = n
proof end;

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

:: deftheorem defines <N< AFINSQ_2:def 5 :
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 :: AFINSQ_2:def 6
for n, m being Nat st n in B1 & m in B2 holds
n <= m;
end;

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

theorem Th23: :: AFINSQ_2:23
for B1, B2 being set st B1 <N< B2 holds
(B1 /\ B2) /\ NAT = {}
proof end;

theorem :: AFINSQ_2:24
for B1, B2 being finite natural-membered set st B1 <N< B2 holds
B1 misses B2
proof end;

theorem Th25: :: AFINSQ_2:25
for A, B1, B2 being set st B1 <N< B2 holds
A /\ B1 <N< A /\ B2
proof end;

theorem :: AFINSQ_2:26
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 Th27: :: AFINSQ_2:27
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:28
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 Th29: :: AFINSQ_2:29
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 Th30: :: AFINSQ_2:30
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 Th31: :: AFINSQ_2:31
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 Th32: :: AFINSQ_2:32
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 Th33: :: AFINSQ_2:33
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 Th34: :: AFINSQ_2:34
for X, Y being finite natural-membered set st X <> {} & X <N< Y holds
(Sgm0 X) . 0 = (Sgm0 (X \/ Y)) . 0
proof end;

theorem Th35: :: AFINSQ_2:35
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 ;
::Following is a subsequence selected from f by B.
func SubXFinS (f,B) -> XFinSequence equals :: AFINSQ_2:def 7
f * (Sgm0 (B /\ (Segm (len f))));
coherence
f * (Sgm0 (B /\ (Segm (len f)))) is XFinSequence
proof end;
end;

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

theorem Th36: :: AFINSQ_2:36
for p being XFinSequence
for B being set holds
( len (SubXFinS (p,B)) = card (B /\ (Segm (len p))) & ( for i being Nat st i < len (SubXFinS (p,B)) holds
(SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (Segm (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;

scheme :: AFINSQ_2:sch 2
Sch5{ F1() -> set , P1[ set ] } :
for F being XFinSequence of F1() holds P1[F]
provided
A1: P1[ <%> F1()] and
A2: for F being XFinSequence of F1()
for d being Element of F1() st P1[F] holds
P1[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 :Def8: :: AFINSQ_2:def 8
it = the_unity_wrt b if ( b is having_a_unity & len F = 0 )
otherwise ex f being sequence of 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 b1 being Element of D st b1 = the_unity_wrt b ) & ( ( not b is having_a_unity or not len F = 0 ) implies ex b1 being Element of D ex f being sequence of 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))) ) & b1 = f . ((len F) - 1) ) ) )
proof end;
uniqueness
for b1, b2 being Element of D holds
( ( b is having_a_unity & len F = 0 & b1 = the_unity_wrt b & b2 = the_unity_wrt b implies b1 = b2 ) & ( ( not b is having_a_unity or not len F = 0 ) & ex f being sequence of 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))) ) & b1 = f . ((len F) - 1) ) & ex f being sequence of 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))) ) & b2 = f . ((len F) - 1) ) implies b1 = b2 ) )
proof end;
consistency
for b1 being Element of D holds verum
;
end;

:: deftheorem Def8 defines "**" AFINSQ_2:def 8 :
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 b4 being Element of D holds
( ( b is having_a_unity & len F = 0 implies ( b4 = b "**" F iff b4 = the_unity_wrt b ) ) & ( ( not b is having_a_unity or not len F = 0 ) implies ( b4 = b "**" F iff ex f being sequence of 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))) ) & b4 = f . ((len F) - 1) ) ) ) );

theorem Th37: :: AFINSQ_2:37
for D being non empty set
for b being BinOp of D
for d being Element of D holds b "**" <%d%> = d
proof end;

reconsider zz = 0 as Nat ;

theorem Th38: :: AFINSQ_2:38
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 Th39: :: AFINSQ_2:39
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 Th40: :: AFINSQ_2:40
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 :: AFINSQ_2:41
canceled;

::\$CT
theorem Th41: :: AFINSQ_2:42
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 Th42: :: AFINSQ_2:43
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 Th43: :: AFINSQ_2:44
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 "**" ()
proof end;

theorem Th44: :: AFINSQ_2:45
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:46
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 Th46: :: AFINSQ_2:47
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 object 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;

Lm2: for cF being complex-valued XFinSequence holds cF is COMPLEX -valued
proof end;

Lm3: 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 9
coherence ;
end;

:: deftheorem defines Sum AFINSQ_2:def 9 :
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 zero
proof end;
end;

theorem Th47: :: AFINSQ_2:48
for F being XFinSequence st F is real-valued holds
Sum F = addreal "**" F
proof end;

theorem Th48: :: AFINSQ_2:49
for F being XFinSequence st F is RAT -valued holds
Sum F = addrat "**" F
proof end;

theorem Th49: :: AFINSQ_2:50
for F being XFinSequence st F is INT -valued holds
Sum F = addint "**" F
proof end;

theorem Th50: :: AFINSQ_2:51
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 RAT -valued XFinSequence;
coherence
Sum F is rational
proof end;
end;

registration
let F be INT -valued XFinSequence;
coherence
Sum F is integer
proof end;
end;

registration
let F be natural-valued XFinSequence;
coherence
Sum F is natural
proof end;
end;

registration
coherence
for b1 being Relation st b1 is natural-valued holds
b1 is nonnegative-yielding
proof end;
end;

theorem :: AFINSQ_2:52
for cF being complex-valued XFinSequence st cF = {} holds
Sum cF = 0 ;

theorem :: AFINSQ_2:53
for c being Complex holds Sum <%c%> = c
proof end;

theorem :: AFINSQ_2:54
for c1, c2 being Complex holds Sum <%c1,c2%> = c1 + c2
proof end;

theorem Th54: :: AFINSQ_2:55
for cF1, cF2 being complex-valued XFinSequence holds Sum (cF1 ^ cF2) = (Sum cF1) + (Sum cF2)
proof end;

theorem :: AFINSQ_2:56
for n being Nat
for rF being real-valued XFinSequence
for S being Real_Sequence st rF = S | (n + 1) holds
Sum rF = () . n
proof end;

theorem Th56: :: AFINSQ_2:57
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 Th57: :: AFINSQ_2:58
for n being Nat
for c being Complex holds Sum (n --> c) = n * c
proof end;

theorem :: AFINSQ_2:59
for rF being real-valued XFinSequence
for r being Real 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:60
for rF being real-valued XFinSequence
for r being Real st ( for n being Nat st n in dom rF holds
rF . n >= r ) holds
Sum rF >= (len rF) * r
proof end;

theorem Th60: :: AFINSQ_2:61
for rF being real-valued XFinSequence
for r being Real st rF is nonnegative-yielding & len rF > 0 & ex x being object st
( x in dom rF & rF . x = r ) holds
Sum rF >= r
proof end;

theorem Th61: :: AFINSQ_2:62
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 Th62: :: AFINSQ_2:63
for n being Nat
for cF being complex-valued XFinSequence
for c being Complex holds c (#) (cF | n) = (c (#) cF) | n
proof end;

theorem :: AFINSQ_2:64
for cF being complex-valued XFinSequence
for c being Complex holds c * (Sum cF) = Sum (c (#) cF)
proof end;

theorem Th64: :: AFINSQ_2:65
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 Th65: :: AFINSQ_2:66
for x, y being object
for f being Function st f . y = x & y in dom f holds
{y} \/ ((f | ((dom f) \ {y})) " {x}) = f " {x}
proof end;

theorem Th66: :: AFINSQ_2:67
for x, y being object
for f being Function st f . y <> x holds
(f | ((dom f) \ {y})) " {x} = f " {x}
proof end;

theorem :: AFINSQ_2:68
for cF being complex-valued XFinSequence
for c being Complex st rng cF c= {0,c} holds
Sum cF = c * (card (cF " {c}))
proof end;

theorem :: AFINSQ_2:69
for cF being complex-valued XFinSequence holds Sum cF = Sum (Rev cF)
proof end;

theorem Th69: :: AFINSQ_2:70
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:71
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;

:: missing, 2010.05.15, A.T.
theorem Th71: :: AFINSQ_2:72
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 :Def10: :: AFINSQ_2:def 10
ex g being BinOp of () st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & it = g "**" F );
existence
ex b1 being Element of D ^omega ex g being BinOp of () st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b1 = g "**" F )
proof end;
uniqueness
for b1, b2 being Element of D ^omega st ex g being BinOp of () st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b1 = g "**" F ) & ex g being BinOp of () st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b2 = g "**" F ) holds
b1 = b2
proof end;
end;

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

theorem :: AFINSQ_2:73
for D being set
for d being Element of D ^omega holds FlattenSeq <%d%> = d
proof end;

theorem :: AFINSQ_2:74
for D being set holds FlattenSeq (<%> ()) = <%> D
proof end;

theorem Th74: :: AFINSQ_2:75
for D being set
for F, G being XFinSequence of D ^omega holds FlattenSeq (F ^ G) = () ^ ()
proof end;

theorem :: AFINSQ_2:76
for D being set
for p, q being Element of D ^omega holds FlattenSeq <%p,q%> = p ^ q
proof end;

theorem :: AFINSQ_2:77
for D being set
for p, q, r being Element of D ^omega holds FlattenSeq <%p,q,r%> = (p ^ q) ^ r
proof end;

theorem Th77: :: AFINSQ_2:78
for p, q being XFinSequence st p c= q holds
p ^ (q /^ (len p)) = q
proof end;

theorem Th78: :: AFINSQ_2:79
for p, q being XFinSequence st p c= q holds
ex r being XFinSequence st p ^ r = q
proof end;

theorem Th79: :: AFINSQ_2:80
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:81
for p, q, r being XFinSequence st q c= r holds
p ^ q c= p ^ r
proof end;

theorem :: AFINSQ_2:82
for D being set
for F, G being XFinSequence of D ^omega st F c= G holds
FlattenSeq F c= FlattenSeq G
proof end;

registration
let p be XFinSequence;
let q be non empty XFinSequence;
cluster p ^ q -> non empty ;
coherence
not p ^ q is empty
by AFINSQ_1:30;
cluster q ^ p -> non empty ;
coherence
not q ^ p is empty
by AFINSQ_1:30;
end;

theorem :: AFINSQ_2:83
for x being object
for p being XFinSequence holds CutLastLoc (p ^ <%x%>) = p
proof end;

:: generalizes BALLOT_1:1 to empty D
theorem Th17: :: AFINSQ_2:84
for D being set
for p being XFinSequence of D
for n being Nat holds
( XFS2FS (p | n) = () | n & XFS2FS (p /^ n) = () /^ n )
proof end;

theorem Th5: :: AFINSQ_2:85
for D being set
for d being FinSequence of D holds XFS2FS () = d
proof end;

registration
let D be set ;
let f be FinSequence of D;
reduce XFS2FS () to f;
reducibility
XFS2FS () = f
by Th5;
end;

theorem :: AFINSQ_2:86
for D being set
for p being FinSequence of D
for n being Nat holds
( () | n = FS2XFS (p | n) & () /^ n = FS2XFS (p /^ n) )
proof end;

:: analogous theorem of FINSEQ_5:34
theorem :: AFINSQ_2:87
for D being set
for p being one-to-one XFinSequence of D
for n being Nat holds rng (p | n) misses rng (p /^ n)
proof end;

registration
existence
ex b1 being Ordinal-Sequence st b1 is finite
proof end;
end;

registration
let A be finite Ordinal-Sequence;
let n be Nat;
coherence
proof end;
end;