let L be non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis:
let n be Nat; :: thesis:
let f be FinSequence of L; :: thesis:
let xf be Function of n,L; :: thesis:
assume A1: xf = FS2XFS f ; :: thesis:
set M = the multF of L;
set A = the addF of L;
defpred S₁[ Nat] means for F being finite set st card F = $1 holds
for E being Enumeration of F
for d being FinSequence st d in doms ((SignGenOp (f, the addF of L,F)) * E) holds
the multF of L "**" ((App ((SignGenOp (f, the addF of L,F)) * E)) . d) = eval ((Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,n)))),xf);
A2: S₁[ 0 ]

proof

let F be finite set ; :: thesis:
assume A3: card F = 0 ; :: thesis:
let E be Enumeration of F; :: thesis:
let d be FinSequence; :: thesis:
assume A4: d in doms ((SignGenOp (f, the addF of L,F)) * E) ; :: thesis:
( len d = len ((SignGenOp (f, the addF of L,F)) * E) & len ((SignGenOp (f, the addF of L,F)) * E) = len E & len E = card F ) by A4, HILB10_7:47, CARD_1:def 7;
then A5: ( d = {} & (SignGenOp (f, the addF of L,F)) * E = {} ) by A3;
then A6: the multF of L "**" ((App ((SignGenOp (f, the addF of L,F)) * E)) . d) = the_unity_wrt the multF of L by FINSOP_1:def 1, HILB10_7:59
.= 1_ L by GROUP_1:22 ;
A7: SgnMembershipNumber (d,L,E) = 1. L by A5, Th56;
count_reps (d,n) = EmptyBag n by A5, Th54;
then eval ((count_reps (d,n)),xf) = 1. L by POLYNOM2:14;
then eval ((Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,n)))),xf) = (1. L) * (1. L) by A7, POLYNOM7:13
.= 1. L ;
hence the multF of L "**" ((App ((SignGenOp (f, the addF of L,F)) * E)) . d) = eval ((Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,n)))),xf) by A6; :: thesis:

end;

