HILB10_7: Prime Representing Polynomial with 10 Unknowns -- Introduction

:: Prime Representing Polynomial with 10 Unknowns -- Introduction
:: by Karol P\kak
::
:: Received September 30, 2022
:: Copyright (c) 2022-2024 Association of Mizar Users

definition

let X be finite set ;

func [#] X -> Element of Fin X equals :: HILB10_7:def 1
X;

coherence by FINSUB_1:def 5;

end;

:: deftheorem defines [#] HILB10_7:def 1 :

theorem Th1: :: HILB10_7:1

for X1, X2, Y being non empty set
for F being BinOp of Y
for B1 being Element of Fin X1
for B2 being Element of Fin X2 st B1 = B2 & ( B1 <> {} or F is having_a_unity ) & F is associative & F is commutative holds
for f1 being Function of X1,Y
for f2 being Function of X2,Y st f1 | B1 = f2 | B2 holds
F $$ (B1,f1) = F $$ (B2,f2)

proof end;

theorem Th2: :: HILB10_7:2

for D being non empty set
for d1, d2 being Element of D
for B being BinOp of D st B is having_a_unity & B is associative & B is commutative & B is having_an_inverseOp holds
( B . (((the_inverseOp_wrt B) . d1),d2) = (the_inverseOp_wrt B) . (B . (d1,((the_inverseOp_wrt B) . d2))) & B . (d1,((the_inverseOp_wrt B) . d2)) = (the_inverseOp_wrt B) . (B . (((the_inverseOp_wrt B) . d1),d2)) )

proof end;

theorem Th3: :: HILB10_7:3

for D being non empty set
for A, M being BinOp of D st A is commutative & A is associative & A is having_a_unity & M is commutative & M is_distributive_wrt A & ( for d being Element of D holds M . ((the_unity_wrt A),d) = the_unity_wrt A ) holds
for X, Y being non empty finite set
for f being Function of X,D
for g being Function of Y,D
for a being Element of Fin X
for b being Element of Fin Y holds A $$ ([:a,b:],(M * (f,g))) = M . ((A $$ (a,f)),(A $$ (b,g)))

proof end;

theorem Th4: :: HILB10_7:4

for n being Nat
for D being non empty set
for M, A being BinOp of D
for d being Element of D st M is having_a_unity & A is associative & A is having_a_unity & A is having_an_inverseOp & M is_distributive_wrt A holds
( ( n is even implies M "**" (n |-> ((the_inverseOp_wrt A) . d)) = M "**" (n |-> d) ) & ( n is odd implies M "**" (n |-> ((the_inverseOp_wrt A) . d)) = (the_inverseOp_wrt A) . (M "**" (n |-> d)) ) )

proof end;

theorem Th5: :: HILB10_7:5

for y being object
for s being FinSequence st s " {y} <> {} holds
ex p being Permutation of (Seg (len s)) st
( (s * p) . (len s) = y & p = p " )

proof end;

registration

let D be non empty set ;

cluster Relation-like non-empty NAT -defined D * -valued Function-like non empty finite FinSequence-like FinSubsequence-like Function-yielding V60() FinSequence-yielding finite-support for FinSequence of D * ;

proof end;

end;

registration

let X, Y be non empty set ;

cluster UNION (X,Y) -> non empty ;

proof end;

end;

registration

let X, Y be finite set ;

cluster UNION (X,Y) -> finite ;

proof end;

end;

theorem Th6: :: HILB10_7:6

for X, Y being set holds UNION ((bool X),(bool Y)) = bool (X \/ Y)

proof end;

theorem Th7: :: HILB10_7:7

for X, Y1, Y2 being set holds UNION (X,(Y1 \/ Y2)) = (UNION (X,Y1)) \/ (UNION (X,Y2))

proof end;

theorem Th8: :: HILB10_7:8

for X, Y being set st X misses union Y holds
card (UNION (Y,{X})) = card Y

proof end;

theorem Th9: :: HILB10_7:9

for m being Nat st m <> 0 holds
2 * (card (bool ((Seg m) \ {1}))) = card (bool ((Seg (1 + m)) \ {1}))

proof end;

definition

let X be set ;
let a, b be object ;

func Ext (X,a,b) -> set equals :: HILB10_7:def 2
{ (A \/ {b}) where A is Element of X : a in A } \/ { A where A is Element of X : ( not a in A & A in X ) } ;

end;

:: deftheorem defines Ext HILB10_7:def 2 :

definition

let X be set ;
let a, b be object ;

func swap (X,a,b) -> set equals :: HILB10_7:def 3
{ ((A \ {a}) \/ {b}) where A is Element of X : a in A } \/ { (A \/ {a}) where A is Element of X : ( not a in A & A in X ) } ;

end;

:: deftheorem defines swap HILB10_7:def 3 :

theorem Th10: :: HILB10_7:10

for x, y being object
for Y being set st not y in union Y holds
card Y = card (Ext (Y,x,y))

proof end;

theorem Th11: :: HILB10_7:11

for x, y being object
for Y being set st not y in union Y holds
card Y = card (swap (Y,x,y))

proof end;

theorem Th12: :: HILB10_7:12

for x, y being object holds swap ({},x,y) = {}

proof end;

theorem Th13: :: HILB10_7:13

for x, y being object
for X, Y being set holds swap ((X \/ Y),x,y) = (swap (X,x,y)) \/ (swap (Y,x,y))

proof end;

theorem Th14: :: HILB10_7:14

for x, y being object
for X, Y being set st Y in swap (X,x,y) & x <> y & not y in union X holds
( x in Y iff not y in Y )

proof end;

theorem :: HILB10_7:15

for x, y being object holds Ext ({},x,y) = {}

proof end;

theorem Th16: :: HILB10_7:16

for x, y being object
for X, Y being set holds Ext ((X \/ Y),x,y) = (Ext (X,x,y)) \/ (Ext (Y,x,y))

proof end;

theorem Th17: :: HILB10_7:17

for x, y being object
for X, Y being set st Y in Ext (X,x,y) & not y in union X holds
( x in Y iff y in Y )

proof end;

registration

let X be finite set ;
let a, b be object ;

cluster swap (X,a,b) -> finite ;

proof end;

cluster Ext (X,a,b) -> finite ;

proof end;

end;

definition

let f be Function;
let a, b be object ;

func Swap (f,a,b) -> Function means :Def4: :: HILB10_7:def 4
( dom it = dom f & ( for x being object st x in dom f holds
( ( a in f . x implies it . x = ((f . x) \ {a}) \/ {b} ) & ( not a in f . x implies it . x = (f . x) \/ {a} ) ) ) );

proof end;

proof end;

end;

:: deftheorem Def4 defines Swap HILB10_7:def 4 :

definition

let f be Function;
let a, b be object ;

func Ext (f,a,b) -> Function means :Def5: :: HILB10_7:def 5
( dom it = dom f & ( for x being object st x in dom f holds
( ( a in f . x implies it . x = (f . x) \/ {b} ) & ( not a in f . x implies it . x = f . x ) ) ) );

proof end;

proof end;

end;

:: deftheorem Def5 defines Ext HILB10_7:def 5 :

registration

let f be FinSequence;
let a, b be object ;

cluster Swap (f,a,b) -> len f -element FinSequence-like ;

proof end;

cluster Ext (f,a,b) -> len f -element FinSequence-like ;

proof end;

end;

theorem Th18: :: HILB10_7:18

for a, b being object
for f, g being FinSequence holds Swap ((f ^ g),a,b) = (Swap (f,a,b)) ^ (Swap (g,a,b))

proof end;

theorem Th19: :: HILB10_7:19

for a, b being object
for f, g being FinSequence holds Ext ((f ^ g),a,b) = (Ext (f,a,b)) ^ (Ext (g,a,b))

proof end;

theorem Th20: :: HILB10_7:20

for a, b, x, y being object
for f being Function st b <> x & b <> y holds
( b in (Ext (f,x,y)) . a iff b in f . a )

proof end;

theorem Th21: :: HILB10_7:21

for a, b, x, y being object
for f being Function st b <> x & b <> y holds
( b in (Swap (f,x,y)) . a iff b in f . a )

proof end;

theorem Th22: :: HILB10_7:22

for x, y being object
for X, Y being set st x <> y & not y in union X & not y in union Y holds
Ext (X,x,y) misses swap (Y,x,y)

proof end;

theorem Th23: :: HILB10_7:23

for x, y being object
for f, g being Function holds (Swap (f,x,y)) * g = Swap ((f * g),x,y)

proof end;

theorem Th24: :: HILB10_7:24

for x, y being object
for X being set
for f being Function holds (Swap (f,x,y)) | X = Swap ((f | X),x,y)

proof end;

theorem Th25: :: HILB10_7:25

for x, y being object
for f, g being Function holds (Ext (f,x,y)) * g = Ext ((f * g),x,y)

proof end;

theorem Th26: :: HILB10_7:26

for x, y being object
for X being set
for f being Function holds (Ext (f,x,y)) | X = Ext ((f | X),x,y)

proof end;

registration

let X be finite set ;

cluster -> X -valued card X -element for Enumeration of X;

proof end;

end;

theorem Th27: :: HILB10_7:27

for x, y being object
for F being finite set
for E being Enumeration of F st not y in union F holds
Swap (E,x,y) is Enumeration of swap (F,x,y)

proof end;

theorem Th28: :: HILB10_7:28

for x, y being object
for F being finite set
for E being Enumeration of F st not y in union F holds
Ext (E,x,y) is Enumeration of Ext (F,x,y)

proof end;

theorem Th29: :: HILB10_7:29

for x, y being object
for X being set st x in X holds
Ext ({X},x,y) = {(X \/ {y})}

proof end;

theorem Th30: :: HILB10_7:30

for x, y being object
for X being set st not x in X holds
Ext ({X},x,y) = {X}

proof end;

theorem Th31: :: HILB10_7:31

for x, y being object
for X being set st x in X holds
swap ({X},x,y) = {((X \ {x}) \/ {y})}

proof end;

theorem Th32: :: HILB10_7:32

for x, y being object
for X being set st not x in X holds
swap ({X},x,y) = {(X \/ {x})}

proof end;

registration

let X be non empty set ;
let a, b be object ;

cluster Ext (X,a,b) -> non empty ;

proof end;

cluster swap (X,a,b) -> non empty ;

proof end;

end;

theorem Th33: :: HILB10_7:33

for x, y being object
for X, Y being set st not y in union X & not y in union Y holds
( X misses Y iff Ext (X,x,y) misses Ext (Y,x,y) )

proof end;

theorem Th34: :: HILB10_7:34

for x, y being object
for X, Y being set st x <> y & not y in union X & not y in union Y holds
( X misses Y iff swap (X,x,y) misses swap (Y,x,y) )

proof end;

theorem Th35: :: HILB10_7:35

for x, y, z being object
for f being Function st z in dom f holds
Ext (<*(f . z)*>,x,y) = <*((Ext (f,x,y)) . z)*>

proof end;

theorem Th36: :: HILB10_7:36

for x, y, z being object
for f being Function st z in dom f holds
Swap (<*(f . z)*>,x,y) = <*((Swap (f,x,y)) . z)*>

proof end;

theorem Th37: :: HILB10_7:37

for x, y, z being object
for f being Function st z in dom f holds
Ext ({(f . z)},x,y) = {((Ext (f,x,y)) . z)}

proof end;

theorem :: HILB10_7:38

for x, y, z being object
for f being Function st z in dom f holds
swap ({(f . z)},x,y) = {((Swap (f,x,y)) . z)}

proof end;

theorem Th39: :: HILB10_7:39

for m being Nat st m <> 0 holds
bool ((Seg (m + 2)) \ {1}) = (Ext ((bool ((Seg (m + 1)) \ {1})),(1 + m),(2 + m))) \/ (swap ((bool ((Seg (m + 1)) \ {1})),(1 + m),(2 + m)))

proof end;

definition

let f be finite Function;

attr f is with_evenly_repeated_values means :Def6: :: HILB10_7:def 6
for y being object holds card (f " {y}) is even ;

end;

:: deftheorem Def6 defines with_evenly_repeated_values HILB10_7:def 6 :

registration

cluster Relation-like Function-like empty finite -> finite with_evenly_repeated_values for set ;

coherence ;
let x be object ;

cluster <*x,x*> -> with_evenly_repeated_values ;

proof end;

end;

theorem Th40: :: HILB10_7:40

for f, g being with_evenly_repeated_values FinSequence holds f ^ g is with_evenly_repeated_values

proof end;

definition

let F be set ;

attr F is with_evenly_repeated_values-member means :Def7: :: HILB10_7:def 7
for y being object st y in F holds
y is finite with_evenly_repeated_values Function;

end;

:: deftheorem Def7 defines with_evenly_repeated_values-member HILB10_7:def 7 :

registration

cluster empty -> with_evenly_repeated_values-member for set ;

end;

registration

let X be FinSequence-membered set ;

cluster -> FinSequence-membered for Element of Fin X;

proof end;

end;

theorem Th41: :: HILB10_7:41

for P1, S1, S2 being FinSequence-membered set holds P1 ^ (S1 \/ S2) = (P1 ^ S1) \/ (P1 ^ S2)

proof end;

theorem Th42: :: HILB10_7:42

for P1, P2, S1 being FinSequence-membered set holds (P1 \/ P2) ^ S1 = (P1 ^ S1) \/ (P2 ^ S1)

proof end;

theorem Th43: :: HILB10_7:43

for f, g being FinSequence holds {f} ^ {g} = {(f ^ g)}

proof end;

registration

let f be finite with_evenly_repeated_values Function;

cluster {f} -> with_evenly_repeated_values-member ;

proof end;

let g be finite with_evenly_repeated_values Function;

cluster {f,g} -> with_evenly_repeated_values-member ;

proof end;

end;

registration

let F, G be FinSequence-membered with_evenly_repeated_values-member set ;

cluster F ^ G -> with_evenly_repeated_values-member ;

proof end;

end;

theorem Th44: :: HILB10_7:44

for f being finite Function
for p being Permutation of (dom f) holds
( f is with_evenly_repeated_values iff f * p is with_evenly_repeated_values )

proof end;

definition

let F be FinSequence-yielding FinSequence;

func doms F -> finite Subset of (NAT *) means :Def8: :: HILB10_7:def 8
for x being object holds
( x in it iff ex p being FinSequence st
( p = x & len p = len F & ( for i being Nat st i in dom p holds
p . i in dom (F . i) ) ) );

proof end;

proof end;

end;

:: deftheorem Def8 defines doms HILB10_7:def 8 :

theorem Th45: :: HILB10_7:45

for F being FinSequence-yielding FinSequence holds
( not doms F is empty iff F is non-empty )

proof end;

theorem Th46: :: HILB10_7:46

proof end;

registration

let F be FinSequence-yielding FinSequence;

cluster doms F -> finite FinSequence-membered ;

proof end;

end;

theorem Th47: :: HILB10_7:47

for F being FinSequence-yielding FinSequence
for p being FinSequence holds
( p in doms F iff ( len p = len F & ( for i being Nat st i in dom p holds
p . i in dom (F . i) ) ) )

proof end;

registration

let F be FinSequence-yielding FinSequence;

cluster -> NAT -valued for Element of doms F;

proof end;

end;

registration

let F be non-empty FinSequence-yielding FinSequence;

cluster doms F -> non empty finite ;

coherence by Th45;

end;

theorem Th48: :: HILB10_7:48

for F, G being FinSequence-yielding FinSequence
for f, g being FinSequence st f in doms F & g in doms G holds
f ^ g in doms (F ^ G)

proof end;

theorem Th49: :: HILB10_7:49

for F, G being FinSequence-yielding FinSequence
for P, S being FinSequence-membered set st P c= doms F & S c= doms G holds
P ^ S c= doms (F ^ G)

proof end;

theorem Th50: :: HILB10_7:50

for F, G being FinSequence-yielding FinSequence
for f, g being FinSequence st ( len f = len F or len g = len G ) & f ^ g in doms (F ^ G) holds
( f in doms F & g in doms G )

proof end;

theorem Th51: :: HILB10_7:51

for f, g being FinSequence holds
( f in doms <*g*> iff ( len f = 1 & f . 1 in dom g ) )

proof end;

theorem Th52: :: HILB10_7:52

for F being FinSequence-yielding FinSequence
for g being FinSequence
for x being object holds doms (F ^ <*(g ^ <*x*>)*>) = (doms (F ^ <*g*>)) \/ { (f ^ <*(1 + (len g))*>) where f is Element of doms F : f in doms F }

proof end;

theorem :: HILB10_7:53

for F being FinSequence-yielding FinSequence
for x being object holds doms (F ^ <*<*x*>*>) = { (f ^ <*1*>) where f is Element of doms F : f in doms F }

proof end;

theorem Th54: :: HILB10_7:54

for F, G being FinSequence-yielding FinSequence holds (NAT -concatenation) .: [:(doms F),(doms G):] = doms (F ^ G)

proof end;

theorem Th55: :: HILB10_7:55

for f being FinSequence holds doms <*f*> = { <*i*> where i is Element of NAT : i in dom f }

proof end;

registration

let n be Nat;
let F be FinSequence-yielding FinSequence;

cluster F | n -> FinSequence-yielding ;

end;

theorem :: HILB10_7:56

for n being Nat
for F being FinSequence-yielding FinSequence
for f being FinSequence st f in doms F holds
f | n in doms (F | n)

proof end;

theorem :: HILB10_7:57

for g being FinSequence holds card (doms <*g*>) = len g

proof end;

theorem :: HILB10_7:58

for F being FinSequence-yielding FinSequence
for f being FinSequence holds card (doms (F ^ <*f*>)) = (card (doms F)) * (len f)

proof end;

definition

let F be FinSequence-yielding FinSequence;

func App F -> FinSequence-yielding Function means :Def9: :: HILB10_7:def 9
( dom it = doms F & ( for p being FinSequence st p in doms F holds
( len (it . p) = len p & ( for i being Nat st i in dom p holds
(it . p) . i = (F . i) . (p . i) ) ) ) );

proof end;

proof end;

end;

:: deftheorem Def9 defines App HILB10_7:def 9 :

definition

let D be non empty set ;
let F be D * -valued FinSequence;
:: original: App
redefine func App F -> Function of (doms F),(D *);
coherence

proof end;

end;

theorem Th59: :: HILB10_7:59

(App {}) . {} = {}

proof end;

theorem Th60: :: HILB10_7:60

for i being Nat
for f being FinSequence st i in dom f holds
(App <*f*>) . <*i*> = <*(f . i)*>

proof end;

theorem Th61: :: HILB10_7:61

for F, G being FinSequence-yielding FinSequence
for f, g being FinSequence st f in doms F & g in doms G holds
(App (F ^ G)) . (f ^ g) = ((App F) . f) ^ ((App G) . g)

proof end;

registration

let D be non empty set ;
let F be D * -valued non empty FinSequence;

cluster App F -> non-empty FinSequence-yielding ;

proof end;

end;

definition

let D be non empty set ;
let f be D * -valued Function;
let x be object ;
:: original: .
redefine func f . x -> FinSequence of D;
coherence

proof end;

end;

definition

let D be non empty set ;
let B be BinOp of D;
let F be D * -valued Function;

func B "**" F -> Function of (dom F),D means :Def10: :: HILB10_7:def 10
for x being object st x in dom F holds
it . x = B "**" (F . x);

proof end;

proof end;

end;

:: deftheorem Def10 defines "**" HILB10_7:def 10 :

registration

let D be non empty set ;
let B be BinOp of D;
let F be D * -valued FinSequence;

cluster B "**" F -> len F -element FinSequence-like ;

proof end;

end;

definition

let D be set ;
let f be FinSequence of D;
:: original: <*
redefine func <*f*> -> FinSequence of D * ;
coherence

proof end;

end;

theorem Th62: :: HILB10_7:62

for D being non empty set
for A being BinOp of D
for f being FinSequence of D holds A "**" <*f*> = <*(A "**" f)*>

proof end;

theorem Th63: :: HILB10_7:63

for D being non empty set
for A being BinOp of D
for F, G being b₁ * -valued FinSequence holds A "**" (F ^ G) = (A "**" F) ^ (A "**" G)

proof end;

registration

let f be non empty FinSequence;

cluster <*f*> -> non-empty ;

end;

theorem Th64: :: HILB10_7:64

for D being non empty set
for A being BinOp of D st A is commutative & A is associative holds
for f, g being non empty FinSequence
for F being Function of (dom f),D
for G being Function of (dom g),D
for FG being Function of (dom (f ^ g)),D st f = F & g = G & f ^ g = FG holds
A $$ (([#] (dom (f ^ g))),FG) = A . ((A $$ (([#] (dom f)),F)),(A $$ (([#] (dom g)),G)))

proof end;

theorem Th65: :: HILB10_7:65

for D being non empty set
for A, M being BinOp of D
for F, G being non-empty non empty FinSequence of D * st M is commutative & M is associative holds
M $$ (([#] (dom (F ^ G))),(A "**" (F ^ G))) = M . ((M $$ (([#] (dom F)),(A "**" F))),(M $$ (([#] (dom G)),(A "**" G))))

proof end;

theorem Th66: :: HILB10_7:66

for D being non empty set
for A, M being BinOp of D
for f being non empty FinSequence of D st M is commutative & M is associative holds
M $$ (([#] (dom <*f*>)),(A "**" <*f*>)) = A "**" f

proof end;

theorem Th67: :: HILB10_7:67

for D being non empty set
for A, M being BinOp of D
for F being non-empty non empty FinSequence of D *
for f being non empty FinSequence of D st M is commutative & M is associative & A is commutative & A is associative & M is_left_distributive_wrt A holds
for fM being Function of (dom f),D st ( for x being object st x in dom f holds
fM . x = M . ((M $$ (([#] (dom F)),(A "**" F))),(f . x)) ) holds
M $$ (([#] (dom (F ^ <*f*>))),(A "**" (F ^ <*f*>))) = A $$ (([#] (dom f)),fM)

proof end;

theorem Th68: :: HILB10_7:68

for D being non empty set
for A, M being BinOp of D
for F being non-empty non empty FinSequence of D * st len F = 1 & M is commutative & M is associative & A is commutative & A is associative holds
M $$ (([#] (dom F)),(A "**" F)) = A $$ (([#] (dom (App F))),(M "**" (App F)))

proof end;

theorem :: HILB10_7:69

for D being non empty set
for A, M being BinOp of D
for F being non-empty non empty FinSequence of D * st M is commutative & M is associative & A is commutative & A is associative & A is having_a_unity & M is_distributive_wrt A holds
M $$ (([#] (dom F)),(A "**" F)) = A $$ (([#] (dom (App F))),(M "**" (App F)))

proof end;

definition

let D be non empty set ;
let B be BinOp of D;
let f be FinSequence of D;
let X be set ;

func SignGen (f,B,X) -> FinSequence of D means :Def11: :: HILB10_7:def 11
( dom it = dom f & ( for i being Nat st i in dom it holds
( ( i in X implies it . i = (the_inverseOp_wrt B) . (f . i) ) & ( not i in X implies it . i = f . i ) ) ) );

proof end;

proof end;

end;

:: deftheorem Def11 defines SignGen HILB10_7:def 11 :

registration

let D be non empty set ;
let B be BinOp of D;
let f be FinSequence of D;
let X be set ;

cluster SignGen (f,B,X) -> len f -element ;

proof end;

end;

theorem Th70: :: HILB10_7:70

for X being set
for D being non empty set
for B being BinOp of D
for f being FinSequence of D st X misses dom f holds
SignGen (f,B,X) = f

proof end;

theorem Th71: :: HILB10_7:71

for D being non empty set
for B being BinOp of D
for f being FinSequence of D holds SignGen (f,B,{}) = f

proof end;

theorem Th72: :: HILB10_7:72

for n being Nat
for X being set
for D being non empty set
for B being BinOp of D
for f being FinSequence of D holds SignGen ((f | n),B,X) = (SignGen (f,B,X)) | n

proof end;

theorem Th73: :: HILB10_7:73

for n being Nat
for X being set
for D being non empty set
for B being BinOp of D
for f being FinSequence of D st n + 1 = len f & n + 1 in X holds
SignGen (f,B,X) = (SignGen ((f | n),B,X)) ^ <*((the_inverseOp_wrt B) . (f . (n + 1)))*>

proof end;

theorem Th74: :: HILB10_7:74

for n being Nat
for X being set
for D being non empty set
for B being BinOp of D
for f being FinSequence of D st n + 1 = len f & not n + 1 in X holds
SignGen (f,B,X) = (SignGen ((f | n),B,X)) ^ <*(f . (n + 1))*>

proof end;

theorem :: HILB10_7:75

for X being set
for D being non empty set
for B being BinOp of D
for f being FinSequence of D st dom f c= X holds
SignGen (f,B,X) = (the_inverseOp_wrt B) * f

proof end;

theorem :: HILB10_7:76

for X being set
for D being non empty set
for B being BinOp of D
for f being FinSequence of D st B is having_a_unity & B is associative & B is having_an_inverseOp holds
SignGen ((SignGen (f,B,X)),B,X) = f

proof end;

registration

let E be non empty set ;
let D be set ;
let p be D -valued FinSequence;
let h be Function of D,E;

cluster p * h -> len p -element FinSequence-like ;

proof end;

end;

definition

let D be non empty set ;
let B be BinOp of D;
let f be FinSequence of D;
let F be finite set ;

func SignGenOp (f,B,F) -> Function of F,(D *) means :Def12: :: HILB10_7:def 12
for X being set st X in F holds
it . X = SignGen (f,B,X);

proof end;

proof end;

end;

:: deftheorem Def12 defines SignGenOp HILB10_7:def 12 :

theorem Th77: :: HILB10_7:77

for x being object
for E being Enumeration of {x} holds E = <*x*>

proof end;

theorem Th78: :: HILB10_7:78

for X being set
for D being non empty set
for B being BinOp of D
for f being FinSequence of D
for E being Enumeration of {X} holds (SignGenOp (f,B,{X})) * E = <*(SignGen (f,B,X))*>

proof end;

theorem Th79: :: HILB10_7:79

for F1, F2 being finite set
for E1 being Enumeration of F1
for E2 being Enumeration of F2 st F1 misses F2 holds
E1 ^ E2 is Enumeration of F1 \/ F2

proof end;

theorem Th80: :: HILB10_7:80

for i being Nat
for D being non empty set
for B being BinOp of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F st ( i in dom E or i in dom ((SignGenOp (f,B,F)) * E) ) holds
((SignGenOp (f,B,F)) * E) . i = SignGen (f,B,(E . i))

proof end;

theorem Th81: :: HILB10_7:81

for D being non empty set
for B being BinOp of D
for f being FinSequence of D
for F1, F2 being finite set
for E1 being Enumeration of F1
for E2 being Enumeration of F2
for E12 being Enumeration of F1 \/ F2 st E12 = E1 ^ E2 holds
(SignGenOp (f,B,(F1 \/ F2))) * E12 = ((SignGenOp (f,B,F1)) * E1) ^ ((SignGenOp (f,B,F2)) * E2)

proof end;

theorem Th82: :: HILB10_7:82

for D being non empty set
for B being BinOp of D
for d being Element of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F st ( B is having_a_unity or len f >= 1 ) & not 1 + (len f) in union F holds
B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E) = B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),d)

proof end;

theorem Th83: :: HILB10_7:83

for D being non empty set
for B being BinOp of D
for d being Element of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F st ( B is having_a_unity or len f >= 1 ) & 1 + (len f) in meet F holds
B "**" ((SignGenOp ((f ^ <*d*>),B,F)) * E) = B [:] ((B "**" ((SignGenOp (f,B,F)) * E)),((the_inverseOp_wrt B) . d))

proof end;

theorem Th84: :: HILB10_7:84

for D being non empty set
for B being BinOp of D
for d1, d2 being Element of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F st ( B is having_a_unity or len f >= 1 ) & B is associative & not 1 + (len f) in union F & not 2 + (len f) in union F holds
B "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),B,F)) * E) = B "**" ((SignGenOp ((f ^ <*(B . (d1,d2))*>),B,F)) * E)

proof end;

theorem Th85: :: HILB10_7:85

for D being non empty set
for B being BinOp of D
for d1, d2 being Element of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F st ( B is having_a_unity or len f >= 1 ) & B is associative & not 1 + (len f) in union F & 2 + (len f) in meet F holds
B "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),B,F)) * E) = B "**" ((SignGenOp ((f ^ <*(B . (d1,((the_inverseOp_wrt B) . d2)))*>),B,F)) * E)

proof end;

theorem Th86: :: HILB10_7:86

for D being non empty set
for B being BinOp of D
for d1, d2 being Element of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F st B is having_a_unity & B is associative & B is commutative & B is having_an_inverseOp & 1 + (len f) in meet F & not 2 + (len f) in union F holds
B "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),B,F)) * E) = B "**" ((SignGenOp ((f ^ <*(B . (d1,((the_inverseOp_wrt B) . d2)))*>),B,F)) * E)

proof end;

theorem Th87: :: HILB10_7:87

for D being non empty set
for B being BinOp of D
for d1, d2 being Element of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F st B is having_a_unity & B is associative & B is commutative & B is having_an_inverseOp & 1 + (len f) in meet F & 2 + (len f) in meet F holds
B "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),B,F)) * E) = B "**" ((SignGenOp ((f ^ <*(B . (d1,d2))*>),B,F)) * E)

proof end;

theorem Th88: :: HILB10_7:88

for X being set
for F being finite set
for E being Enumeration of F st X misses union F holds
ex Ex being Enumeration of UNION (F,{X}) st
for i being Nat st i in dom E holds
Ex . i = X \/ (E . i)

proof end;

theorem Th89: :: HILB10_7:89

for X being set
for D being non empty set
for B being BinOp of D
for f being FinSequence of D holds SignGen (f,B,X) = SignGen (f,B,(X /\ (dom f)))

proof end;

theorem Th90: :: HILB10_7:90

for D being non empty set
for A being BinOp of D
for f being FinSequence of D
for F1, F2 being finite set
for E1 being Enumeration of F1
for E2 being Enumeration of F2 st card F1 = card F2 & ( for i being Nat st i in dom E1 holds
(dom f) /\ (E1 . i) = (dom f) /\ (E2 . i) ) holds
(SignGenOp (f,A,F1)) * E1 = (SignGenOp (f,A,F2)) * E2

proof end;

theorem Th91: :: HILB10_7:91

for D being non empty set
for A being BinOp of D
for d1, d2 being Element of D
for f being FinSequence of D st A is having_a_unity & A is associative & A is commutative & A is having_an_inverseOp holds
for F being non empty finite set st union F c= dom f holds
for F1, F2 being finite set st F1 = UNION (F,(bool {((len f) + 1)})) & F2 = UNION (F,(bool {((len f) + 1),((len f) + 2)})) holds
ex E1 being Enumeration of F1 ex E2 being Enumeration of F2 st A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F2)) * E2) = (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * E1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,F1)) * E1))

proof end;

definition

let D be non empty set ;
let A, M be BinOp of D;
assume A1: ( M is commutative & M is associative ) ;
let f be FinSequence of D;
let F be finite set ;

func SignGenOp (f,M,A,F) -> Element of D means :Def13: :: HILB10_7:def 13
for E being Enumeration of bool F holds it = M $$ (([#] (dom ((SignGenOp (f,A,(bool F))) * E))),(A "**" ((SignGenOp (f,A,(bool F))) * E)));

proof end;

proof end;

end;

:: deftheorem Def13 defines SignGenOp HILB10_7:def 13 :

theorem Th92: :: HILB10_7:92

for D being non empty set
for A, M being BinOp of D st M is commutative & M is associative & A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is_distributive_wrt A holds
for CE1, CE2, CE12 being non-empty non empty FinSequence of D * st CE12 = CE1 ^ CE2 holds
for S1 being Element of Fin (dom (App CE1))
for s2 being Element of dom (App CE2)
for S12 being Element of Fin (dom (App CE12)) st S12 = S1 ^ {s2} holds
M . ((A $$ (S1,(M "**" (App CE1)))),((M "**" (App CE2)) . s2)) = A $$ (S12,(M "**" (App CE12)))

proof end;

theorem Th93: :: HILB10_7:93

for D being non empty set
for A, M being BinOp of D st M is commutative & M is associative & A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is_distributive_wrt A holds
for CE1, CE2, CE12 being non-empty non empty FinSequence of D * st CE12 = CE1 ^ CE2 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2))
for S12 being Element of Fin (dom (App CE12)) st S12 = S1 ^ S2 holds
M . ((A $$ (S1,(M "**" (App CE1)))),(A $$ (S2,(M "**" (App CE2))))) = A $$ (S12,(M "**" (App CE12)))

proof end;

theorem :: HILB10_7:94

for D being non empty set
for A being BinOp of D
for f, g being FinSequence of D
for F1 being finite set
for E1 being Enumeration of F1 holds doms ((SignGenOp (f,A,F1)) * E1) c= doms ((SignGenOp ((f ^ g),A,F1)) * E1)

proof end;

theorem :: HILB10_7:95

for D being non empty set
for A, M being BinOp of D
for f, g being FinSequence of D
for F1 being finite set st A is having_a_unity & A is commutative & A is associative holds
for E1 being Enumeration of F1
for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp ((f ^ g),A,F1)) * E1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S1 = S2 holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))

proof end;

theorem Th96: :: HILB10_7:96

for n being Nat
for F being finite set
for E being Enumeration of F st len E = n + 1 holds
( E | n is Enumeration of F \ {(E . (len E))} & <*(E . (len E))*> is Enumeration of {(E . (len E))} & F = (F \ {(E . (len E))}) \/ {(E . (len E))} )

proof end;

registration

let F be with_evenly_repeated_values-member set ;

cluster -> Relation-like Function-like finite for Element of F;

proof end;

end;

registration

let F be with_evenly_repeated_values-member set ;

cluster -> with_evenly_repeated_values for Element of F;

proof end;

end;

theorem Th97: :: HILB10_7:97

for F1 being finite set
for E1 being Enumeration of F1
for p being Function st union F1 c= dom p & p | (union F1) is one-to-one holds
( (.: p) * E1 is Enumeration of (.: p) .: F1 & card E1 = card ((.: p) * E1) )

proof end;

theorem Th98: :: HILB10_7:98

for D being non empty set
for A being BinOp of D
for f being FinSequence of D
for F1 being finite set
for E1 being Enumeration of F1
for g being Function st union F1 c= dom g & g | (union F1) is one-to-one holds
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st g .: (dom f) c= dom fg holds
for s being FinSequence st s in doms ((SignGenOp (f,A,F1)) * E1) & rng s c= dom g holds
g * s in doms ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)

proof end;

theorem Th99: :: HILB10_7:99

for D being non empty set
for A being BinOp of D
for f being FinSequence of D
for F1 being finite set
for E1 being Enumeration of F1
for g being Function st union F1 c= dom g & g is one-to-one holds
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = (f * (g ")) | (dom fg) & g .: (dom f) c= dom fg holds
for s being FinSequence st s in doms ((SignGenOp (f,A,F1)) * E1) & rng s c= dom g holds
(App ((SignGenOp (f,A,F1)) * E1)) . s = (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)) . (g * s)

proof end;

theorem Th100: :: HILB10_7:100

for D being non empty set
for A being BinOp of D
for f being FinSequence of D
for F1 being finite set
for E1 being Enumeration of F1 st union F1 c= dom f holds
for g being Permutation of (dom f)
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = f * (g ") holds
for S1 being Element of Fin (dom (App ((SignGenOp (f,A,F1)) * E1))) holds { (g * s) where s is FinSequence of NAT : s in S1 } is Element of Fin (dom (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)))

proof end;

theorem :: HILB10_7:101

for D being non empty set
for A, M being BinOp of D
for f being FinSequence of D
for F1 being finite set st A is having_a_unity & A is commutative & A is associative holds
for E1 being Enumeration of F1 st union F1 c= dom f holds
for g being Permutation of (dom f)
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = f * (g ") holds
for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp (fg,A,((.: g) .: F1))) * gE1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S2 = { (g * s) where s is FinSequence of NAT : s in S1 } holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))

proof end;

Lm1: for X being set
for S being with_evenly_repeated_values-member set st ( for x being Element of S st x in S holds
dom x = X ) holds
for p being Permutation of X holds { (s * p) where s is FinSequence of NAT : s in S } is with_evenly_repeated_values-member

proof end;

theorem Th102: :: HILB10_7:102

for n being Nat
for D being non empty set
for A being BinOp of D
for f being FinSequence of D
for F1 being finite set
for E1 being Enumeration of F1 st n in dom f holds
(len E1) |-> n in doms ((SignGenOp (f,A,F1)) * E1)

proof end;

theorem Th103: :: HILB10_7:103

for D being non empty set
for B being BinOp of D
for d1, d2 being Element of D st B is having_a_unity & B is associative & B is commutative & B is having_an_inverseOp holds
(the_inverseOp_wrt B) . (B . (d1,d2)) = B . (((the_inverseOp_wrt B) . d1),((the_inverseOp_wrt B) . d2))

proof end;

registration

let x be object ;
let n be even Nat;

cluster n |-> x -> with_evenly_repeated_values ;

proof end;

end;

theorem :: HILB10_7:104

for f, g being FinSequence st f ^ g is with_evenly_repeated_values & f is with_evenly_repeated_values holds
g is with_evenly_repeated_values

proof end;

theorem Th105: :: HILB10_7:105

for f, g being FinSequence st f ^ g is with_evenly_repeated_values & g is with_evenly_repeated_values holds
f is with_evenly_repeated_values

proof end;

registration

let x be object ;
let n be even Nat;

cluster n |-> x -> with_evenly_repeated_values ;

proof end;

end;

registration

let X, Y be with_evenly_repeated_values-member set ;

cluster X \/ Y -> with_evenly_repeated_values-member ;

proof end;

end;

definition

let n, k be Nat;

func doms (n,k) -> finite FinSequence-membered set equals :: HILB10_7:def 14
k -tuples_on (Seg n);

end;

:: deftheorem defines doms HILB10_7:def 14 :

registration

let n, k be Nat;

cluster -> Seg n -valued for Element of doms (n,k);

proof end;

end;

registration

let n be non empty Nat;
let k be Nat;

cluster doms (n,k) -> non empty finite FinSequence-membered ;

cluster -> k -element for Element of doms (n,k);

end;

theorem Th106: :: HILB10_7:106

for D being non empty set
for A being BinOp of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F holds doms ((SignGenOp (f,A,F)) * E) = doms ((len f),(card F))

proof end;

Lm2: for D being non empty set
for A being BinOp of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F holds doms ((SignGenOp (f,A,F)) * E) = doms ((len f),(len E))

proof end;

Lm3: for D being non empty set
for A being BinOp of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F holds
( dom (App ((SignGenOp (f,A,F)) * E)) = doms ((len f),(card F)) & dom (App ((SignGenOp (f,A,F)) * E)) = doms ((len f),(len E)) )

proof end;

theorem Th107: :: HILB10_7:107

for D being non empty set
for A being BinOp of D
for f, g being FinSequence of D
for F1, F2 being finite set
for E1 being Enumeration of F1
for E2 being Enumeration of F2 st card F1 = card F2 & len f <= len g holds
doms ((SignGenOp (f,A,F1)) * E1) c= doms ((SignGenOp (g,A,F2)) * E2)

proof end;

theorem :: HILB10_7:108

for D being non empty set
for A being BinOp of D
for f being FinSequence of D
for F1, F2 being finite set
for E1 being Enumeration of F1
for E2 being Enumeration of F2 st card F1 = card F2 holds
doms ((SignGenOp (f,A,F1)) * E1) = doms ((SignGenOp (f,A,F2)) * E2)

proof end;

theorem Th109: :: HILB10_7:109

for F being finite set
for E being Enumeration of F
for p being Permutation of (dom E) holds E * p is Enumeration of F

proof end;

theorem Th110: :: HILB10_7:110

for D being non empty set
for A being BinOp of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F
for p being Permutation of (dom E)
for s being FinSequence st s in doms ((SignGenOp (f,A,F)) * E) holds
s * p in doms ((SignGenOp (f,A,F)) * (E * p))

proof end;

theorem Th111: :: HILB10_7:111

for D being non empty set
for A being BinOp of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F
for p being Permutation of (dom E)
for s being FinSequence st s in doms ((SignGenOp (f,A,F)) * E) holds
((App ((SignGenOp (f,A,F)) * E)) . s) * p = (App ((SignGenOp (f,A,F)) * (E * p))) . (s * p)

proof end;

theorem Th112: :: HILB10_7:112

for D being non empty set
for A, M being BinOp of D
for f being FinSequence of D
for F being finite set st M is commutative & M is associative holds
for E being Enumeration of F
for p being Permutation of (dom E)
for s being FinSequence st s in doms ((SignGenOp (f,A,F)) * E) & ( len s >= 1 or M is having_a_unity ) holds
(M "**" (App ((SignGenOp (f,A,F)) * E))) . s = (M "**" (App ((SignGenOp (f,A,F)) * (E * p)))) . (s * p)

proof end;

theorem Th113: :: HILB10_7:113

for D being non empty set
for A being BinOp of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F
for p being Permutation of (dom E)
for S being Element of Fin (dom (App ((SignGenOp (f,A,F)) * E))) holds { (s * p) where s is FinSequence of NAT : s in S } is Element of Fin (dom (App ((SignGenOp (f,A,F)) * (E * p))))

proof end;

theorem :: HILB10_7:114

for n being Nat
for F being finite set
for E being Enumeration of F
for p being Permutation of (dom E)
for S being Element of Fin (doms (n,(card F))) holds { (s * p) where s is FinSequence of NAT : s in S } is Element of Fin (doms (n,(card F)))

proof end;

theorem Th115: :: HILB10_7:115

for D being non empty set
for A, M being BinOp of D
for f being FinSequence of D
for F being finite set st M is commutative & M is associative & A is having_a_unity & A is commutative & A is associative holds
for E being Enumeration of F
for p being Permutation of (dom E) st ( M is having_a_unity or len E >= 1 ) holds
for CE, CEp being non-empty non empty FinSequence of D * st CE = (SignGenOp (f,A,F)) * E & CEp = (SignGenOp (f,A,F)) * (E * p) holds
for S being Element of Fin (dom (App CE))
for Sp being Element of Fin (dom (App CEp)) st Sp = { (s * p) where s is FinSequence of NAT : s in S } holds
A $$ (S,(M "**" (App CE))) = A $$ (Sp,(M "**" (App CEp)))

proof end;

theorem Th116: :: HILB10_7:116

for D being non empty set
for A being BinOp of D
for d1 being Element of D
for f being FinSequence of D st A is having_a_unity & A is associative & A is having_an_inverseOp holds
for F, Fb being finite set st Fb = UNION (F,(bool {((len f) + 1)})) & union F c= dom f holds
for E1 being Enumeration of Fb ex E2 being Enumeration of Fb st (SignGenOp ((f ^ <*d1*>),A,Fb)) * E1 = (SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E2

proof end;

theorem Th117: :: HILB10_7:117

for D being non empty set
for A being BinOp of D
for d1, d2 being Element of D
for f being FinSequence of D st A is having_a_unity & A is associative & A is commutative & A is having_an_inverseOp holds
for F being non empty finite set st union F c= dom f holds
for F1, F2 being finite set st F1 = UNION (F,(bool {((len f) + 1)})) & F2 = UNION (F,(bool {((len f) + 1),((len f) + 2)})) holds
ex E1, E2 being Enumeration of F1 ex E being Enumeration of F2 st A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F2)) * E) = (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * E1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F1)) * E2))

proof end;

theorem Th118: :: HILB10_7:118

for D being non empty set
for B, A being BinOp of D
for f being FinSequence of D
for F being finite set st A is having_a_unity holds
for E being Enumeration of F
for s being FinSequence st F = {} & s in doms ((SignGenOp (f,B,F)) * E) holds
(A "**" (App ((SignGenOp (f,B,F)) * E))) . s = the_unity_wrt A

proof end;

theorem Th119: :: HILB10_7:119

for n being Nat
for F being finite set
for E being Enumeration of F
for p being Permutation of (dom E)
for S being Subset of (doms (n,(card F))) holds { (s * p) where s is FinSequence of NAT : s in S } is Subset of (doms (n,(card F)))

proof end;

theorem Th120: :: HILB10_7:120

for n, k, m being Nat
for f, g being FinSequence st ( len f = n or len g = m ) & f ^ g in doms (k,(n + m)) holds
( f in doms (k,n) & g in doms (k,m) )

proof end;

theorem Th121: :: HILB10_7:121

for n, k being Nat
for f being FinSequence st f in doms (n,k) holds
len f = k

proof end;

theorem Th122: :: HILB10_7:122

for n, k, m being Nat
for f, g being FinSequence st f in doms (k,n) & g in doms (k,m) holds
f ^ g in doms (k,(n + m))

proof end;

theorem Th123: :: HILB10_7:123

for n, k, m being Nat holds (doms (k,n)) ^ (doms (k,m)) = doms (k,(n + m))

proof end;

theorem Th124: :: HILB10_7:124

for m being Nat
for F being finite set
for E being Enumeration of F
for p being Permutation of (dom E)
for s being FinSequence st s in doms (m,(card F)) holds
s * p in doms (m,(card F))

proof end;

theorem Th125: :: HILB10_7:125

for n, k, m being Nat st k <= n holds
doms (k,m) c= doms (n,m)

proof end;

theorem Th126: :: HILB10_7:126

for m being Nat
for D being non empty set
for A, M being BinOp of D
for F1, F2 being finite set st A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is associative & M is commutative & M is having_a_unity & M is_distributive_wrt A holds
for E1 being Enumeration of F1
for E2 being Enumeration of F2 st union F1 c= Seg (1 + m) & union F2 c= Seg (1 + m) holds
for Ee being Enumeration of Ext (F1,(1 + m),(2 + m))
for Es being Enumeration of swap (F2,(1 + m),(2 + m)) st Ee = Ext (E1,(1 + m),(2 + m)) & Es = Swap (E2,(1 + m),(2 + m)) holds
for Ees being Enumeration of (Ext (F1,(1 + m),(2 + m))) \/ (swap (F2,(1 + m),(2 + m))) st Ees = Ee ^ Es holds
for s1, s2 being FinSequence st s1 in doms ((m + 1),(card F1)) & s2 in doms ((m + 1),(card F2)) & s1 ^ s2 is with_evenly_repeated_values & card (s1 " {(1 + m)}) = card (s2 " {(1 + m)}) holds
ex S being Subset of (doms ((m + 2),((card F1) + (card F2)))) st
( ( card (s1 " {(1 + m)}) = 0 implies s1 ^ s2 in S ) & S is with_evenly_repeated_values-member & ( for CE1, CE2 being FinSequence of D *
for f being FinSequence of D
for d1, d2 being Element of D st len f = m & CE1 = (SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * E1 & CE2 = (SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F2)) * E2 holds
for CFes being non-empty non empty FinSequence of D * st CFes = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F1,(1 + (len f)),(2 + (len f)))) \/ (swap (F2,(1 + (len f)),(2 + (len f))))))) * Ees holds
for Sd being Element of Fin (dom (App CFes)) st S = Sd holds
( M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2)) = A $$ (Sd,(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in Sd & i in dom h holds
( ( (s1 ^ s2) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) & ( (s1 ^ s2) . i <> 1 + (len f) implies h . i = (s1 ^ s2) . i ) ) ) ) ) )

proof end;

theorem Th127: :: HILB10_7:127

for m being Nat
for D being non empty set
for A, M being BinOp of D
for F1 being finite set st A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is associative & M is commutative & M is having_a_unity & M is_distributive_wrt A holds
for E1 being Enumeration of F1 st union F1 c= Seg (1 + m) holds
for Ee being Enumeration of Ext (F1,(1 + m),(2 + m)) st Ee = Ext (E1,(1 + m),(2 + m)) holds
ex S being Subset of (doms ((m + 2),(card F1))) st
( S = (len E1) -tuples_on {(1 + m),(2 + m)} & ( for CFe being non-empty non empty FinSequence of D *
for f being FinSequence of D
for d1, d2 being Element of D st len f = m & CFe = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext (F1,(1 + (len f)),(2 + (len f)))))) * Ee holds
for Sd being Element of Fin (dom (App CFe)) st Sd = S holds
(M "**" (App ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * E1))) . ((len E1) |-> (1 + (len f))) = A $$ (Sd,(M "**" (App CFe))) ) )

proof end;

theorem Th128: :: HILB10_7:128

for D being non empty set
for A, M being BinOp of D
for d1, d2 being Element of D
for f being FinSequence of D
for F1 being finite set st A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp holds
for E1 being Enumeration of F1 st union F1 c= Seg (1 + (len f)) holds
for Ee being Enumeration of Ext (F1,(1 + (len f)),(2 + (len f)))
for Es being Enumeration of swap (F1,(1 + (len f)),(2 + (len f))) st Ee = Ext (E1,(1 + (len f)),(2 + (len f))) & Es = Swap (E1,(1 + (len f)),(2 + (len f))) holds
for CFe, CFs being non-empty non empty FinSequence of D * st CFe = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext (F1,(1 + (len f)),(2 + (len f)))))) * Ee & CFs = (SignGenOp (((f ^ <*((the_inverseOp_wrt A) . d1)*>) ^ <*d2*>),A,(swap (F1,(1 + (len f)),(2 + (len f)))))) * Es holds
for S1 being Element of Fin (dom (App CFe))
for S2 being Element of Fin (dom (App CFs)) st S1 = S2 holds
A $$ (S1,(M "**" (App CFe))) = A $$ (S2,(M "**" (App CFs)))

