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

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

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

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

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

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

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

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;

( ( f = g & k <= n implies ex b_{1} 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

b_{1} = Sum (h | ((n -' k) + 1)) ) & ( ( not f = g or not k <= n ) implies ex b_{1} being complex number st b_{1} = 0 ) )

for b_{1}, b_{2} 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

b_{1} = 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

b_{2} = Sum (h | ((n -' k) + 1)) ) implies b_{1} = b_{2} ) & ( ( not f = g or not k <= n ) & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

consistency

for b_{1} being complex number holds verum;

;

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

( ( f = g & k <= n implies ex b

for h being complex-valued FinSequence st h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) holds

b

proof end;

uniqueness for b

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

b

b

proof end;

correctness consistency

for b

;

:: deftheorem Def1 defines +...+ FLEXARY1:def 1 :

for k, n being Nat

for f, g being complex-valued Function

for b_{5} being complex number holds

( ( f = g & k <= n implies ( b_{5} = (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

b_{5} = Sum (h | ((n -' k) + 1)) ) ) & ( ( not f = g or not k <= n ) implies ( b_{5} = (f,k) +...+ (g,n) iff b_{5} = 0 ) ) );

for k, n being Nat

for f, g being complex-valued Function

for b

( ( f = g & k <= n implies ( b

b

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

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 )

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

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

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)

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

for h being complex-valued FinSequence st n >= len h holds

(h,k) +...+ (h,n) = (h,k) +...+ (h,(len 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))))

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

registration

let n, k be Nat;

let f be natural-valued FinSequence;

coherence

(f,k) +...+ (f,n) is natural

end;
let f be natural-valued FinSequence;

coherence

(f,k) +...+ (f,n) is natural

proof end;

definition

let n be Nat;

let f be complex-valued Function;

assume A1: (dom f) /\ NAT is finite ;

ex b_{1} being complex number st

for k being Nat st ( for i being Nat st i in dom f holds

i <= k ) holds

b_{1} = (f,n) +...+ (f,k)

for b_{1}, b_{2} being complex number st ( for k being Nat st ( for i being Nat st i in dom f holds

i <= k ) holds

b_{1} = (f,n) +...+ (f,k) ) & ( for k being Nat st ( for i being Nat st i in dom f holds

i <= k ) holds

b_{2} = (f,n) +...+ (f,k) ) holds

b_{1} = b_{2}

end;
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 for k being Nat st ( for i being Nat st i in dom f holds

i <= k ) holds

it = (f,n) +...+ (f,k);

ex b

for k being Nat st ( for i being Nat st i in dom f holds

i <= k ) holds

b

proof end;

uniqueness for b

i <= k ) holds

b

i <= k ) holds

b

b

proof 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 b_{3} being complex number holds

( b_{3} = (f,n) +... iff for k being Nat st ( for i being Nat st i in dom f holds

i <= k ) holds

b_{3} = (f,n) +...+ (f,k) );

for n being Nat

for f being complex-valued Function st (dom f) /\ NAT is finite holds

for b

( b

i <= k ) holds

b

definition

let n be Nat;

let h be complex-valued FinSequence;

(h,n) +... is complex number ;

compatibility

for b_{1} being complex number holds

( b_{1} = (h,n) +... iff b_{1} = (h,n) +...+ (h,(len h)) )

end;
let h be complex-valued FinSequence;

:: original: +...

redefine func (h,n) +... -> complex number equals :: FLEXARY1:def 3

(h,n) +...+ (h,(len h));

coherence redefine func (h,n) +... -> complex number equals :: FLEXARY1:def 3

(h,n) +...+ (h,(len h));

(h,n) +... is complex number ;

compatibility

for b

( b

proof end;

:: deftheorem defines +... FLEXARY1:def 3 :

for n being Nat

for h being complex-valued FinSequence holds (h,n) +... = (h,n) +...+ (h,(len h));

for n being Nat

for h being complex-valued FinSequence holds (h,n) +... = (h,n) +...+ (h,(len h));

registration
end;

theorem Th20: :: FLEXARY1:20

for n being Nat

for f being finite complex-valued Function holds (f . n) + ((f,(n + 1)) +...) = (f,n) +...

for f being finite complex-valued Function holds (f . n) + ((f,(n + 1)) +...) = (f,n) +...

proof end;

scheme :: FLEXARY1:sch 1

TT{ F_{1}() -> complex-valued FinSequence, F_{2}() -> complex-valued FinSequence, F_{3}() -> Nat, F_{4}() -> Nat, F_{5}() -> non zero Nat, F_{6}() -> non zero Nat } :

provided

TT{ F

provided

A1:
for j being Nat holds (F_{1}(),(F_{3}() + (j * F_{5}()))) +...+ (F_{1}(),((F_{3}() + (j * F_{5}())) + (F_{5}() -' 1))) = (F_{2}(),(F_{4}() + (j * F_{6}()))) +...+ (F_{2}(),((F_{4}() + (j * F_{6}())) + (F_{6}() -' 1)))

proof end;

definition

let r be Real;

let f be real-valued Function;

ex b_{1} being real-valued Function st

( dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = r to_power (f . x) ) )

for b_{1}, b_{2} being real-valued Function st dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = r to_power (f . x) ) & dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = r to_power (f . x) ) holds

b_{1} = b_{2}

end;
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 ( dom it = dom f & ( for x being object st x in dom f holds

it . x = r to_power (f . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines |^ FLEXARY1:def 4 :

for r being Real

for f, b_{3} being real-valued Function holds

( b_{3} = r |^ f iff ( dom b_{3} = dom f & ( for x being object st x in dom f holds

b_{3} . x = r to_power (f . x) ) ) );

for r being Real

for f, b

( b

b

registration
end;

registration

let r be Real;

let f be real-valued FinSequence;

coherence

r |^ f is FinSequence-like

r |^ f is len f -element

end;
let f be real-valued FinSequence;

coherence

r |^ f is FinSequence-like

proof end;

coherence r |^ f is len f -element

proof end;

registration

let n be Nat;

let f be one-to-one natural-valued Function;

coherence

(2 + n) |^ f is one-to-one

end;
let f be one-to-one natural-valued Function;

coherence

(2 + n) |^ f is one-to-one

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

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

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)

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 )

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

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

:: deftheorem defines _ FLEXARY1:def 5 :

for o being Function-yielding Function

for x, y being object holds o _ (x,y) = (o . x) . y;

for o being Function-yielding Function

for x, y being object holds o _ (x,y) = (o . x) . y;

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

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 ;

coherence

for b_{1} being FinSequence of D * st b_{1} is empty holds

b_{1} is double-one-to-one
;

end;
coherence

for b

b

registration

existence

ex b_{1} being Function-yielding Function st b_{1} is double-one-to-one

ex b_{1} being FinSequence of D * st b_{1} is double-one-to-one

end;
ex b

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 b

proof end;

registration

let F be Function-yielding double-one-to-one Function;

let x be object ;

coherence

F . x is one-to-one

end;
let x be object ;

coherence

F . x is one-to-one

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

( 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

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 ;

ex b_{1} being double-one-to-one FinSequence of D * st Values b_{1} = D

end;
mode DoubleReorganization of D -> double-one-to-one FinSequence of D * means :Def7: :: FLEXARY1:def 7

Values it = D;

existence Values it = D;

ex b

proof end;

:: deftheorem Def7 defines DoubleReorganization FLEXARY1:def 7 :

for D being finite set

for b_{2} being double-one-to-one FinSequence of D * holds

( b_{2} is DoubleReorganization of D iff Values b_{2} = D );

for D being finite set

for b

( b

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

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

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

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;

ex b_{1} being DoubleReorganization of D st b_{1} is n -element

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

proof end;

registration

let D be natural-membered finite set ;

let o be DoubleReorganization of D;

let x be object ;

coherence

o . x is natural-valued

end;
let o be DoubleReorganization of D;

let x be object ;

coherence

o . x is natural-valued

proof 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 b_{1} -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))))

for G being finite Function st rng G c= rng F holds

ex o being len b

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 b_{1} -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)))) )

for G being FinSequence st rng G c= rng F holds

ex o being len b

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 ;

coherence

f * (o . x) is FinSequence-like

end;
let o be DoubleReorganization of dom f;

let x be object ;

coherence

f * (o . x) is FinSequence-like

proof end;

registration

ex b_{1} being FinSequence st

( b_{1} is complex-functions-valued & b_{1} is FinSequence-yielding )
end;

cluster Relation-like omega -defined Function-like finite FinSequence-like FinSubsequence-like FinSequence-yielding finite-support complex-functions-valued for set ;

existence ex b

( b

proof end;

registration

let f be Function-yielding Function;

let g be Function;

coherence

g *. f is Function-yielding

end;
let g be Function;

coherence

g *. f is Function-yielding

proof end;

registration

let g be Function;

let f be (dom g) * -valued FinSequence;

coherence

g *. f is FinSequence-yielding

coherence

(g *. f) . x is len (f . x) -element

end;
let f be (dom g) * -valued FinSequence;

coherence

g *. f is FinSequence-yielding

proof end;

let x be object ;coherence

(g *. f) . x is len (f . x) -element

proof end;

registration

let f be Function-yielding FinSequence;

let g be Function;

coherence

g *. f is FinSequence-like

g *. f is len f -element

end;
let g be Function;

coherence

g *. f is FinSequence-like

proof end;

coherence g *. f is len f -element

proof end;

registration

let f be Function-yielding Function;

let g be complex-valued Function;

coherence

g *. f is complex-functions-valued

end;
let g be complex-valued Function;

coherence

g *. f is complex-functions-valued

proof end;

registration

let f be Function-yielding Function;

let g be natural-valued Function;

coherence

g *. f is natural-functions-valued

end;
let g be natural-valued Function;

coherence

g *. f is natural-functions-valued

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)

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

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;

ex b_{1} being complex-valued Function st

( dom b_{1} = dom f & ( for x being set holds b_{1} . x = Sum (f . x) ) )

for b_{1}, b_{2} being complex-valued Function st dom b_{1} = dom f & ( for x being set holds b_{1} . x = Sum (f . x) ) & dom b_{2} = dom f & ( for x being set holds b_{2} . x = Sum (f . x) ) holds

b_{1} = b_{2}

end;
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 ( dom it = dom f & ( for x being set holds it . x = Sum (f . x) ) );

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines Sum FLEXARY1:def 8 :

for f being FinSequence-yielding complex-functions-valued Function

for b_{2} being complex-valued Function holds

( b_{2} = Sum f iff ( dom b_{2} = dom f & ( for x being set holds b_{2} . x = Sum (f . x) ) ) );

for f being FinSequence-yielding complex-functions-valued Function

for b

( b

registration

let f be FinSequence-yielding complex-functions-valued FinSequence;

coherence

Sum f is FinSequence-like

Sum f is len f -element

end;
coherence

Sum f is FinSequence-like

proof end;

coherence Sum f is len f -element

proof end;

registration

let f be FinSequence-yielding natural-functions-valued Function;

coherence

Sum f is natural-valued

end;
coherence

Sum f is natural-valued

proof end;

registration

let f, g be complex-functions-valued FinSequence;

coherence

f ^ g is complex-functions-valued

end;
coherence

f ^ g is complex-functions-valued

proof end;

registration
end;

registration

let f be complex-functions-valued Function;

let X be set ;

coherence

f | X is complex-functions-valued

end;
let X be set ;

coherence

f | X is complex-functions-valued

proof end;

registration

let f be FinSequence-yielding Function;

let X be set ;

coherence

f | X is FinSequence-yielding

end;
let X be set ;

coherence

f | X is FinSequence-yielding

proof end;

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

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

( f is complex-functions-valued & g is complex-functions-valued )

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

for o being DoubleReorganization of dom f holds Sum f = Sum (Sum (f *. o))

proof end;

registration

coherence

NAT * is natural-functions-membered

COMPLEX * is complex-functions-membered

end;
NAT * is natural-functions-membered

proof end;

coherence COMPLEX * is complex-functions-membered

proof end;

definition

let f be finite Function;

ex b_{1} being DoubleReorganization of dom f st

( ( for n being Nat ex x being object st x = f . (b_{1} _ (n,1)) & ... & x = f . (b_{1} _ (n,(len (b_{1} . n)))) ) & ( for n1, n2, i1, i2 being Nat st i1 in dom (b_{1} . n1) & i2 in dom (b_{1} . n2) & f . (b_{1} _ (n1,i1)) = f . (b_{1} _ (n2,i2)) holds

n1 = n2 ) )

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

ex b

( ( for n being Nat ex x being object st x = f . (b

n1 = n2 ) )

proof end;

:: deftheorem Def9 defines valued_reorganization FLEXARY1:def 9 :

for f being finite Function

for b_{2} being DoubleReorganization of dom f holds

( b_{2} is valued_reorganization of f iff ( ( for n being Nat ex x being object st x = f . (b_{2} _ (n,1)) & ... & x = f . (b_{2} _ (n,(len (b_{2} . n)))) ) & ( for n1, n2, i1, i2 being Nat st i1 in dom (b_{2} . n1) & i2 in dom (b_{2} . n2) & f . (b_{2} _ (n1,i1)) = f . (b_{2} _ (n2,i2)) holds

n1 = n2 ) ) );

for f being finite Function

for b

( b

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

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

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

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;