:: 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 b1 being Nat holds b1 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{ 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;

theorem :: AFINSQ_2:5
canceled;

registration
cluster Relation-like NAT -defined Function-like empty T-Sequence-like natural-valued finite V176() set ;
existence
ex b1 being XFinSequence st
( b1 is empty & b1 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 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 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 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 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 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 Def5 defines Sgm0 AFINSQ_2:def 5 :
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 ;
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{ 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 :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 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 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))) ) & 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 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))) ) & b1 = 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))) ) & b2 = f . ((len F) - 1) ) implies b1 = b2 ) )
proof end;
consistency
for b1 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 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 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))) ) & b4 = 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 b1 being Relation st b1 is natural-valued holds
b1 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 b1 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 ) & b1 = g "**" F )
proof end;
uniqueness
for b1, b2 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 ) & b1 = g "**" F ) & ex g being BinOp of (D ^omega) 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 Def11 defines FlattenSeq AFINSQ_2:def 11 :
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 (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b3 = 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;