proof end;

theorem Th129: :: HILB10_7:129

for m being Nat
for D being non empty set
for A, M being BinOp of D
for F1 being finite set st A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is associative & M is commutative & M is having_a_unity & M is_distributive_wrt A holds
for E1 being Enumeration of F1 st union F1 c= Seg (1 + m) holds
for Es being Enumeration of swap (F1,(1 + m),(2 + m)) st Es = Swap (E1,(1 + m),(2 + m)) holds
ex S being Subset of (doms ((m + 2),(card F1))) st
( S = (len E1) -tuples_on {(1 + m),(2 + m)} & ( for CFs being non-empty non empty FinSequence of D *
for f being FinSequence of D
for d1, d2 being Element of D st len f = m & CFs = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(swap (F1,(1 + (len f)),(2 + (len f)))))) * Es holds
for Sd being Element of Fin (dom (App CFs)) st Sd = S holds
(M "**" (App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F1)) * E1))) . ((len E1) |-> (1 + (len f))) = A $$ (Sd,(M "**" (App CFs))) ) )

proof end;

theorem Th130: :: HILB10_7:130

for D being non empty set
for A, M being BinOp of D
for d1, d2 being Element of D
for f being FinSequence of D st A is having_a_unity & A is associative & A is commutative & A is having_an_inverseOp & M is commutative & M is associative & len f <> 0 holds
SignGenOp (((f ^ <*d1*>) ^ <*d2*>),M,A,((Seg (2 + (len f))) \ {1})) = M . ((SignGenOp ((f ^ <*(A . (d1,d2))*>),M,A,((Seg (1 + (len f))) \ {1}))),(SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),M,A,((Seg (1 + (len f))) \ {1}))))

