let D be non empty set ; :: thesis: 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))) )
let A, M be BinOp of D; :: thesis: 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))) )
let f be FinSequence of D; :: thesis: ( 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 implies 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))) ) )
assume A1: ( 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 ) ; :: thesis: 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))) )
let E be Enumeration of bool {2}; :: thesis: 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))) )
let CE be non-empty non empty FinSequence of D * ; :: thesis: ( CE = (SignGenOp (f,A,(bool {2}))) * E & len f = 2 implies 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))) ) )
assume A2: ( CE = (SignGenOp (f,A,(bool {2}))) * E & len f = 2 ) ; :: thesis: 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))) )
consider S being Element of Fin (dom (App CE)) such that
A3: S = {<*1,1*>,<*2,2*>} and
A4: SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE))) by A2, A1, Th141;
take S ; :: thesis: ( S is with_evenly_repeated_values-member & SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE))) )
thus S is with_evenly_repeated_values-member by A3; :: thesis: SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE)))
thus SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE))) by A4; :: thesis: verum