:: 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-2012 Association of Mizar Users


begin

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

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 )
proofend;

theorem Th1: :: AFINSQ_2:1
for i being Nat
for x being set st x in i holds
x is Element of NAT
proofend;

registration
cluster natural  ->  natural-membered for set ;
coherence
 for b1 being Nat holds b1 is natural-membered
proofend;
end;

begin

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

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 )
proofend;

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
proofend;

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) ) )
proofend;

registration
cluster Relation-like NAT -defined Function-like empty T-Sequence-like natural-valued finite V86() for set ;
existence
 ex b1 being XFinSequence st
( b1 is empty & b1 is natural-valued )
proofend;
let p be T-Sequence-like complex-valued Function;
cluster - p ->  T-Sequence-like ;
coherence
 - p is T-Sequence-like
proofend;
clusterp "  ->  T-Sequence-like ;
coherence
 p " is T-Sequence-like
proofend;
clusterp ^2  ->  T-Sequence-like ;
coherence
 p ^2 is T-Sequence-like
proofend;
cluster|.p.| ->  T-Sequence-like ;
coherence
 abs p is T-Sequence-like
proofend;
let q be T-Sequence-like complex-valued Function;
clusterp + q ->  T-Sequence-like ;
coherence
 p + q is T-Sequence-like
proofend;
clusterp - q ->  T-Sequence-like ;
coherence
 p - q is T-Sequence-like ;
clusterp (#) q ->  T-Sequence-like ;
coherence
 p (#) q is T-Sequence-like
proofend;
clusterp /" q ->  T-Sequence-like ;
coherence
 p /" q is T-Sequence-like ;
end;

registration
let p be complex-valued finite Function;
cluster - p ->  finite ;
coherence
 - p is finite
proofend;
clusterp "  ->  finite ;
coherence
 p " is finite
proofend;
clusterp ^2  ->  finite ;
coherence
 p ^2 is finite
proofend;
cluster|.p.| ->  finite ;
coherence
 abs p is finite
proofend;
let q be complex-valued Function;
clusterp + q ->  finite ;
coherence
 p + q is finite
proofend;
clusterp - q ->  finite ;
coherence
 p - q is finite ;
clusterp (#) q ->  finite ;
coherence
 p (#) q is finite
proofend;
clusterp /" q ->  finite ;
coherence
 p /" q is finite ;
clusterq /" p ->  finite ;
coherence
 q /" p is finite ;
end;

registration
let p be T-Sequence-like complex-valued Function;
let c be complex number ;
clusterc + p ->  T-Sequence-like ;
coherence
 c + p is T-Sequence-like
proofend;
clusterp - c ->  T-Sequence-like ;
coherence
 p - c is T-Sequence-like ;
clusterc (#) p ->  T-Sequence-like ;
coherence
 c (#) p is T-Sequence-like
proofend;
end;

registration
let p be complex-valued finite Function;
let c be complex number ;
clusterc + p ->  finite ;
coherence
 c + p is finite
proofend;
clusterp - c ->  finite ;
coherence
 p - c is finite ;
clusterc (#) p ->  finite ;
coherence
 c (#) p is finite
proofend;
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)) ) )
proofend;
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
proofend;
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) )
proofend;

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

definition
let p be XFinSequence;
let n be Nat;
funcp /^ 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) ) )
proofend;
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
proofend;
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 = {}
proofend;

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

theorem Th8: :: AFINSQ_2:8
for m, n being Nat
for p being XFinSequence st m + n < len p holds
(p /^ n) . m = p . (m + n)
proofend;

registration
let f be one-to-one XFinSequence;
let n be Nat;
clusterf /^ n ->  one-to-one ;
coherence
 f /^ n is one-to-one
proofend;
end;

theorem Th9: :: AFINSQ_2:9
for n being Nat
for p being XFinSequence holds rng (p /^ n) c= rng p
proofend;

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

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

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

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

registration
let D be set ;
let f be XFinSequence of D;
let n be Nat;
clusterf /^ n -> D -valued ;
coherence
 f /^ n is D -valued
proofend;
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) = {}
proofend;

theorem :: AFINSQ_2:15
for p being XFinSequence
for k1, k2 being Nat st 1 <= k1 &amp; k2 <= len p holds
mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1)
proofend;

theorem Th16: :: AFINSQ_2:16
for k being Nat
for p being XFinSequence holds mid (p,1,k) = p | k
proofend;

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

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

theorem :: AFINSQ_2:19
for p, q being XFinSequence holds mid ((p ^ q),((len p) + 1),((len p) + (len q))) = q
proofend;

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;

begin

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

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

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

theorem Th22: :: AFINSQ_2:22
for n being Nat holds (Sgm0 {n}) . 0 = n
proofend;

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

:: deftheorem Def5 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 &amp; m in B2 holds
n < m );

definition
let B1, B2 be set ;
predB1 <N= B2 means :Def6: :: AFINSQ_2:def 6
 for n, m being Nat st n in B1 &amp; 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 &amp; m in B2 holds
n <= m );

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

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

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