proof end;

theorem :: HILB10_7:131

for D being non empty set
for A being BinOp of D
for d, d1, d2 being Element of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F st union F c= Seg (1 + (len f)) holds
for Ee being Enumeration of Ext (F,(1 + (len f)),(2 + (len f))) st Ee = Ext (E,(1 + (len f)),(2 + (len f))) holds
for CE1, CEE being FinSequence of D * st CE1 = (SignGenOp ((f ^ <*d*>),A,F)) * E & CEE = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext (F,(1 + (len f)),(2 + (len f)))))) * Ee holds
for s being FinSequence st s in doms CE1 & rng s c= dom f holds
( s in doms CEE & (App CE1) . s = (App CEE) . s )

proof end;

theorem :: HILB10_7:132

for D being non empty set
for A being BinOp of D
for d, d1, d2 being Element of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F st union F c= Seg (1 + (len f)) holds
for Es being Enumeration of swap (F,(1 + (len f)),(2 + (len f))) st Es = Swap (E,(1 + (len f)),(2 + (len f))) holds
for CE1, CES being FinSequence of D * st CE1 = (SignGenOp ((f ^ <*d*>),A,F)) * E & CES = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(swap (F,(1 + (len f)),(2 + (len f)))))) * Es holds
for s being FinSequence st s in doms CE1 & rng s c= dom f holds
( s in doms CES & (App CE1) . s = (App CES) . s )

