reconsider mm = m as non trivial Nat by A1, NEWTON03:def 1;
set A = the addF of L;
set M = the multF of L;
A2: the addF of L is having_a_unity by FVSUM_1:8;
A3: comp L is_an_inverseOp_wrt the addF of L by PRVECT_1:2;
A4: the multF of L is_distributive_wrt the addF of L by FVSUM_1:10;
A5: the_unity_wrt the addF of L = 0. L by FVSUM_1:7;
A6: for d being Element of L holds the multF of L . ((the_unity_wrt the addF of L),d) = the_unity_wrt the addF of L

let d be Element of L; :: thesis:
thus the multF of L . ((the_unity_wrt the addF of L),d) = (0. L) * d by FVSUM_1:7
.= the_unity_wrt the addF of L by FVSUM_1:7 ; :: thesis:

end;

set F = bool ((Seg mm) \ {1});
set D = doms (mm,(card (bool ((Seg mm) \ {1}))));
consider E being Enumeration of bool ((Seg mm) \ {1}), S being Subset of (doms (mm,(card (bool ((Seg mm) \ {1}))))) such that
A7: S is with_evenly_repeated_values-member and
A8: (card (bool ((Seg mm) \ {1}))) |-> 1 in S and
A9: for CE being non-empty non empty FinSequence of the carrier of L *
for f being FinSequence of the carrier of L st CE = (SignGenOp (f, the addF of L,(bool ((Seg mm) \ {1})))) * E & len f = m holds
for Sce being Element of Fin (dom (App CE)) st Sce = S holds
SignGenOp (f, the multF of L, the addF of L,((Seg m) \ {1})) = the addF of L $$ (Sce,( the multF of L "**" (App CE))) by A2, FINSEQOP:def 2, A3, A4, A1, A6, HILB10_7:143;
defpred S₁[ set ] means ( $1 c= S implies ex P being Polynomial of m,L st
( ( (card (bool ((Seg mm) \ {1}))) |-> 1 in $1 implies P . ((EmptyBag m) +* (0,(2 |^ (m -' 1)))) = 1. L ) & ( for b being bag of m st b in Support P holds
( degree b = 2 |^ (m -' 1) & ex i being Integer st P . b = i '*' (1_ L) & ( for n being Nat st b . n = 2 |^ (m -' 1) holds
( ( P . b = 1. L or P . b = - (1. L) ) & (2 |^ (m -' 1)) |-> (n + 1) in $1 ) ) & ( for n being Nat holds b . n is even ) ) ) & ( for f being FinSequence of L
for xf being Function of m,L st xf = FS2XFS f holds
for CE being non-empty non empty FinSequence of the carrier of L * st CE = (SignGenOp (f, the addF of L,(bool ((Seg mm) \ {1})))) * E holds
for Sce being Element of Fin (dom (App CE)) st Sce = $1 holds
eval (P,xf) = the addF of L $$ (Sce,( the multF of L "**" (App CE))) ) ) );
A10: S₁[ {}. (doms (mm,(card (bool ((Seg mm) \ {1})))))]

proof

assume {}. (doms (mm,(card (bool ((Seg mm) \ {1}))))) c= S ; :: thesis:
take P = 0_ (m,L); :: thesis:
thus ( (card (bool ((Seg mm) \ {1}))) |-> 1 in {}. (doms (mm,(card (bool ((Seg mm) \ {1}))))) implies P . ((EmptyBag m) +* (0,(2 |^ (m -' 1)))) = 1. L ) ; :: thesis:
Support P = {}

proof

assume Support P <> {} ; :: thesis:
then consider b being object such that
A11: b in Support P by XBOOLE_0:def 1;
( b in dom P & P . b <> 0. L ) by A11, POLYNOM1:def 3;
hence contradiction by POLYNOM1:22; :: thesis:

end;

hence for b being bag of m st b in Support P holds
( degree b = 2 |^ (m -' 1) & ex i being Integer st P . b = i '*' (1_ L) & ( for n being Nat st b . n = 2 |^ (m -' 1) holds
( ( P . b = 1. L or P . b = - (1. L) ) & (2 |^ (m -' 1)) |-> (n + 1) in {}. (doms (mm,(card (bool ((Seg mm) \ {1}))))) ) ) & ( for n being Nat holds b . n is even ) ) ; :: thesis:
let f be FinSequence of L; :: thesis:
let xf be Function of m,L; :: thesis:
assume xf = FS2XFS f ; :: thesis:
let CE be non-empty non empty FinSequence of the carrier of L * ; :: thesis:
assume CE = (SignGenOp (f, the addF of L,(bool ((Seg mm) \ {1})))) * E ; :: thesis:
let Sce be Element of Fin (dom (App CE)); :: thesis:
assume A12: Sce = {}. (doms (mm,(card (bool ((Seg mm) \ {1}))))) ; :: thesis:
thus eval (P,xf) = 0. L by POLYNOM2:20
.= the addF of L $$ (({}. (dom (App CE))),( the multF of L "**" (App CE))) by A5, SETWISEO:31, FVSUM_1:8
.= the addF of L $$ (Sce,( the multF of L "**" (App CE))) by A12 ; :: thesis:

end;

A13: for B9 being Element of Fin (doms (mm,(card (bool ((Seg mm) \ {1})))))
for b being Element of doms (mm,(card (bool ((Seg mm) \ {1})))) st S₁[B9] & not b in B9 holds
S₁[B9 \/ {b}]

proof

let X be Element of Fin (doms (mm,(card (bool ((Seg mm) \ {1}))))); :: thesis:
let d be Element of doms (mm,(card (bool ((Seg mm) \ {1})))); :: thesis:
assume A14: ( S₁[X] & not d in X & X \/ {d} c= S ) ; :: thesis:
X c= X \/ {d} by XBOOLE_1:7;
then X c= S by A14;
then consider P being Polynomial of m,L such that
A15: ( (card (bool ((Seg mm) \ {1}))) |-> 1 in X implies P . ((EmptyBag m) +* (0,(2 |^ (m -' 1)))) = 1. L ) and
A16: for b being bag of m st b in Support P holds
( degree b = 2 |^ (m -' 1) & ex i being Integer st P . b = i '*' (1_ L) & ( for n being Nat st b . n = 2 |^ (m -' 1) holds
( ( P . b = 1. L or P . b = - (1. L) ) & (2 |^ (m -' 1)) |-> (n + 1) in X ) ) & ( for n being Nat holds b . n is even ) ) and
A17: for f being FinSequence of L
for xf being Function of m,L st xf = FS2XFS f holds
for CE being non-empty non empty FinSequence of the carrier of L * st CE = (SignGenOp (f, the addF of L,(bool ((Seg mm) \ {1})))) * E holds
for Sce being Element of Fin (dom (App CE)) st Sce = X holds
eval (P,xf) = the addF of L $$ (Sce,( the multF of L "**" (App CE))) by A14;
set s = count_reps (d,m);
set Q = Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,m)));
A18: d in X \/ {d} by ZFMISC_1:136;
A19: d is Element of (card (bool ((Seg mm) \ {1}))) -tuples_on (Seg m) by HILB10_7:def 14;
A20: len d = card (bool ((Seg mm) \ {1})) by CARD_1:def 7;
then A21: len d = 2 |^ (m -' 1) by Th4;
take PQ = P + (Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,m)))); :: thesis:
thus ( (card (bool ((Seg mm) \ {1}))) |-> 1 in X \/ {d} implies PQ . ((EmptyBag m) +* (0,(2 |^ (m -' 1)))) = 1. L ) :: thesis:

proof

set Em = EmptyBag m;
set EM = (EmptyBag m) +* (0,(2 |^ (m -' 1)));
0 < mm ;
then A22: 0 in Segm m by NAT_1:44;
assume (card (bool ((Seg mm) \ {1}))) |-> 1 in X \/ {d} ; :: thesis:

per cases ) |-> 1 in X or (card (bool ((Seg mm) \ {1}))) |-> 1 = d ) by ZFMISC_1:136;

suppose A23: (card (bool ((Seg mm) \ {1}))) |-> 1 in X ; :: thesis:

A24: (EmptyBag m) +* (0,(2 |^ (m -' 1))) <> count_reps (d,m)

proof

assume (EmptyBag m) +* (0,(2 |^ (m -' 1))) = count_reps (d,m) ; :: thesis:
then d = (len d) |-> (0 + 1) by A21, A22, A19, Th63;
hence contradiction by A14, A23, CARD_1:def 7; :: thesis:

end;

(Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,m)))) . ((EmptyBag m) +* (0,(2 |^ (m -' 1)))) = (0_ (m,L)) . ((EmptyBag m) +* (0,(2 |^ (m -' 1)))) by A24, FUNCT_7:32
.= 0. L by POLYNOM1:22 ;
then PQ . ((EmptyBag m) +* (0,(2 |^ (m -' 1)))) = (P . ((EmptyBag m) +* (0,(2 |^ (m -' 1))))) + (0. L) by POLYNOM1:15
.= P . ((EmptyBag m) +* (0,(2 |^ (m -' 1)))) ;
hence PQ . ((EmptyBag m) +* (0,(2 |^ (m -' 1)))) = 1. L by A23, A15; :: thesis:

end;

suppose A25: (card (bool ((Seg mm) \ {1}))) |-> 1 = d ; :: thesis:

then (len d) |-> (1 + 0) = d ;
then count_reps (d,m) = (EmptyBag m) +* (0,(len d)) by A22, Th64;
then A26: count_reps (d,m) = (EmptyBag m) +* (0,(2 |^ (m -' 1))) by A20, Th4;
A27: ( dom PQ = Bags m & Bags m = dom P & (EmptyBag m) +* (0,(2 |^ (m -' 1))) in Bags m ) by FUNCT_2:def 1, PRE_POLY:def 12;
A28: not (EmptyBag m) +* (0,(2 |^ (m -' 1))) in Support P

proof

dom (EmptyBag m) = m by PARTFUN1:def 2;
then A29: ((EmptyBag m) +* (0,(2 |^ (m -' 1)))) . 0 = 2 |^ (m -' 1) by A22, FUNCT_7:31;
assume (EmptyBag m) +* (0,(2 |^ (m -' 1))) in Support P ; :: thesis:
then (2 |^ (m -' 1)) |-> (0 + 1) in X by A29, A16;
hence contradiction by A25, A14, Th4; :: thesis:

end;

dom (0_ (m,L)) = Bags m by FUNCT_2:def 1;
then A30: count_reps (d,m) in dom (0_ (m,L)) by PRE_POLY:def 12;
A31: (Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,m)))) . (count_reps (d,m)) = SgnMembershipNumber (d,L,E) by A30, FUNCT_7:31;
A32: PQ . ((EmptyBag m) +* (0,(2 |^ (m -' 1)))) = (P . ((EmptyBag m) +* (0,(2 |^ (m -' 1))))) + ((Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,m)))) . ((EmptyBag m) +* (0,(2 |^ (m -' 1))))) by POLYNOM1:15
.= (0. L) + ((Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,m)))) . ((EmptyBag m) +* (0,(2 |^ (m -' 1))))) by A28, A27, POLYNOM1:def 4
.= (Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,m)))) . ((EmptyBag m) +* (0,(2 |^ (m -' 1)))) ;
set X = { x where x is Element of dom d : ( x in dom d & d . x in E . x ) } ;
{ x where x is Element of dom d : ( x in dom d & d . x in E . x ) } = {}

proof

assume { x where x is Element of dom d : ( x in dom d & d . x in E . x ) } <> {} ; :: thesis:
then consider a being object such that
A33: a in { x where x is Element of dom d : ( x in dom d & d . x in E . x ) } by XBOOLE_0:def 1;
consider x being Element of dom d such that
A34: ( a = x & x in dom d & d . x in E . x ) by A33;
reconsider x = x as Nat ;
len E = card (bool ((Seg mm) \ {1})) by CARD_1:def 7;
then dom E = dom d by A20, FINSEQ_3:29;
then ( E . x in rng E & rng E = bool ((Seg mm) \ {1}) ) by FUNCT_1:def 3, RLAFFIN3:def 1;
hence contradiction by ZFMISC_1:56, A34, A25; :: thesis:

end;

then ( card { x where x is Element of dom d : ( x in dom d & d . x in E . x ) } = 0 & 0 is even ) ;
hence PQ . ((EmptyBag m) +* (0,(2 |^ (m -' 1)))) = 1. L by A31, A26, A32, Def9; :: thesis:

end;

thus for b being bag of m st b in Support PQ holds
( degree b = 2 |^ (m -' 1) & ex i being Integer st PQ . b = i '*' (1_ L) & ( for n being Nat st b . n = 2 |^ (m -' 1) holds
( ( PQ . b = 1. L or PQ . b = - (1. L) ) & (2 |^ (m -' 1)) |-> (n + 1) in X \/ {d} ) ) & ( for n being Nat holds b . n is even ) ) :: thesis:

proof

let b be bag of m; :: thesis:
assume A35: b in Support PQ ; :: thesis:
dom P = Bags m by FUNCT_2:def 1;
then A36: b in dom P by PRE_POLY:def 12;

per cases ;

suppose A37: b in Support P ; :: thesis:

hence degree b = 2 |^ (m -' 1) by A16; :: thesis:
consider i being Integer such that
A38: P . b = i '*' (1_ L) by A37, A16;
thus ex i being Integer st PQ . b = i '*' (1_ L) :: thesis:

proof

per cases ;

suppose A39: b <> count_reps (d,m) ; :: thesis:

(Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,m)))) . b = (0_ (m,L)) . b by A39, FUNCT_7:32
.= 0. L by POLYNOM1:22 ;
then PQ . b = (P . b) + (0. L) by POLYNOM1:15
.= P . b ;
hence ex i being Integer st PQ . b = i '*' (1_ L) by A38; :: thesis:

end;

suppose A40: b = count_reps (d,m) ; :: thesis:

dom (0_ (m,L)) = Bags m by FUNCT_2:def 1;
then A41: b in dom (0_ (m,L)) by PRE_POLY:def 12;
A42: (Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,m)))) . b = SgnMembershipNumber (d,L,E) by A41, A40, FUNCT_7:31;
( SgnMembershipNumber (d,L,E) = 1. L or SgnMembershipNumber (d,L,E) = - (1. L) ) by Th62;
then ( SgnMembershipNumber (d,L,E) = 1 '*' (1. L) or SgnMembershipNumber (d,L,E) = (- 1) '*' (1. L) ) by RING_3:60, RING_3:61;
then ( PQ . b = (i '*' (1_ L)) + (1 '*' (1. L)) or PQ . b = (i '*' (1_ L)) + ((- 1) '*' (1. L)) ) by A38, A42, POLYNOM1:15;
then ( PQ . b = (i + 1) '*' (1_ L) or PQ . b = (i + (- 1)) '*' (1_ L) ) by RING_3:62;
hence ex i being Integer st PQ . b = i '*' (1_ L) ; :: thesis:

end;

thus for n being Nat st b . n = 2 |^ (m -' 1) holds
( ( PQ . b = 1. L or PQ . b = - (1. L) ) & (2 |^ (m -' 1)) |-> (n + 1) in X \/ {d} ) :: thesis:

proof

let n be Nat; :: thesis:
assume A43: b . n = 2 |^ (m -' 1) ; :: thesis:
A44: ( n in dom b & dom b = m ) by A43, FUNCT_1:def 2, PARTFUN1:def 2;
A45: (2 |^ (m -' 1)) |-> (n + 1) in X by A16, A37, A43;
b <> count_reps (d,m)

proof

assume A46: b = count_reps (d,m) ; :: thesis:
b . n = degree b by A37, A16, A43;
then count_reps (d,m) = (EmptyBag m) +* (n,(len d)) by A21, A43, A46, Th19;
hence contradiction by A21, A14, A45, A19, A44, Th63; :: thesis:

end;

then (Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,m)))) . b = (0_ (m,L)) . b by FUNCT_7:32
.= 0. L by POLYNOM1:22 ;
then PQ . b = (P . b) + (0. L) by POLYNOM1:15
.= P . b ;
hence ( ( PQ . b = 1. L or PQ . b = - (1. L) ) & (2 |^ (m -' 1)) |-> (n + 1) in X \/ {d} ) by A45, ZFMISC_1:136, A16, A37, A43; :: thesis:

end;

thus for n being Nat holds b . n is even by A37, A16; :: thesis:

end;

suppose A47: not b in Support P ; :: thesis:

proof

let n be Nat; :: thesis:
assume A57: b . n = 2 |^ (m -' 1) ; :: thesis:
A58: ( n in dom b & dom b = m ) by A57, FUNCT_1:def 2, PARTFUN1:def 2;
count_reps (d,m) = (EmptyBag m) +* (n,(len d)) by A57, A54, A21, A53, Th19;
then d = (len d) |-> (n + 1) by A19, A58, Th63;
hence ( ( PQ . b = 1. L or PQ . b = - (1. L) ) & (2 |^ (m -' 1)) |-> (n + 1) in X \/ {d} ) by A21, A55, A56, Th62, ZFMISC_1:136; :: thesis:

end;

thus for n being Nat holds b . n is even by A18, A14, A7, Th60, A53; :: thesis:

end;

let f be FinSequence of L; :: thesis:
let xf be Function of m,L; :: thesis:
assume A59: xf = FS2XFS f ; :: thesis:
let CE be non-empty non empty FinSequence of the carrier of L * ; :: thesis:
assume A60: CE = (SignGenOp (f, the addF of L,(bool ((Seg mm) \ {1})))) * E ; :: thesis:
let Sce be Element of Fin (dom (App CE)); :: thesis:
assume A61: Sce = X \/ {d} ; :: thesis:
dom xf = m by FUNCT_2:def 1;
then A62: len f = m by A59, AFINSQ_1:def 8;
A63: doms CE = doms (mm,(card (bool ((Seg mm) \ {1})))) by HILB10_7:106, A60, A62;
then d in doms CE ;
then A64: d in dom (App CE) by HILB10_7:def 9;
A65: eval ((Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,m)))),xf) = the multF of L "**" ((App CE) . d) by A63, A60, A59, Th59
.= ( the multF of L "**" (App CE)) . d by HILB10_7:def 10, A64 ;
reconsider X1 = X as Element of Fin (dom (App CE)) by A63, HILB10_7:def 9;
reconsider dd = d as Element of dom (App CE) by A63, HILB10_7:def 9;
thus the addF of L $$ (Sce,( the multF of L "**" (App CE))) = the addF of L . (( the addF of L $$ (X1,( the multF of L "**" (App CE)))),(( the multF of L "**" (App CE)) . dd)) by SETWOP_2:2, FVSUM_1:8, A14, A61
.= (eval (P,xf)) + (eval ((Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,m)))),xf)) by A65, A17, A59, A60
.= eval (PQ,xf) by POLYNOM2:23 ; :: thesis:

end;

A66: for B being Element of Fin (doms (mm,(card (bool ((Seg mm) \ {1}))))) holds S₁[B] from SETWISEO:sch 2(A10, A13);
S is Element of Fin (doms (mm,(card (bool ((Seg mm) \ {1}))))) by FINSUB_1:def 5;
then consider P being Polynomial of m,L such that
A67: ( (card (bool ((Seg mm) \ {1}))) |-> 1 in S implies P . ((EmptyBag m) +* (0,(2 |^ (m -' 1)))) = 1. L ) and
A68: for b being bag of m st b in Support P holds
( degree b = 2 |^ (m -' 1) & ex i being Integer st P . b = i '*' (1_ L) & ( for n being Nat st b . n = 2 |^ (m -' 1) holds
( ( P . b = 1. L or P . b = - (1. L) ) & (2 |^ (m -' 1)) |-> (n + 1) in S ) ) & ( for n being Nat holds b . n is even ) ) and
A69: for f being FinSequence of L
for xf being Function of m,L st xf = FS2XFS f holds
for CE being non-empty non empty FinSequence of the carrier of L * st CE = (SignGenOp (f, the addF of L,(bool ((Seg mm) \ {1})))) * E holds
for Sce being Element of Fin (dom (App CE)) st Sce = S holds
eval (P,xf) = the addF of L $$ (Sce,( the multF of L "**" (App CE))) by A66;
take P ; :: thesis:
thus P . ((EmptyBag m) +* (0,(2 |^ (m -' 1)))) = 1. L by A8, A67; :: thesis:
thus for b being bag of m st b in Support P holds
( degree b = 2 |^ (m -' 1) & ex i being Integer st P . b = i '*' (1_ L) & ( not 2 |^ (m -' 1) in rng b or P . b = 1. L or P . b = - (1. L) ) & ( for n being Nat holds b . n is even ) ) :: thesis:

proof

let b be bag of m; :: thesis:
assume A70: b in Support P ; :: thesis:
( not 2 |^ (m -' 1) in rng b or P . b = 1. L or P . b = - (1. L) )

proof

assume 2 |^ (m -' 1) in rng b ; :: thesis:
then consider n being object such that
A71: ( n in dom b & b . n = 2 |^ (m -' 1) ) by FUNCT_1:def 3;
dom b = Segm m by PARTFUN1:def 2;
hence ( P . b = 1. L or P . b = - (1. L) ) by A70, A68, A71; :: thesis:

end;

hence ( degree b = 2 |^ (m -' 1) & ex i being Integer st P . b = i '*' (1_ L) & ( not 2 |^ (m -' 1) in rng b or P . b = 1. L or P . b = - (1. L) ) & ( for n being Nat holds b . n is even ) ) by A70, A68; :: thesis:

end;

let f be FinSequence of L; :: thesis:
let xf be Function of m,L; :: thesis:
assume A72: xf = FS2XFS f ; :: thesis:
set CE = (SignGenOp (f, the addF of L,(bool ((Seg mm) \ {1})))) * E;
len (FS2XFS f) = m by A72, FUNCT_2:def 1;
then A73: len f = m by AFINSQ_1:def 8;
A74: for x being object st x in dom ((SignGenOp (f, the addF of L,(bool ((Seg mm) \ {1})))) * E) holds
not ((SignGenOp (f, the addF of L,(bool ((Seg mm) \ {1})))) * E) . x is empty

proof

let x be object ; :: thesis:
assume x in dom ((SignGenOp (f, the addF of L,(bool ((Seg mm) \ {1})))) * E) ; :: thesis:
then ((SignGenOp (f, the addF of L,(bool ((Seg mm) \ {1})))) * E) . x = SignGen (f, the addF of L,(E . x)) by HILB10_7:80;
hence not ((SignGenOp (f, the addF of L,(bool ((Seg mm) \ {1})))) * E) . x is empty by A73; :: thesis:

end;

reconsider CE = (SignGenOp (f, the addF of L,(bool ((Seg mm) \ {1})))) * E as non-empty non empty FinSequence of the carrier of L * by A74, FUNCT_1:def 9;
doms CE = doms (mm,(card (bool ((Seg mm) \ {1})))) by A73, HILB10_7:106;
then S c= doms CE ;
then S c= dom (App CE) by HILB10_7:def 9;
then reconsider Sce = S as Element of Fin (dom (App CE)) by FINSUB_1:def 5;
SignGenOp (f, the multF of L, the addF of L,((Seg m) \ {1})) = the addF of L $$ (Sce,( the multF of L "**" (App CE))) by A9, A73;
hence eval (P,xf) = SignGenOp (f, the multF of L, the addF of L,((Seg m) \ {1})) by A72, A69; :: thesis: