:: by Yatsuka Nakamura and Hisashi Ito

::

:: Received June 27, 2008

:: Copyright (c) 2008-2018 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 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 )

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

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;

registration

ex b_{1} being XFinSequence st

( b_{1} is empty & b_{1} is natural-valued )

coherence

- p is Sequence-like

p " is Sequence-like

p ^2 is Sequence-like

abs p is Sequence-like

coherence

p + q is Sequence-like

p - q is Sequence-like ;

coherence

p (#) q is Sequence-like

p /" q is Sequence-like ;

end;

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

existence ex b

( b

proof end;

let p be Sequence-like complex-valued Function;coherence

- p is Sequence-like

proof end;

coherence p " is Sequence-like

proof end;

coherence p ^2 is Sequence-like

proof end;

coherence abs p is Sequence-like

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 ;

registration

let p be complex-valued finite Function;

coherence

- p is finite

p " is finite

p ^2 is finite

abs p is finite

coherence

p + q is finite

p - q is finite ;

coherence

p (#) q is finite

p /" q is finite ;

coherence

q /" p is finite ;

end;
coherence

- p is finite

proof end;

coherence p " is finite

proof end;

coherence p ^2 is finite

proof end;

coherence abs p is finite

proof end;

let q be complex-valued Function;coherence

p + q is finite

proof end;

coherence p - q is finite ;

coherence

p (#) q is finite

proof end;

coherence p /" q is finite ;

coherence

q /" p is finite ;

registration

let p be Sequence-like complex-valued Function;

let c be Complex;

coherence

c + p is Sequence-like

p - c is Sequence-like ;

coherence

c (#) p is Sequence-like

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

registration

let p be complex-valued finite Function;

let c be Complex;

coherence

c + p is finite

p - c is finite ;

coherence

c (#) p is finite

end;
let c be Complex;

coherence

c + p is finite

proof end;

coherence p - c is finite ;

coherence

c (#) p is finite

proof end;

definition

let p be XFinSequence;

ex b_{1} being XFinSequence st

( len b_{1} = len p & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = p . ((len p) - (i + 1)) ) )

for b_{1}, b_{2} being XFinSequence st len b_{1} = len p & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = p . ((len p) - (i + 1)) ) & len b_{2} = len p & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = p . ((len p) - (i + 1)) ) holds

b_{1} = b_{2}

end;
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 ( len it = len p & ( for i being Nat st i in dom it holds

it . i = p . ((len p) - (i + 1)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines Rev AFINSQ_2:def 1 :

for p, b_{2} being XFinSequence holds

( b_{2} = Rev p iff ( len b_{2} = len p & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = p . ((len p) - (i + 1)) ) ) );

for p, b

( b

b

definition

let p be XFinSequence;

let n be Nat;

ex b_{1} being XFinSequence st

( len b_{1} = (len p) -' n & ( for m being Nat st m in dom b_{1} holds

b_{1} . m = p . (m + n) ) )

for b_{1}, b_{2} being XFinSequence st len b_{1} = (len p) -' n & ( for m being Nat st m in dom b_{1} holds

b_{1} . m = p . (m + n) ) & len b_{2} = (len p) -' n & ( for m being Nat st m in dom b_{2} holds

b_{2} . m = p . (m + n) ) holds

b_{1} = b_{2}

end;
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 ( len it = (len p) -' n & ( for m being Nat st m in dom it holds

it . m = p . (m + n) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines /^ AFINSQ_2:def 2 :

for p being XFinSequence

for n being Nat

for b_{3} being XFinSequence holds

( b_{3} = p /^ n iff ( len b_{3} = (len p) -' n & ( for m being Nat st m in dom b_{3} holds

b_{3} . m = p . (m + n) ) ) );

for p being XFinSequence

for n being Nat

for b

( b

b

registration
end;

registration
end;

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

for p being XFinSequence

for k1, k2 being Nat holds mid (p,k1,k2) = (p | k2) /^ (k1 -' 1);

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)

for k1, k2 being Nat st 1 <= k1 & k2 <= len p holds

mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1)

proof end;

registration
end;

definition

let X be finite natural-membered set ;

ex b_{1} being XFinSequence of NAT st

( rng b_{1} = X & ( for l, m, k1, k2 being Nat st l < m & m < len b_{1} & k1 = b_{1} . l & k2 = b_{1} . m holds

k1 < k2 ) )

for b_{1}, b_{2} being XFinSequence of NAT st rng b_{1} = X & ( for l, m, k1, k2 being Nat st l < m & m < len b_{1} & k1 = b_{1} . l & k2 = b_{1} . m holds

k1 < k2 ) & rng b_{2} = X & ( for l, m, k1, k2 being Nat st l < m & m < len b_{2} & k1 = b_{2} . l & k2 = b_{2} . m holds

k1 < k2 ) holds

b_{1} = b_{2}

end;
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 ( 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 ) );

ex b

( rng b

k1 < k2 ) )

proof end;

uniqueness for b

k1 < k2 ) & rng b

k1 < k2 ) holds