proof end;

theorem Th133: :: HILB10_7:133

for D being non empty set
for A being BinOp of D
for d1, d2 being Element of D
for f being FinSequence of D
for F1 being finite set
for E1 being Enumeration of F1
for CE1, CE2 being b₁ * -valued FinSequence st CE1 = (SignGenOp ((f ^ <*d1*>),A,F1)) * E1 & CE2 = (SignGenOp ((f ^ <*d2*>),A,F1)) * E1 holds
for s being FinSequence st s in doms CE1 & not 1 + (len f) in rng s holds
( s in doms CE2 & (App CE1) . s = (App CE2) . s )

proof end;

theorem Th134: :: HILB10_7:134

for k being Nat
for y being object
for s being FinSequence st card (s " {y}) = k holds
ex p being Permutation of (dom s) ex s1 being FinSequence st
( s * p = s1 ^ (k |-> y) & not y in rng s1 )

proof end;

theorem Th135: :: HILB10_7:135

for n being Nat
for D being non empty set
for A, M being BinOp of D
for F being finite set
for f being FinSequence of D st A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is associative & M is commutative & M is having_a_unity & M is_distributive_wrt A & n in dom f holds
for E being Enumeration of F
for D being Subset of (dom E) st ( for i being Nat holds
( i in D iff n in E . i ) ) holds
( ( card D is even implies (M "**" (App ((SignGenOp (f,A,F)) * E))) . ((len E) |-> n) = M "**" ((len E) |-> (f /. n)) ) & ( card D is odd implies (M "**" (App ((SignGenOp (f,A,F)) * E))) . ((len E) |-> n) = (the_inverseOp_wrt A) . (M "**" ((len E) |-> (f /. n))) ) )

proof end;

theorem Th136: :: HILB10_7:136

for D being non empty set
for A, M being BinOp of D
for d1, d2 being Element of D
for F1, F2 being finite set st M is commutative & M is associative & M is having_a_unity & A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is_distributive_wrt A holds
for f being FinSequence of D
for E1 being Enumeration of F1
for E2 being Enumeration of F2
for s1, s2 being FinSequence st s1 in doms ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1) & s2 in doms ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2) & card (s1 " {(1 + (len f))}) = card (s2 " {(1 + (len f))}) holds
M . (((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F2)) * E2))) . s2)) = M . (((M "**" (App ((SignGenOp ((f ^ <*d2*>),A,F1)) * E1))) . s1),((M "**" (App ((SignGenOp ((f ^ <*d1*>),A,F2)) * E2))) . s2))

