:: Flexary Operations
:: by Karol P\kak
::
:: Received March 26, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users


Lm1: for D being non empty set
for f being FinSequence of D * st f = {} holds
(D -concatenation) "**" f = {}
proof end;

theorem Th1: :: FLEXARY1:1
for F being Function-yielding Function
for a being object holds
( a in Values F iff ex x, y being object st
( x in dom F & y in dom (F . x) & a = (F . x) . y ) )
proof end;

theorem Th2: :: FLEXARY1:2
for D being set
for f, g being FinSequence of D * holds Values (f ^ g) = (Values f) \/ (Values g)
proof end;

theorem Th3: :: FLEXARY1:3
for D being non empty set
for f, g being FinSequence of D * holds (D -concatenation) "**" (f ^ g) = ((D -concatenation) "**" f) ^ ((D -concatenation) "**" g)
proof end;

theorem :: FLEXARY1:4
for D being non empty set
for f being FinSequence of D * holds rng ((D -concatenation) "**" f) = Values f
proof end;

theorem :: FLEXARY1:5
for D1, D2 being non empty set
for f1 being FinSequence of D1 *
for f2 being FinSequence of D2 * st f1 = f2 holds
(D1 -concatenation) "**" f1 = (D2 -concatenation) "**" f2
proof end;

theorem :: FLEXARY1:6
for D being non empty set
for i being Nat
for f being FinSequence of D * holds
( i in dom ((D -concatenation) "**" f) iff ex n, k being Nat st
( n + 1 in dom f & k in dom (f . (n + 1)) & i = k + (len ((D -concatenation) "**" (f | n))) ) )
proof end;

theorem :: FLEXARY1:7
for D being non empty set
for i being Nat
for f, g being FinSequence of D * st i in dom ((D -concatenation) "**" f) holds
( ((D -concatenation) "**" f) . i = ((D -concatenation) "**" (f ^ g)) . i & ((D -concatenation) "**" f) . i = ((D -concatenation) "**" (g ^ f)) . (i + (len ((D -concatenation) "**" g))) )
proof end;

theorem :: FLEXARY1:8
for D being non empty set
for k, n being Nat
for f being FinSequence of D * st k in dom (f . (n + 1)) holds
(f . (n + 1)) . k = ((D -concatenation) "**" f) . (k + (len ((D -concatenation) "**" (f | n))))
proof end;

definition
let k, n be Nat;
let f, g be complex-valued Function;
func (f,k) +...+ (g,n) -> complex number means :Def1: :: FLEXARY1:def 1
 for h being complex-valued FinSequence st h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) holds