b

proof end;

:: deftheorem Def4 defines Sgm0 AFINSQ_2:def 4 :

for X being finite natural-membered set

for b_{2} being XFinSequence of NAT holds

( b_{2} = Sgm0 X iff ( rng b_{2} = X & ( for l, m, k1, k2 being Nat st l < m & m < len b_{2} & k1 = b_{2} . l & k2 = b_{2} . m holds

k1 < k2 ) ) );

for X being finite natural-membered set

for b

( b

k1 < k2 ) ) );

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

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

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

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

( 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 )

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

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

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

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

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

(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

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

(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) )

( X <N< Y iff Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y) )

proof end;

definition

let f be XFinSequence;

let B be set ;

f * (Sgm0 (B /\ (Segm (len f)))) is XFinSequence

end;
let B be set ;

::Following is a subsequence selected from f by B.

coherence f * (Sgm0 (B /\ (Segm (len f)))) is XFinSequence

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

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

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

registration
end;

scheme :: AFINSQ_2:sch 2

Sch5{ F_{1}() -> set , P_{1}[ set ] } :

provided

Sch5{ F

provided

A1:
P_{1}[ <%> F_{1}()]
and

A2: for F being XFinSequence of F_{1}()

for d being Element of F_{1}() st P_{1}[F] holds

P_{1}[F ^ <%d%>]

A2: for F being XFinSequence of F

for d being Element of F

P

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

( ( b is having_a_unity & len F = 0 implies ex b_{1} being Element of D st b_{1} = the_unity_wrt b ) & ( ( not b is having_a_unity or not len F = 0 ) implies ex b_{1} 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_{1} = f . ((len F) - 1) ) ) )

for b_{1}, b_{2} being Element of D holds

( ( b is having_a_unity & len F = 0 & b_{1} = the_unity_wrt b & b_{2} = the_unity_wrt b implies b_{1} = b_{2} ) & ( ( 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_{1} = 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_{2} = f . ((len F) - 1) ) implies b_{1} = b_{2} ) )

for b_{1} being Element of D holds verum
;

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

( ( b is having_a_unity & len F = 0 implies ex b

( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds

f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b

proof end;

uniqueness for b

( ( b is having_a_unity & len F = 0 & b

( 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 . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds

f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b

proof end;

consistency for b

:: 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_{4} being Element of D holds

( ( b is having_a_unity & len F = 0 implies ( b_{4} = b "**" F iff b_{4} = the_unity_wrt b ) ) & ( ( not b is having_a_unity or not len F = 0 ) implies ( b_{4} = 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_{4} = f . ((len F) - 1) ) ) ) );

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

( ( b is having_a_unity & len F = 0 implies ( b

( f . 0 = F . 0 & ( for n being Nat st n + 1 < len F holds

f . (n + 1) = b . ((f . n),(F . (n + 1))) ) & b

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)

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)

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)

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;

::$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))

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

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)

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

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

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

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;

:: deftheorem defines Sum AFINSQ_2:def 9 :

for F being XFinSequence holds Sum F = addcomplex "**" F;

for F being XFinSequence holds Sum F = addcomplex "**" F;

registration
end;

registration
end;

registration

coherence

for b_{1} being Relation st b_{1} is natural-valued holds

b_{1} is nonnegative-yielding

end;
for b

b

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

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

rF1 . i <= rF2 . i ) holds

Sum rF1 <= Sum rF2

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

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

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

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

( 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

for cF being complex-valued XFinSequence

for c being Complex holds c (#) (cF | n) = (c (#) cF) | n

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

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}

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}

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}))

for c being Complex st rng cF c= {0,c} holds

Sum cF = c * (card (cF " {c}))

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)

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

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

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 ;

ex b_{1} 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_{1} = g "**" F )

for b_{1}, b_{2} 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_{1} = 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_{2} = g "**" F ) holds

b_{1} = b_{2}

end;
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 g being BinOp of (D ^omega) st

( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & it = g "**" F );

ex b

( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b

proof end;

uniqueness for b

( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b

( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b

b

proof end;

:: deftheorem Def10 defines FlattenSeq AFINSQ_2:def 10 :

for D being set

for F being XFinSequence of D ^omega

for b_{3} being Element of D ^omega holds

( b_{3} = 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_{3} = g "**" F ) );

for D being set

for F being XFinSequence of D ^omega

for b

( b

( ( for p, q being Element of D ^omega holds g . (p,q) = p ^ q ) & b

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)

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

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

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:82

for D being set

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

FlattenSeq F c= FlattenSeq G

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;

coherence

not p ^ q is empty by AFINSQ_1:30;

coherence

not q ^ p is empty by AFINSQ_1:30;

end;
let q be non empty XFinSequence;

coherence

not p ^ q is empty by AFINSQ_1:30;

coherence

not q ^ p is empty by AFINSQ_1:30;