proof end;

theorem Th137: :: HILB10_7:137

for m being Nat
for D being non empty set
for A, M being BinOp of D
for F1 being finite set st M is commutative & M is associative & M is having_a_unity & A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is_distributive_wrt A holds
for E1 being Enumeration of F1 st union F1 c= Seg (1 + m) & len E1 is even holds
for Ee being Enumeration of Ext (F1,(1 + m),(2 + m))
for Es being Enumeration of swap (F1,(1 + m),(2 + m)) st Ee = Ext (E1,(1 + m),(2 + m)) & Es = Swap (E1,(1 + m),(2 + m)) holds
ex se, ss being Subset of (doms ((m + 2),(card F1))) st
( se c= (len E1) -tuples_on {(1 + m),(2 + m)} & ss c= (len E1) -tuples_on {(1 + m),(2 + m)} & se is with_evenly_repeated_values-member & ss is with_evenly_repeated_values-member & ( for CFe, CFs being non-empty non empty FinSequence of D *
for f being FinSequence of D
for d1, d2 being Element of D st len f = m & CFe = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext (F1,(1 + (len f)),(2 + (len f)))))) * Ee & CFs = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(swap (F1,(1 + (len f)),(2 + (len f)))))) * Es holds
for Se being Element of Fin (dom (App CFe))
for Ss being Element of Fin (dom (App CFs)) st Se = se & Ss = ss holds
A . (((M "**" (App ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * E1))) . ((len E1) |-> (1 + (len f)))),((M "**" (App ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F1)) * E1))) . ((len E1) |-> (1 + (len f))))) = A . ((A $$ (Se,(M "**" (App CFe)))),(A $$ (Ss,(M "**" (App CFs))))) ) )

