let D be non empty set ; :: thesis: 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}))))
let A, M be BinOp of D; :: thesis: 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}))))
let d1, d2 be Element of D; :: thesis: 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}))))
let f be FinSequence of D; :: thesis: ( 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 implies 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})))) )
set I = the_inverseOp_wrt A;
assume that
A1: ( A is having_a_unity & A is associative & A is commutative & A is having_an_inverseOp ) and
A2: ( M is commutative & M is associative ) and
A3: len f <> 0 ; :: thesis: 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}))))
set S = (Seg (len f)) \ {1};
set F = bool ((Seg (len f)) \ {1});
set F1 = UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}));
set F2 = UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1),((len f) + 2)}));
1 <> 1 + (len f) by A3;
then A4: {(1 + (len f))} \ {1} = {(1 + (len f))} by ZFMISC_1:14;
1 <> (1 + (len f)) + 1 by A3;
then A5: {(2 + (len f))} \ {1} = {(2 + (len f))} by ZFMISC_1:14;
Seg ((len f) + 1) = (Seg (len f)) \/ {(1 + (len f))} by FINSEQ_1:9;
then A6: (Seg (1 + (len f))) \ {1} = ((Seg (len f)) \ {1}) \/ {(1 + (len f))} by A4, XBOOLE_1:42;
then A7: bool ((Seg (1 + (len f))) \ {1}) = UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)})) by Th6;
union (bool ((Seg (len f)) \ {1})) = (Seg (len f)) \ {1} by ZFMISC_1:81;
then union (bool ((Seg (len f)) \ {1})) c= Seg (len f) by XBOOLE_1:36;
then union (bool ((Seg (len f)) \ {1})) c= dom f by FINSEQ_1:def 3;
then consider E1, E2 being Enumeration of UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)})), E being Enumeration of UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1),((len f) + 2)})) such that
A8: A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1),((len f) + 2)}))))) * E) = (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E2)) by Th117, A1;
set f1 = A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E1);
set f2 = A "**" ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E2);
rng (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E1)) c= D ;
then reconsider G1 = A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E1) as Function of (dom (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E1))),D by FUNCT_2:2;
rng (A "**" ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E2)) c= D ;
then reconsider G2 = A "**" ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E2) as Function of (dom (A "**" ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E2))),D by FUNCT_2:2;
rng ((A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E2))) c= D ;
then reconsider G12 = (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E2)) as Function of (dom ((A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E2)))),D by FUNCT_2:2;
dom ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E1) = dom (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E1)) by FUNCT_2:def 1;
then A9: M $$ (([#] (dom (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E1)))),G1) = SignGenOp ((f ^ <*(A . (d1,d2))*>),M,A,((Seg (1 + (len f))) \ {1})) by A7, Def13, A2;
dom ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E2) = dom (A "**" ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E2)) by FUNCT_2:def 1;
then A10: M $$ (([#] (dom (A "**" ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E2)))),G2) = SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),M,A,((Seg (1 + (len f))) \ {1})) by A7, Def13, A2;
A11: dom (A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1),((len f) + 2)}))))) * E)) = dom ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1),((len f) + 2)}))))) * E) by FUNCT_2:def 1;
Seg ((1 + (len f)) + 1) = (Seg (1 + (len f))) \/ {(2 + (len f))} by FINSEQ_1:9;
then (Seg (2 + (len f))) \ {1} = ((Seg (1 + (len f))) \ {1}) \/ {(2 + (len f))} by A5, XBOOLE_1:42;
then (Seg (2 + (len f))) \ {1} = ((Seg (len f)) \ {1}) \/ ({(1 + (len f))} \/ {(2 + (len f))}) by A6, XBOOLE_1:4;
then (Seg (2 + (len f))) \ {1} = ((Seg (len f)) \ {1}) \/ {(1 + (len f)),(2 + (len f))} by ENUMSET1:1;
then bool ((Seg (2 + (len f))) \ {1}) = UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1),((len f) + 2)})) by Th6;
then SignGenOp (((f ^ <*d1*>) ^ <*d2*>),M,A,((Seg (2 + (len f))) \ {1})) = M $$ (([#] (dom ((A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,(UNION ((bool ((Seg (len f)) \ {1})),(bool {((len f) + 1)}))))) * E2))))),G12) by Def13, A2, A11, A8;
hence 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})))) by A2, Th64, A9, A10; :: thesis: verum