theorem :: AFINSQ_2:26
for X, Y being finite natural-membered set st Y <> {} &amp; ex x being set st
( x in X &amp; {x} <N= Y ) holds
(Sgm0 X) . 0 <= (Sgm0 Y) . 0
proofend;

theorem Th27: :: AFINSQ_2:27
for i being Nat
for X0, Y0 being finite natural-membered set st X0 <N< Y0 &amp; i < card X0 holds
( rng ((Sgm0 (X0 \/ Y0)) | (card X0)) = X0 &amp; ((Sgm0 (X0 \/ Y0)) | (card X0)) . i = (Sgm0 (X0 \/ Y0)) . i )
proofend;

theorem :: AFINSQ_2:28
for i being Nat
for X, Y being finite natural-membered set st X <N< Y &amp; i in card X holds
(Sgm0 (X \/ Y)) . i in X
proofend;

theorem Th29: :: AFINSQ_2:29
for i being Nat
for X, Y being finite natural-membered set st X <N< Y &amp; i < len (Sgm0 X) holds
(Sgm0 X) . i = (Sgm0 (X \/ Y)) . i
proofend;

theorem Th30: :: AFINSQ_2:30
for i being Nat
for X0, Y0 being finite natural-membered set st X0 <N< Y0 &amp; i < card Y0 holds
( rng ((Sgm0 (X0 \/ Y0)) /^ (card X0)) = Y0 &amp; ((Sgm0 (X0 \/ Y0)) /^ (card X0)) . i = (Sgm0 (X0 \/ Y0)) . (i + (card X0)) )
proofend;

theorem Th31: :: AFINSQ_2:31
for i being Nat
for X, Y being finite natural-membered set st X <N< Y &amp; i < len (Sgm0 Y) holds
(Sgm0 Y) . i = (Sgm0 (X \/ Y)) . (i + (len (Sgm0 X)))
proofend;

theorem Th32: :: AFINSQ_2:32
for X, Y being finite natural-membered set st Y <> {} &amp; X <N< Y holds
(Sgm0 Y) . 0 = (Sgm0 (X \/ Y)) . (len (Sgm0 X))
proofend;

theorem Th33: :: AFINSQ_2:33
for l, m, n, k being Nat
for X being finite natural-membered set st k < l &amp; m < len (Sgm0 X) &amp; (Sgm0 X) . m = k &amp; (Sgm0 X) . n = l holds
m < n
proofend;

theorem Th34: :: AFINSQ_2:34
for X, Y being finite natural-membered set st X <> {} &amp; X <N< Y holds
(Sgm0 X) . 0 = (Sgm0 (X \/ Y)) . 0
proofend;

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) )
proofend;

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

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

theorem Th36: :: AFINSQ_2:36
for p being XFinSequence
for B being set holds
( len (SubXFinS (p,B)) = card (B /\ (len p)) &amp; ( for i being Nat st i < len (SubXFinS (p,B)) holds
(SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (len p))) . i) ) )
proofend;

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
proofend;
end;

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

registration
let n be Nat;
let x be set ;
clustern --> x ->  T-Sequence-like ;
coherence
 n --> x is T-Sequence-like ;
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%>]
proofend;

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 ) ;
funcb "**" F ->  Element of D means :Def8: :: AFINSQ_2:def 8
it = the_unity_wrt b if ( b is having_a_unity &amp; len F = 0 )
otherwise  ex f being Function of NAT,D st
( f . 0 = F . 0 &amp; ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) &amp; it = f . ((len F) - 1) );
existence
 ( ( b is having_a_unity &amp; len F = 0 implies ex b1 being Element of D st b1 = the_unity_wrt b ) &amp; ( ( 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 &amp; ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) &amp; b1 = f . ((len F) - 1) ) ) )
proofend;
uniqueness
 for b1, b2 being Element of D holds