proof end;

theorem Th138: :: HILB10_7:138

for m being Nat
for D being non empty set
for A, M being BinOp of D
for F being finite set st A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is associative & M is commutative & M is having_a_unity & M is_distributive_wrt A holds
for E being Enumeration of F st union F c= Seg (1 + m) holds
for Ee being Enumeration of Ext (F,(1 + m),(2 + m))
for Es being Enumeration of swap (F,(1 + m),(2 + m)) st Ee = Ext (E,(1 + m),(2 + m)) & Es = Swap (E,(1 + m),(2 + m)) holds
for Ees being Enumeration of (Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m))) st Ees = Ee ^ Es holds
for s1, s2 being FinSequence st s1 in doms ((m + 1),(card F)) & s2 in doms ((m + 1),(card F)) & s1 is with_evenly_repeated_values & s2 is with_evenly_repeated_values & card (s1 " {(1 + m)}) < card (s2 " {(1 + m)}) holds
ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( for CE1, CE2 being FinSequence of D *
for f being FinSequence of D
for d1, d2 being Element of D st len f = m & CE1 = (SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * E & CE2 = (SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E holds
for CFes being non-empty non empty FinSequence of D * st CFes = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + (len f)),(2 + (len f)))) \/ (swap (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & i in dom (s1 ^ s2) holds
( ( (s1 ^ s2) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) & ( (s1 ^ s2) . i <> 1 + (len f) implies h . i = (s1 ^ s2) . i ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & i in dom (s2 ^ s1) holds
( ( (s2 ^ s1) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) & ( (s2 ^ s1) . i <> 1 + (len f) implies h . i = (s2 ^ s1) . i ) ) ) ) ) )

