:: 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-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{ 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;

registration

cluster Relation-like omega -defined Function-like empty Sequence-like natural-valued finite V93() for set ;

existence
ex b₁ being XFinSequence st
( b₁ is empty & b₁ is natural-valued )

proof end;

let p be Sequence-like complex-valued Function;

cluster - p -> Sequence-like ;

coherence
- p is Sequence-like

proof end;

cluster p " -> Sequence-like ;

coherence
p " is Sequence-like

proof end;

cluster p ^2 -> Sequence-like ;

coherence
p ^2 is Sequence-like

proof end;

cluster |.p.| -> Sequence-like ;

coherence
abs p is Sequence-like

proof end;

let q be Sequence-like complex-valued Function;

cluster p + q -> Sequence-like ;

coherence
p + q is Sequence-like

proof end;

cluster p - q -> Sequence-like ;

coherence
p - q is Sequence-like ;

cluster p (#) q -> Sequence-like ;

coherence
p (#) q is Sequence-like

proof end;

cluster p /" q -> Sequence-like ;

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;

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 ;

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;

cluster c + p -> Sequence-like ;

coherence
c + p is Sequence-like

proof end;

cluster p - c -> Sequence-like ;

coherence
p - c is Sequence-like ;

cluster c (#) p -> 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 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 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 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 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 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 Def4 defines Sgm0 AFINSQ_2:def 4 :
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 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 (Sgm0 {n}) . 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{ 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 :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 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 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))) ) & 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 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))) ) & b₁ = 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))) ) & b₂ = f . ((len F) - 1) ) implies b₁ = b₂ ) )

proof end;

consistency
for b₁ 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 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 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))) ) & b₄ = 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 "**" (XFS2FS F)

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

cluster Sum F -> rational ;

coherence
Sum F is rational

proof end;

end;

registration

let F be INT -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 for set ;

coherence
for b₁ being Relation st b₁ is natural-valued holds
b₁ 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 = (Partial_Sums S) . 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 (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 Def10 defines FlattenSeq AFINSQ_2:def 10 :
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: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 ^omega)) = <%> D

proof end;

theorem Th74: :: AFINSQ_2:75

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: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) = (XFS2FS p) | n & XFS2FS (p /^ n) = (XFS2FS p) /^ n )

proof end;

theorem Th5: :: AFINSQ_2:85

for D being set
for d being FinSequence of D holds XFS2FS (FS2XFS d) = d

proof end;

registration

let D be set ;
let f be FinSequence of D;

reduce XFS2FS (FS2XFS f) to f;

reducibility
XFS2FS (FS2XFS f) = f by Th5;

end;

theorem :: AFINSQ_2:86

for D being set
for p being FinSequence of D
for n being Nat holds
( (FS2XFS p) | n = FS2XFS (p | n) & (FS2XFS p) /^ 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

cluster Relation-like Function-like Sequence-like finite Ordinal-yielding for set ;

existence
ex b₁ being Ordinal-Sequence st b₁ is finite

proof end;

end;

registration

let A be finite Ordinal-Sequence;
let n be Nat;

cluster A /^ n -> Ordinal-yielding ;

coherence
A /^ n is Ordinal-yielding

proof end;

end;