( ( b is having_a_unity &amp; len F = 0 &amp; b1 = the_unity_wrt b &amp; b2 = the_unity_wrt b implies b1 = b2 ) &amp; ( ( not b is having_a_unity or not len F = 0 ) &amp; ex f being Function of NAT,D st
( f . 0 = F . 0 &amp; ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) &amp; b1 = f . ((len F) - 1) ) &amp; ex f being Function of NAT,D st
( f . 0 = F . 0 &amp; ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) &amp; b2 = f . ((len F) - 1) ) implies b1 = b2 ) )
proofend;
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 &amp; len F = 0 implies ( b4 = b "**" F iff b4 = the_unity_wrt b ) ) &amp; ( ( 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 &amp; ( for n being Nat st n + 1 < len F holds
f . (n + 1) = b . ((f . n),(F . (n + 1))) ) &amp; 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
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

theorem Th41: :: AFINSQ_2:41
for D being non empty set
for F, G being XFinSequence of D
for b being BinOp of D st b is associative &amp; ( b is having_a_unity or ( len F >= 1 &amp; len G >= 1 ) ) holds
b "**" (F ^ G) = b . ((b "**" F),(b "**" G))
proofend;

theorem Th42: :: 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 &amp; ( b is having_a_unity or ( len F >= 1 &amp; len G >= 1 ) ) holds
b "**" (F ^ G) = b . ((b "**" F),(b "**" G))
proofend;

theorem Th43: :: 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 &amp; ( b is having_a_unity or n <> 0 ) holds
b . ((b "**" (F | n)),(F . n)) = b "**" (F | (n + 1))
proofend;

theorem Th44: :: 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 "**" (XFS2FS F)
proofend;

theorem Th45: :: 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 &amp; b is associative &amp; ( b is having_a_unity or len F >= 1 ) &amp; G = F * P holds
b "**" F = b "**" G
proofend;

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 &amp; b is associative &amp; ( b is having_a_unity or len F >= 1 ) &amp; len F = len G &amp; len F = len bFG &amp; ( for n being Nat st n in dom bFG holds
bFG . n = b . ((F . n),(G . n)) ) holds
b "**" (F ^ G) = b "**" bFG
proofend;

theorem Th47: :: 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 &amp; D c= D1 /\ D2 &amp; ( for x, y being set st x in D &amp; y in D holds
( b1 . (x,y) = b2 . (x,y) &amp; b1 . (x,y) in D ) ) holds
b1 "**" F = b2 "**" F
proofend;

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

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

definition
let F be XFinSequence;
func Sum F ->  Element of COMPLEX  equals :: AFINSQ_2:def 9
addcomplex "**" F;
coherence
 addcomplex "**" F is Element of COMPLEX ;
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 empty
proofend;
end;

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

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

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

theorem Th51: :: AFINSQ_2:51
for F being XFinSequence st F is natural-valued holds
Sum F = addnat "**" F
proofend;

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

registration
let F be RAT -valued XFinSequence;
cluster Sum F ->  rational ;
coherence
 Sum F is rational
proofend;
end;

registration
let F be INT -valued XFinSequence;
cluster Sum F ->  integer ;
coherence
 Sum F is integer
proofend;
end;

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

registration
cluster Relation-like natural-valued  ->  nonnegative-yielding for set ;
coherence
 for b1 being Relation st b1 is natural-valued holds
b1 is nonnegative-yielding
proofend;
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 number holds Sum <%c%> = c
proofend;

theorem :: AFINSQ_2:54
for c1, c2 being complex number holds Sum <%c1,c2%> = c1 + c2
proofend;

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

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 = (Partial_Sums S) . n
proofend;

theorem Th57: :: AFINSQ_2:57
for rF1, rF2 being real-valued XFinSequence st len rF1 = len rF2 &amp; ( for i being Nat st i in dom rF1 holds
rF1 . i <= rF2 . i ) holds
Sum rF1 <= Sum rF2
proofend;

theorem Th58: :: AFINSQ_2:58
for n being Nat
for c being complex number holds Sum (n --> c) = n * c
proofend;

theorem :: AFINSQ_2:59
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
proofend;

theorem :: AFINSQ_2:60
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
proofend;

theorem Th61: :: AFINSQ_2:61
for rF being real-valued XFinSequence
for r being real number st rF is nonnegative-yielding &amp; len rF > 0 &amp; ex x being set st
( x in dom rF &amp; rF . x = r ) holds
Sum rF >= r
proofend;

theorem Th62: :: 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 ) )
proofend;

theorem Th63: :: AFINSQ_2:63
for n being Nat
for cF being complex-valued XFinSequence
for c being complex number holds c (#) (cF | n) = (c (#) cF) | n
proofend;

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

theorem Th65: :: 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))
proofend;

theorem Th66: :: AFINSQ_2:66
for y, x being set
for f being Function st f . y = x &amp; y in dom f holds
{y} \/ ((f | ((dom f) \ {y})) " {x}) = f " {x}
proofend;

theorem Th67: :: AFINSQ_2:67
for y, x being set
for f being Function st f . y <> x holds
(f | ((dom f) \ {y})) " {x} = f " {x}
proofend;

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

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

theorem Th70: :: AFINSQ_2:70
for f being Function
for p, q, fp, fq being XFinSequence st rng p c= dom f &amp; rng q c= dom f &amp; fp = f * p &amp; fq = f * q holds
fp ^ fq = f * (p ^ q)
proofend;

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)))
proofend;

:: missing, 2010.05.15, A.T.
theorem Th72: :: 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
proofend;

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 (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) &amp; 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 ) &amp; b1 = g "**" F )
proofend;
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 ) &amp; b1 = g "**" F ) &amp; ex g being BinOp of (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) &amp; b2 = g "**" F ) holds
b1 = b2
proofend;
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 (D ^omega) st
( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) &amp; b3 = g "**" F ) );

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

theorem :: AFINSQ_2:74
for D being set holds FlattenSeq (<%> (D ^omega)) = <%> D
proofend;

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

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

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
proofend;

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

theorem Th79: :: AFINSQ_2:79
for p, q being XFinSequence st p c= q holds
ex r being XFinSequence st p ^ r = q
proofend;

theorem Th80: :: 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
proofend;

theorem :: AFINSQ_2:81
for q, p, r being XFinSequence st q c= r holds
p ^ q c= p ^ r
proofend;

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
proofend;

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

theorem :: AFINSQ_2:83
for x being set
for p being XFinSequence holds CutLastLoc (p ^ <%x%>) = p
proofend;