let D be non empty set ; :: thesis: 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))
let A 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 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))
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 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))
let f be FinSequence of D; :: thesis: ( A is having_a_unity & A is associative & A is commutative & A is having_an_inverseOp implies 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)) )
set I = the_inverseOp_wrt A;
assume A1: ( A is having_a_unity & A is associative & A is commutative & A is having_an_inverseOp ) ; :: thesis: 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))
let F be non empty finite set ; :: thesis: ( union F c= dom f implies 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)) )
assume A2: union F c= dom f ; :: thesis: 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))
let F1, F2 be finite set ; :: thesis: ( F1 = UNION (F,(bool {((len f) + 1)})) & F2 = UNION (F,(bool {((len f) + 1),((len f) + 2)})) implies 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)) )
assume A3: ( F1 = UNION (F,(bool {((len f) + 1)})) & F2 = UNION (F,(bool {((len f) + 1),((len f) + 2)})) ) ; :: thesis: 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))
consider E1 being Enumeration of F1, E2 being Enumeration of F2 such that
A4: 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)) by A1, A2, A3, Th91;
consider E3 being Enumeration of F1 such that
A5: (SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,F1)) * E1 = (SignGenOp ((f ^ <*((the_inverseOp_wrt A) . (A . (d1,((the_inverseOp_wrt A) . d2))))*>),A,F1)) * E3 by A1, A2, A3, Th116;
take E1 ; :: thesis: ex 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))
take E3 ; :: thesis: 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)) * E3))
take E2 ; :: thesis: A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F2)) * E2) = (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * E1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F1)) * E3))
thus A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F2)) * E2) = (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * E1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (((the_inverseOp_wrt A) . d1),d2))*>),A,F1)) * E3)) by A4, A5, A1, Th2; :: thesis: verum