it = Sum (h | ((n -' k) + 1)) if ( f = g & k <= n )
otherwise it = 0 ;
existence
( ( f = g & k <= n implies ex b1 being complex number st
for h being complex-valued FinSequence st h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) holds
b1 = Sum (h | ((n -' k) + 1)) ) & ( ( not f = g or not k <= n ) implies ex b1 being complex number st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being complex number holds
( ( f = g & k <= n & ( for h being complex-valued FinSequence st h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) holds
b1 = Sum (h | ((n -' k) + 1)) ) & ( for h being complex-valued FinSequence st h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) holds
b2 = Sum (h | ((n -' k) + 1)) ) implies b1 = b2 ) & ( ( not f = g or not k <= n ) & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being complex number holds verum;
;
end;

:: deftheorem Def1 defines +...+ FLEXARY1:def 1 :
for k, n being Nat
for f, g being complex-valued Function
for b5 being complex number holds
( ( f = g & k <= n implies ( b5 = (f,k) +...+ (g,n) iff for h being complex-valued FinSequence st h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) holds
b5 = Sum (h | ((n -' k) + 1)) ) ) & ( ( not f = g or not k <= n ) implies ( b5 = (f,k) +...+ (g,n) iff b5 = 0 ) ) );

theorem Th9: :: FLEXARY1:9
for k, n being Nat
for f being complex-valued Function st k <= n holds
ex h being complex-valued FinSequence st
( (f,k) +...+ (f,n) = Sum h & len h = (n -' k) + 1 & h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) )
proof end;

theorem Th10: :: FLEXARY1:10
for k, n being Nat
for f being complex-valued Function st (f,k) +...+ (f,n) <> 0 holds
ex i being Nat st
( k <= i & i <= n & i in dom f )
proof end;

theorem Th11: :: FLEXARY1:11
for k being Nat
for f being complex-valued Function holds (f,k) +...+ (f,k) = f . k
proof end;

theorem Th12: :: FLEXARY1:12
for k, n being Nat
for f being complex-valued Function st k <= n + 1 holds
(f,k) +...+ (f,(n + 1)) = ((f,k) +...+ (f,n)) + (f . (n + 1))
proof end;

theorem Th13: :: FLEXARY1:13
for k, n being Nat
for f being complex-valued Function st k <= n holds
(f,k) +...+ (f,n) = (f . k) + ((f,(k + 1)) +...+ (f,n))
proof end;

theorem Th14: :: FLEXARY1:14
for k, m, n being Nat
for f being complex-valued Function st k <= m & m <= n holds
((f,k) +...+ (f,m)) + ((f,(m + 1)) +...+ (f,n)) = (f,k) +...+ (f,n)
proof end;

theorem Th15: :: FLEXARY1:15
for k, n being Nat
for h being complex-valued FinSequence st k > len h holds
(h,k) +...+ (h,n) = 0
proof end;

theorem Th16: :: FLEXARY1:16
for k, n being Nat
for h being complex-valued FinSequence st n >= len h holds
(h,k) +...+ (h,n) = (h,k) +...+ (h,(len h))
proof end;

theorem Th17: :: FLEXARY1:17
for k being Nat
for h being complex-valued FinSequence holds (h,0) +...+ (h,k) = (h,1) +...+ (h,k)
proof end;

theorem Th18: :: FLEXARY1:18
for h being complex-valued FinSequence holds (h,1) +...+ (h,(len h)) = Sum h
proof end;

Lm2: for k, n being Nat
for g, h being complex-valued FinSequence st k <= n & n <= len g holds
((g ^ h),k) +...+ ((g ^ h),n) = (g,k) +...+ (g,n)
proof end;

Lm3: for k, n being Nat
for g, h being complex-valued FinSequence st k <= n & k > len g holds
((g ^ h),k) +...+ ((g ^ h),n) = (h,(k -' (len g))) +...+ (h,(n -' (len g)))
proof end;

theorem :: FLEXARY1:19
for k, n being Nat
for g, h being complex-valued FinSequence holds ((g ^ h),k) +...+ ((g ^ h),n) = ((g,k) +...+ (g,n)) + ((h,(k -' (len g))) +...+ (h,(n -' (len g))))
proof end;

registration
let n, k be Nat;
let f be real-valued FinSequence;
cluster (f,k) +...+ (f,n) -> complex real ;
coherence
(f,k) +...+ (f,n) is real
proof end;
end;

registration
let n, k be Nat;
let f be natural-valued FinSequence;
cluster (f,k) +...+ (f,n) -> natural complex ;
coherence
(f,k) +...+ (f,n) is natural
proof end;
end;

definition
let n be Nat;
let f be complex-valued Function;
assume A1: (dom f) /\ NAT is finite ;
func (f,n) +... -> complex number means :Def2: :: FLEXARY1:def 2
 for k being Nat st ( for i being Nat st i in dom f holds
i <= k ) holds
it = (f,n) +...+ (f,k);
existence
ex b1 being complex number st
for k being Nat st ( for i being Nat st i in dom f holds
i <= k ) holds
b1 = (f,n) +...+ (f,k)
proof end;
uniqueness
for b1, b2 being complex number st ( for k being Nat st ( for i being Nat st i in dom f holds
i <= k ) holds
b1 = (f,n) +...+ (f,k) ) & ( for k being Nat st ( for i being Nat st i in dom f holds
i <= k ) holds
b2 = (f,n) +...+ (f,k) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines +... FLEXARY1:def 2 :
for n being Nat
for f being complex-valued Function st (dom f) /\ NAT is finite holds
for b3 being complex number holds
( b3 = (f,n) +... iff for k being Nat st ( for i being Nat st i in dom f holds
i <= k ) holds
b3 = (f,n) +...+ (f,k) );

definition
let n be Nat;
let h be complex-valued FinSequence;
:: original: +...
redefine func (h,n) +... -> complex number equals :: FLEXARY1:def 3
(h,n) +...+ (h,(len h));
coherence
(h,n) +... is complex number ;
compatibility
for b1 being complex number holds
( b1 = (h,n) +... iff b1 = (h,n) +...+ (h,(len h)) )
proof end;
end;

:: deftheorem defines +... FLEXARY1:def 3 :
for n being Nat
for h being complex-valued FinSequence holds (h,n) +... = (h,n) +...+ (h,(len h));

registration
let n be Nat;
let h be natural-valued FinSequence;
cluster (h,n) +... -> natural complex ;
coherence
(h,n) +... is natural ;
end;

theorem Th20: :: FLEXARY1:20
for n being Nat
for f being finite complex-valued Function holds (f . n) + ((f,(n + 1)) +...) = (f,n) +...
proof end;

theorem Th21: :: FLEXARY1:21
for h being complex-valued FinSequence holds Sum h = (h,1) +... by Th18;

theorem Th22: :: FLEXARY1:22
for h being complex-valued FinSequence holds Sum h = (h . 1) + ((h,2) +...)
proof end;

scheme :: FLEXARY1:sch 1
TT{ F1() -> complex-valued FinSequence, F2() -> complex-valued FinSequence, F3() -> Nat, F4() -> Nat, F5() -> non zero Nat, F6() -> non zero Nat } :
(F1(),F3()) +... = (F2(),F4()) +...
provided
A1: for j being Nat holds (F1(),(F3() + (j * F5()))) +...+ (F1(),((F3() + (j * F5())) + (F5() -' 1))) = (F2(),(F4() + (j * F6()))) +...+ (F2(),((F4() + (j * F6())) + (F6() -' 1)))
proof end;

definition
let r be Real;
let f be real-valued Function;
func r |^ f -> real-valued Function means :Def4: :: FLEXARY1:def 4
( dom it = dom f & ( for x being object st x in dom f holds
it . x = r to_power (f . x) ) );
existence
ex b1 being real-valued Function st
( dom b1 = dom f & ( for x being object st x in dom f holds
b1 . x = r to_power (f . x) ) )
proof end;
uniqueness
for b1, b2 being real-valued Function st dom b1 = dom f & ( for x being object st x in dom f holds
b1 . x = r to_power (f . x) ) & dom b2 = dom f & ( for x being object st x in dom f holds
b2 . x = r to_power (f . x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines |^ FLEXARY1:def 4 :
for r being Real
for f, b3 being real-valued Function holds
( b3 = r |^ f iff ( dom b3 = dom f & ( for x being object st x in dom f holds
b3 . x = r to_power (f . x) ) ) );

registration
let n be Nat;
let f be natural-valued Function;
cluster n |^ f -> real-valued natural-valued ;
coherence
n |^ f is natural-valued
proof end;
end;

registration
let r be Real;
let f be real-valued FinSequence;
cluster r |^ f -> FinSequence-like real-valued ;
coherence
r |^ f is FinSequence-like
proof end;
cluster r |^ f -> len f -element real-valued ;
coherence
r |^ f is len f -element
proof end;
end;

registration
let n be Nat;
let f be one-to-one natural-valued Function;
cluster (2 + n) |^ f -> one-to-one real-valued ;
coherence
(2 + n) |^ f is one-to-one
proof end;
end;

theorem Th23: :: FLEXARY1:23
for r, s being Real holds r |^ <*s*> = <*(r to_power s)*>
proof end;

theorem Th24: :: FLEXARY1:24
for r being Real
for f, g being real-valued FinSequence holds r |^ (f ^ g) = (r |^ f) ^ (r |^ g)
proof end;

theorem :: FLEXARY1:25
for f being real-valued Function
for g being Function holds (2 |^ f) * g = 2 |^ (f * g)
proof end;

Lm4: for n being Nat
for f, g being natural-valued FinSequence st f is increasing & f | n = g holds
g is increasing
proof end;

Lm5: for i, n being Nat
for f1, f2 being natural-valued FinSequence st len f1 = i + 1 & f1 | i = f2 holds
Sum (n |^ f1) = (Sum (n |^ f2)) + (n |^ (f1 . (i + 1)))
proof end;

theorem Th26: :: FLEXARY1:26
for n being Nat
for f being natural-valued increasing FinSequence st n > 1 holds
((n |^ f) . 1) + (((n |^ f),2) +...) < 2 * (n |^ (f . (len f)))
proof end;

Lm6: for n being Nat
for f1, f2 being natural-valued increasing FinSequence st n > 1 & Sum (n |^ f1) > 0 & Sum (n |^ f1) = Sum (n |^ f2) holds
f1 . (len f1) <= f2 . (len f2)
proof end;

theorem Th27: :: FLEXARY1:27
for n being Nat
for f1, f2 being natural-valued increasing FinSequence st n > 1 & ((n |^ f1) . 1) + (((n |^ f1),2) +...) = ((n |^ f2) . 1) + (((n |^ f2),2) +...) holds
f1 = f2
proof end;

theorem Th28: :: FLEXARY1:28
for k, n being Nat
for f being natural-valued Function st n > 1 holds
Coim ((n |^ f),(n |^ k)) = Coim (f,k)
proof end;

theorem Th29: :: FLEXARY1:29
for n being Nat
for f1, f2 being natural-valued Function st n > 1 holds
( f1,f2 are_fiberwise_equipotent iff n |^ f1,n |^ f2 are_fiberwise_equipotent )
proof end;

theorem :: FLEXARY1:30
for n being Nat
for f1, f2 being one-to-one natural-valued FinSequence st n > 1 & ((n |^ f1) . 1) + (((n |^ f1),2) +...) = ((n |^ f2) . 1) + (((n |^ f2),2) +...) holds
rng f1 = rng f2
proof end;

theorem :: FLEXARY1:31
for n being Nat ex f being natural-valued increasing FinSequence st n = ((2 |^ f) . 1) + (((2 |^ f),2) +...)
proof end;

definition
let o be Function-yielding Function;
let x, y be object ;
func o _ (x,y) -> set equals :: FLEXARY1:def 5
(o . x) . y;
coherence
(o . x) . y is set ;
end;

:: deftheorem defines _ FLEXARY1:def 5 :
for o being Function-yielding Function
for x, y being object holds o _ (x,y) = (o . x) . y;

definition
let F be Function-yielding Function;
attr F is double-one-to-one means :Def6: :: FLEXARY1:def 6
 for x1, x2, y1, y2 being object st x1 in dom F & y1 in dom (F . x1) & x2 in dom F & y2 in dom (F . x2) & F _ (x1,y1) = F _ (x2,y2) holds
( x1 = x2 & y1 = y2 );
end;

:: deftheorem Def6 defines double-one-to-one FLEXARY1:def 6 :
for F being Function-yielding Function holds
( F is double-one-to-one iff for x1, x2, y1, y2 being object st x1 in dom F & y1 in dom (F . x1) & x2 in dom F & y2 in dom (F . x2) & F _ (x1,y1) = F _ (x2,y2) holds
( x1 = x2 & y1 = y2 ) );

registration
let D be set ;
cluster empty -> double-one-to-one for FinSequence of D * ;
coherence
for b1 being FinSequence of D * st b1 is empty holds
b1 is double-one-to-one ;
end;

registration
cluster Relation-like Function-like Function-yielding V68() double-one-to-one for set ;
existence
ex b1 being Function-yielding Function st b1 is double-one-to-one
proof end;
let D be set ;
cluster Relation-like omega -defined D * -valued Function-like finite Function-yielding V68() FinSequence-like FinSubsequence-like FinSequence-yielding finite-support double-one-to-one for FinSequence of D * ;
existence
ex b1 being FinSequence of D * st b1 is double-one-to-one
proof end;
end;

registration
let F be Function-yielding double-one-to-one Function;
let x be object ;
cluster F . x -> one-to-one ;
coherence
F . x is one-to-one
proof end;
end;

registration
let F be one-to-one Function;
cluster <*F*> -> double-one-to-one ;
coherence
<*F*> is double-one-to-one
proof end;
end;

theorem :: FLEXARY1:32
for f being Function-yielding Function holds
( f is double-one-to-one iff ( ( for x being object holds f . x is one-to-one ) & ( for x, y being object st x <> y holds
rng (f . x) misses rng (f . y) ) ) )
proof end;

theorem Th33: :: FLEXARY1:33
for D being set
for f1, f2 being double-one-to-one FinSequence of D * st Values f1 misses Values f2 holds
f1 ^ f2 is double-one-to-one
proof end;

definition
let D be finite set ;
mode DoubleReorganization of D -> double-one-to-one FinSequence of D * means :Def7: :: FLEXARY1:def 7
 Values it = D;
existence
ex b1 being double-one-to-one FinSequence of D * st Values b1 = D
proof end;
end;

:: deftheorem Def7 defines DoubleReorganization FLEXARY1:def 7 :
for D being finite set
for b2 being double-one-to-one FinSequence of D * holds
( b2 is DoubleReorganization of D iff Values b2 = D );

theorem Th34: :: FLEXARY1:34
( {} is DoubleReorganization of {} & <*{}*> is DoubleReorganization of {} )
proof end;

theorem Th35: :: FLEXARY1:35
for D being finite set
for F being one-to-one onto FinSequence of D holds <*F*> is DoubleReorganization of D
proof end;

theorem Th36: :: FLEXARY1:36
for D1, D2 being finite set st D1 misses D2 holds
for o1 being DoubleReorganization of D1
for o2 being DoubleReorganization of D2 holds o1 ^ o2 is DoubleReorganization of D1 \/ D2
proof end;

theorem Th37: :: FLEXARY1:37
for i being Nat
for D being finite set
for o being DoubleReorganization of D
for F being one-to-one FinSequence st i in dom o & (rng F) /\ D c= rng (o . i) holds
o +* (i,F) is DoubleReorganization of (rng F) \/ (D \ (rng (o . i)))
proof end;

registration
let D be finite set ;
let n be non zero Nat;
cluster Relation-like omega -defined D * -valued Function-like finite n -element Function-yielding V68() FinSequence-like FinSubsequence-like FinSequence-yielding finite-support double-one-to-one for DoubleReorganization of D;
existence
ex b1 being DoubleReorganization of D st b1 is n -element
proof end;
end;

registration
let D be natural-membered finite set ;
let o be DoubleReorganization of D;
let x be object ;
cluster o . x -> natural-valued ;
coherence
o . x is natural-valued
proof end;
end;

theorem Th38: :: FLEXARY1:38
for F being non empty FinSequence
for G being finite Function st rng G c= rng F holds
ex o being len b1 -element DoubleReorganization of dom G st
for n being Nat holds F . n = G . (o _ (n,1)) & ... & F . n = G . (o _ (n,(len (o . n))))
proof end;

theorem :: FLEXARY1:39
for F being non empty FinSequence
for G being FinSequence st rng G c= rng F holds
ex o being len b1 -element DoubleReorganization of dom G st
for n being Nat holds
( o . n is increasing & F . n = G . (o _ (n,1)) & ... & F . n = G . (o _ (n,(len (o . n)))) )
proof end;

registration
let f be finite Function;
let o be DoubleReorganization of dom f;
let x be object ;
cluster (o . x) * f -> FinSequence-like ;
coherence
f * (o . x) is FinSequence-like
proof end;
end;

registration
cluster Relation-like omega -defined Function-like finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support complex-functions-valued for set ;
existence
ex b1 being FinSequence st
( b1 is complex-functions-valued & b1 is FinSequence-yielding )
proof end;
end;

notation
let f be Function-yielding Function;
let g be Function;
synonym g *. f for ^^^g,f__;
end;

registration
let f be Function-yielding Function;
let g be Function;
cluster g *. f -> Function-yielding ;
coherence
g *. f is Function-yielding
proof end;
end;

registration
let g be Function;
let f be (dom g) * -valued FinSequence;
cluster g *. f -> FinSequence-yielding ;
coherence
g *. f is FinSequence-yielding
proof end;
let x be object ;
cluster (g *. f) . x -> len (f . x) -element ;
coherence
(g *. f) . x is len (f . x) -element
proof end;
end;

registration
let f be Function-yielding FinSequence;
let g be Function;
cluster g *. f -> FinSequence-like ;
coherence
g *. f is FinSequence-like
proof end;
cluster g *. f -> len f -element ;
coherence
g *. f is len f -element
proof end;
end;

registration
let f be Function-yielding Function;
let g be complex-valued Function;
cluster g *. f -> complex-functions-valued ;
coherence
g *. f is complex-functions-valued
proof end;
end;

registration
let f be Function-yielding Function;
let g be natural-valued Function;
cluster g *. f -> natural-functions-valued ;
coherence
g *. f is natural-functions-valued
proof end;
end;

theorem :: FLEXARY1:40
for f being Function-yielding Function
for g being Function holds Values (g *. f) = g .: (Values f)
proof end;

theorem Th41: :: FLEXARY1:41
for x being object
for f being Function-yielding Function
for g being Function holds (g *. f) . x = g * (f . x)
proof end;

theorem Th42: :: FLEXARY1:42
for f being Function-yielding Function
for g being FinSequence
for x, y being object holds (g *. f) _ (x,y) = g . (f _ (x,y))
proof end;

definition
let f be FinSequence-yielding complex-functions-valued Function;
func Sum f -> complex-valued Function means :Def8: :: FLEXARY1:def 8
( dom it = dom f & ( for x being set holds it . x = Sum (f . x) ) );
existence
ex b1 being complex-valued Function st
( dom b1 = dom f & ( for x being set holds b1 . x = Sum (f . x) ) )
proof end;
uniqueness
for b1, b2 being complex-valued Function st dom b1 = dom f & ( for x being set holds b1 . x = Sum (f . x) ) & dom b2 = dom f & ( for x being set holds b2 . x = Sum (f . x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines Sum FLEXARY1:def 8 :
for f being FinSequence-yielding complex-functions-valued Function
for b2 being complex-valued Function holds
( b2 = Sum f iff ( dom b2 = dom f & ( for x being set holds b2 . x = Sum (f . x) ) ) );

registration
let f be FinSequence-yielding complex-functions-valued FinSequence;
cluster Sum f -> FinSequence-like complex-valued ;
coherence
Sum f is FinSequence-like
proof end;
cluster Sum f -> len f -element complex-valued ;
coherence
Sum f is len f -element
proof end;
end;

registration
let f be FinSequence-yielding natural-functions-valued Function;
cluster Sum f -> complex-valued natural-valued ;
coherence
Sum f is natural-valued
proof end;
end;

registration
let f, g be complex-functions-valued FinSequence;
cluster f ^ g -> complex-functions-valued ;
coherence
f ^ g is complex-functions-valued
proof end;
end;

registration
let f, g be ext-real-valued FinSequence;
cluster f ^ g -> ext-real-valued ;
coherence
f ^ g is ext-real-valued
proof end;
end;

registration
let f be complex-functions-valued Function;
let X be set ;
cluster f | X -> complex-functions-valued ;
coherence
f | X is complex-functions-valued
proof end;
end;

registration
let f be FinSequence-yielding Function;
let X be set ;
cluster f | X -> FinSequence-yielding ;
coherence
f | X is FinSequence-yielding
proof end;
end;

registration
let F be complex-valued Function;
cluster <*F*> -> complex-functions-valued ;
coherence
<*F*> is complex-functions-valued
proof end;
end;

theorem Th43: :: FLEXARY1:43
for f, g being FinSequence st f ^ g is FinSequence-yielding holds
( f is FinSequence-yielding & g is FinSequence-yielding )
proof end;

theorem Th44: :: FLEXARY1:44
for f, g being FinSequence st f ^ g is complex-functions-valued holds
( f is complex-functions-valued & g is complex-functions-valued )
proof end;

theorem Th45: :: FLEXARY1:45
for f being complex-valued FinSequence holds Sum <*f*> = <*(Sum f)*>
proof end;

theorem Th46: :: FLEXARY1:46
for f, g being FinSequence-yielding complex-functions-valued FinSequence holds Sum (f ^ g) = (Sum f) ^ (Sum g)
proof end;

theorem :: FLEXARY1:47
for f being complex-valued FinSequence
for o being DoubleReorganization of dom f holds Sum f = Sum (Sum (f *. o))
proof end;

registration
cluster NAT * -> natural-functions-membered ;
coherence
NAT * is natural-functions-membered
proof end;
cluster COMPLEX * -> complex-functions-membered ;
coherence
COMPLEX * is complex-functions-membered
proof end;
end;

theorem :: FLEXARY1:48
for f being FinSequence of COMPLEX * holds Sum ((COMPLEX -concatenation) "**" f) = Sum (Sum f)
proof end;

definition
let f be finite Function;
mode valued_reorganization of f -> DoubleReorganization of dom f means :Def9: :: FLEXARY1:def 9
( ( for n being Nat ex x being object st x = f . (it _ (n,1)) & ... & x = f . (it _ (n,(len (it . n)))) ) & ( for n1, n2, i1, i2 being Nat st i1 in dom (it . n1) & i2 in dom (it . n2) & f . (it _ (n1,i1)) = f . (it _ (n2,i2)) holds
n1 = n2 ) );
existence
ex b1 being DoubleReorganization of dom f st
( ( for n being Nat ex x being object st x = f . (b1 _ (n,1)) & ... & x = f . (b1 _ (n,(len (b1 . n)))) ) & ( for n1, n2, i1, i2 being Nat st i1 in dom (b1 . n1) & i2 in dom (b1 . n2) & f . (b1 _ (n1,i1)) = f . (b1 _ (n2,i2)) holds
n1 = n2 ) )
proof end;
end;

:: deftheorem Def9 defines valued_reorganization FLEXARY1:def 9 :
for f being finite Function
for b2 being DoubleReorganization of dom f holds
( b2 is valued_reorganization of f iff ( ( for n being Nat ex x being object st x = f . (b2 _ (n,1)) & ... & x = f . (b2 _ (n,(len (b2 . n)))) ) & ( for n1, n2, i1, i2 being Nat st i1 in dom (b2 . n1) & i2 in dom (b2 . n2) & f . (b2 _ (n1,i1)) = f . (b2 _ (n2,i2)) holds
n1 = n2 ) ) );

theorem :: FLEXARY1:49
for n being Nat
for f being finite Function
for o being valued_reorganization of f holds
( rng ((f *. o) . n) = {} or ( rng ((f *. o) . n) = {(f . (o _ (n,1)))} & 1 in dom (o . n) ) )
proof end;

Lm7: for i being Nat
for f being FinSequence
for o1, o2 being valued_reorganization of f st rng ((f *. o1) . i) = rng ((f *. o2) . i) holds
rng (o1 . i) c= rng (o2 . i)
proof end;

theorem :: FLEXARY1:50
for i being Nat
for f being FinSequence
for o1, o2 being valued_reorganization of f st rng ((f *. o1) . i) = rng ((f *. o2) . i) holds
rng (o1 . i) = rng (o2 . i) by Lm7;

theorem :: FLEXARY1:51
for i being Nat
for f being FinSequence
for g being complex-valued FinSequence
for o1, o2 being DoubleReorganization of dom g st o1 is valued_reorganization of f & o2 is valued_reorganization of f & rng ((f *. o1) . i) = rng ((f *. o2) . i) holds
(Sum (g *. o1)) . i = (Sum (g *. o2)) . i
proof end;