proof end;

theorem Th139: :: HILB10_7:139

for m being Nat
for D being non empty set
for A, M being BinOp of D
for F being finite set st A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is associative & M is commutative & M is having_a_unity & M is_distributive_wrt A holds
for E being Enumeration of F st union F c= Seg (1 + m) holds
for Ee being Enumeration of Ext (F,(1 + m),(2 + m))
for Es being Enumeration of swap (F,(1 + m),(2 + m)) st Ee = Ext (E,(1 + m),(2 + m)) & Es = Swap (E,(1 + m),(2 + m)) holds
for Ees being Enumeration of (Ext (F,(1 + m),(2 + m))) \/ (swap (F,(1 + m),(2 + m))) st Ees = Ee ^ Es holds
for s1, s2 being FinSequence st s1 in doms ((m + 1),(card F)) & s2 in doms ((m + 1),(card F)) & s1 is with_evenly_repeated_values & s2 is with_evenly_repeated_values & s1 <> s2 holds
ex D1, D2 being Subset of (doms ((m + 2),((card F) + (card F)))) st
( D1 is with_evenly_repeated_values-member & D2 is with_evenly_repeated_values-member & ( for CE1, CE2 being FinSequence of D *
for f being FinSequence of D
for d1, d2 being Element of D st len f = m & CE1 = (SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * E & CE2 = (SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F)) * E holds
for CFes being non-empty non empty FinSequence of D * st CFes = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((Ext (F,(1 + (len f)),(2 + (len f)))) \/ (swap (F,(1 + (len f)),(2 + (len f))))))) * Ees holds
for S1, S2 being Element of Fin (dom (App CFes)) st S1 = D1 & S2 = D2 holds
( S1 misses S2 & A . ((M . (((M "**" (App CE1)) . s1),((M "**" (App CE2)) . s2))),(M . (((M "**" (App CE1)) . s2),((M "**" (App CE2)) . s1)))) = A $$ ((S1 \/ S2),(M "**" (App CFes))) & ( for h being FinSequence
for i being Nat st h in S1 & i in dom (s1 ^ s2) holds
( ( (s1 ^ s2) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) & ( (s1 ^ s2) . i <> 1 + (len f) implies h . i = (s1 ^ s2) . i ) ) ) & ( for h being FinSequence
for i being Nat st h in S2 & i in dom (s2 ^ s1) holds
( ( (s2 ^ s1) . i = 1 + (len f) implies h . i in {(1 + (len f)),(2 + (len f))} ) & ( (s2 ^ s1) . i <> 1 + (len f) implies h . i = (s2 ^ s1) . i ) ) ) ) ) )