A8: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis:
assume A9: S₁[i] ; :: thesis:
let F be finite set ; :: thesis:
assume A10: card F = i + 1 ; :: thesis:
let E be Enumeration of F; :: thesis:
let d be FinSequence; :: thesis:
assume A11: d in doms ((SignGenOp (f, the addF of L,F)) * E) ; :: thesis:
A12: ( len d = len ((SignGenOp (f, the addF of L,F)) * E) & len ((SignGenOp (f, the addF of L,F)) * E) = len E & len E = card F ) by A11, HILB10_7:47, CARD_1:def 7;
set EE = {(E . (len E))};
set Fi = F \ {(E . (len E))};
reconsider Ei = E | i as Enumeration of F \ {(E . (len E))} by A12, A10, HILB10_7:96;
reconsider Ee = <*(E . (len E))*> as Enumeration of {(E . (len E))} by A12, A10, HILB10_7:96;
set di = d | i;
set D = <*(d . (i + 1))*>;
A13: ( len (d | i) = i & len Ei = i ) by A12, A10, NAT_1:11, FINSEQ_1:59;
A14: d = (d | i) ^ <*(d . (i + 1))*> by A10, A12, FINSEQ_3:55;
A15: len ((SignGenOp (f, the addF of L,(F \ {(E . (len E))}))) * Ei) = len Ei by CARD_1:def 7;
A16: F = (F \ {(E . (len E))}) \/ {(E . (len E))} by A12, A10, HILB10_7:96;
A17: E = Ei ^ Ee by A10, A12, FINSEQ_3:55;
then A18: (SignGenOp (f, the addF of L,F)) * E = ((SignGenOp (f, the addF of L,(F \ {(E . (len E))}))) * Ei) ^ ((SignGenOp (f, the addF of L,{(E . (len E))})) * Ee) by A16, HILB10_7:81;
then A19: ( d | i in doms ((SignGenOp (f, the addF of L,(F \ {(E . (len E))}))) * Ei) & <*(d . (i + 1))*> in doms ((SignGenOp (f, the addF of L,{(E . (len E))})) * Ee) ) by A11, A15, A13, A14, HILB10_7:50;
then (App ((SignGenOp (f, the addF of L,F)) * E)) . d = ((App ((SignGenOp (f, the addF of L,(F \ {(E . (len E))}))) * Ei)) . (d | i)) ^ ((App ((SignGenOp (f, the addF of L,{(E . (len E))})) * Ee)) . <*(d . (i + 1))*>) by HILB10_7:61, A14, A18;
then A20: the multF of L "**" ((App ((SignGenOp (f, the addF of L,F)) * E)) . d) = the multF of L . (( the multF of L "**" ((App ((SignGenOp (f, the addF of L,(F \ {(E . (len E))}))) * Ei)) . (d | i))),( the multF of L "**" ((App ((SignGenOp (f, the addF of L,{(E . (len E))})) * Ee)) . <*(d . (i + 1))*>))) by FINSOP_1:5;
A21: (SignGenOp (f, the addF of L,{(E . (len E))})) * Ee = <*(SignGen (f, the addF of L,(E . (len E))))*> by HILB10_7:78;
then A22: <*(d . (i + 1))*> . 1 in dom (SignGen (f, the addF of L,(E . (len E)))) by A19, HILB10_7:51;
then A23: (SignGen (f, the addF of L,(E . (len E)))) . (d . (i + 1)) in rng (SignGen (f, the addF of L,(E . (len E)))) by FUNCT_1:def 3;
A24: rng (SignGen (f, the addF of L,(E . (len E)))) c= the carrier of L by FINSEQ_1:def 4;
(App ((SignGenOp (f, the addF of L,{(E . (len E))})) * Ee)) . <*(d . (i + 1))*> = <*((SignGen (f, the addF of L,(E . (len E)))) . (d . (i + 1)))*> by A21, A22, HILB10_7:60;
then A25: the multF of L "**" ((App ((SignGenOp (f, the addF of L,{(E . (len E))})) * Ee)) . <*(d . (i + 1))*>) = (SignGen (f, the addF of L,(E . (len E)))) . (d . (i + 1)) by A24, A23, FINSOP_1:11;
A26: card (F \ {(E . (len E))}) = i by A13, CARD_1:def 7;
1 <= 1 + i by NAT_1:11;
then A27: ( i + 1 in dom d & i + 1 in dom E ) by A10, A12, FINSEQ_3:25;
then A28: d . (i + 1) in dom (((SignGenOp (f, the addF of L,F)) * E) . (i + 1)) by HILB10_7:47, A11;
then d . (i + 1) in dom (SignGen (f, the addF of L,(E . (i + 1)))) by HILB10_7:80, A27;
then A29: d . (i + 1) in dom f by HILB10_7:def 11;
reconsider dd = d . (i + 1) as Nat by A11;
1 <= dd by A28, FINSEQ_3:25;
then reconsider dd1 = dd - 1 as Nat ;
len (FS2XFS f) = n by A1, FUNCT_2:def 1;
then A30: n = len f by AFINSQ_1:def 8;
then A31: dd1 + 1 <= n by A29, FINSEQ_3:25;
then dd1 < n by NAT_1:13;
then A32: dd1 in Segm n by NAT_1:44;
A33: ( f . dd in rng f & rng f c= the carrier of L ) by FINSEQ_1:def 4, A29, FUNCT_1:def 3;
then reconsider fdd = f . dd as Element of L ;
A34: f . (dd1 + 1) = xf . dd1 by A1, A31, NAT_1:13, A30, AFINSQ_1:def 8;
A35: dd1 + 1 = dd ;
A36: count_reps (d,n) = (count_reps ((d | i),n)) + ((EmptyBag n) +* (dd1,1)) by A14, A35, Th55;
A37: eval (((EmptyBag n) +* (dd1,1)),xf) = (power L) . ((xf . dd1),1) by A32, Th14
.= xf . dd1 by A33, A34, GROUP_1:50 ;
A38: the multF of L "**" ((App ((SignGenOp (f, the addF of L,F)) * E)) . d) = the multF of L . ((eval ((Monom ((SgnMembershipNumber ((d | i),L,Ei)),(count_reps ((d | i),n)))),xf)),((SignGen (f, the addF of L,(E . (len E)))) . dd)) by A26, A25, A20, A9, A19
.= the multF of L . (((SgnMembershipNumber ((d | i),L,Ei)) * (eval ((count_reps ((d | i),n)),xf))),((SignGen (f, the addF of L,(E . (len E)))) . dd)) by POLYNOM7:13 ;