proof end;

theorem Th140: :: HILB10_7:140

for D being non empty set
for A, M being BinOp of D
for f being FinSequence of D st M is commutative & M is associative & len f = 2 holds
SignGenOp (f,M,A,{2}) = M . ((A . ((f . 1),(f . 2))),(A . ((f . 1),((the_inverseOp_wrt A) . (f . 2)))))

proof end;

theorem Th141: :: HILB10_7:141

for D being non empty set
for A, M being BinOp of D
for f being FinSequence of D st M is commutative & M is associative & A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is_distributive_wrt A holds
for E being Enumeration of bool {2}
for CE being non-empty non empty FinSequence of D * st CE = (SignGenOp (f,A,(bool {2}))) * E & len f = 2 holds
ex S being Element of Fin (dom (App CE)) st
( S = {<*1,1*>,<*2,2*>} & SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE))) )

proof end;

theorem :: HILB10_7:142

for D being non empty set
for A, M being BinOp of D
for f being FinSequence of D st M is commutative & M is associative & A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is_distributive_wrt A holds
for E being Enumeration of bool {2}
for CE being non-empty non empty FinSequence of D * st CE = (SignGenOp (f,A,(bool {2}))) * E & len f = 2 holds
ex S being Element of Fin (dom (App CE)) st
( S is with_evenly_repeated_values-member & SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE))) )

proof end;

::

WP:

theorem :: HILB10_7:143

for m being Nat
for D being non empty set
for A, M being BinOp of D st A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is associative & M is commutative & M is having_a_unity & M is_distributive_wrt A & m > 1 & ( for d being Element of D holds M . ((the_unity_wrt A),d) = the_unity_wrt A ) holds
ex E being Enumeration of bool ((Seg m) \ {1}) ex S being Subset of (doms (m,(card (bool ((Seg m) \ {1}))))) st
( S is with_evenly_repeated_values-member & (card (bool ((Seg m) \ {1}))) |-> 1 in S & ( for CE being non-empty non empty FinSequence of D *
for f being FinSequence of D st CE = (SignGenOp (f,A,(bool ((Seg m) \ {1})))) * E & len f = m holds
for Sce being Element of Fin (dom (App CE)) st Sce = S holds
SignGenOp (f,M,A,((Seg m) \ {1})) = A $$ (Sce,(M "**" (App CE))) ) )

proof end;