per cases ;

suppose A39: dd in E . (len E) ; :: thesis:

dd in dom (SignGen (f, the addF of L,(E . (len E)))) by A29, HILB10_7:def 11;
then (SignGen (f, the addF of L,(E . (len E)))) . dd = (the_inverseOp_wrt the addF of L) . fdd by A39, HILB10_7:def 11
.= (comp L) . fdd by FVSUM_1:15
.= - fdd by VECTSP_1:def 13 ;
hence the multF of L "**" ((App ((SignGenOp (f, the addF of L,F)) * E)) . d) = ((SgnMembershipNumber ((d | i),L,Ei)) * (eval ((count_reps ((d | i),n)),xf))) * (- fdd) by A38
.= (SgnMembershipNumber ((d | i),L,Ei)) * ((eval ((count_reps ((d | i),n)),xf)) * (- fdd)) by GROUP_1:def 3
.= (SgnMembershipNumber ((d | i),L,Ei)) * (- ((eval ((count_reps ((d | i),n)),xf)) * fdd)) by VECTSP_1:8
.= (SgnMembershipNumber ((d | i),L,Ei)) * (- (eval ((count_reps (d,n)),xf))) by A36, POLYNOM2:16, A37, A34
.= - ((SgnMembershipNumber ((d | i),L,Ei)) * (eval ((count_reps (d,n)),xf))) by VECTSP_1:8
.= (- (SgnMembershipNumber ((d | i),L,Ei))) * (eval ((count_reps (d,n)),xf)) by VECTSP_1:8
.= (SgnMembershipNumber (d,L,E)) * (eval ((count_reps (d,n)),xf)) by A13, A39, Th58, A14, A17
.= eval ((Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,n)))),xf) by POLYNOM7:13 ;
:: thesis:

end;

suppose A40: not dd in E . (len E) ; :: thesis:

dd in dom (SignGen (f, the addF of L,(E . (len E)))) by A29, HILB10_7:def 11;
hence the multF of L "**" ((App ((SignGenOp (f, the addF of L,F)) * E)) . d) = ((SgnMembershipNumber ((d | i),L,Ei)) * (eval ((count_reps ((d | i),n)),xf))) * fdd by A38, A40, HILB10_7:def 11
.= (SgnMembershipNumber ((d | i),L,Ei)) * ((eval ((count_reps ((d | i),n)),xf)) * fdd) by GROUP_1:def 3
.= (SgnMembershipNumber ((d | i),L,Ei)) * (eval ((count_reps (d,n)),xf)) by A36, POLYNOM2:16, A37, A34
.= (SgnMembershipNumber (d,L,E)) * (eval ((count_reps (d,n)),xf)) by A13, A40, Th57, A14, A17
.= eval ((Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,n)))),xf) by POLYNOM7:13 ;
:: thesis:

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A8);
hence for F being finite set
for E being Enumeration of F
for d being FinSequence st d in doms ((SignGenOp (f, the addF of L,F)) * E) holds
the multF of L "**" ((App ((SignGenOp (f, the addF of L,F)) * E)) . d) = eval ((Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,n)))),xf) ; :: thesis: