let D be non empty set ; :: thesis: for A, M being BinOp of D
for f being FinSequence of D
for F being finite set st M is commutative & M is associative holds
for E being Enumeration of F
for p being Permutation of (dom E)
for s being FinSequence st s in doms ((SignGenOp (f,A,F)) * E) & ( len s >= 1 or M is having_a_unity ) holds
(M "**" (App ((SignGenOp (f,A,F)) * E))) . s = (M "**" (App ((SignGenOp (f,A,F)) * (E * p)))) . (s * p)
let A, M be BinOp of D; :: thesis: for f being FinSequence of D
for F being finite set st M is commutative & M is associative holds
for E being Enumeration of F
for p being Permutation of (dom E)
for s being FinSequence st s in doms ((SignGenOp (f,A,F)) * E) & ( len s >= 1 or M is having_a_unity ) holds
(M "**" (App ((SignGenOp (f,A,F)) * E))) . s = (M "**" (App ((SignGenOp (f,A,F)) * (E * p)))) . (s * p)
let f be FinSequence of D; :: thesis: for F being finite set st M is commutative & M is associative holds
for E being Enumeration of F
for p being Permutation of (dom E)
for s being FinSequence st s in doms ((SignGenOp (f,A,F)) * E) & ( len s >= 1 or M is having_a_unity ) holds
(M "**" (App ((SignGenOp (f,A,F)) * E))) . s = (M "**" (App ((SignGenOp (f,A,F)) * (E * p)))) . (s * p)
let F be finite set ; :: thesis: ( M is commutative & M is associative implies for E being Enumeration of F
for p being Permutation of (dom E)
for s being FinSequence st s in doms ((SignGenOp (f,A,F)) * E) & ( len s >= 1 or M is having_a_unity ) holds
(M "**" (App ((SignGenOp (f,A,F)) * E))) . s = (M "**" (App ((SignGenOp (f,A,F)) * (E * p)))) . (s * p) )
assume A1: ( M is commutative & M is associative ) ; :: thesis: for E being Enumeration of F
for p being Permutation of (dom E)
for s being FinSequence st s in doms ((SignGenOp (f,A,F)) * E) & ( len s >= 1 or M is having_a_unity ) holds
(M "**" (App ((SignGenOp (f,A,F)) * E))) . s = (M "**" (App ((SignGenOp (f,A,F)) * (E * p)))) . (s * p)
let E be Enumeration of F; :: thesis: for p being Permutation of (dom E)
for s being FinSequence st s in doms ((SignGenOp (f,A,F)) * E) & ( len s >= 1 or M is having_a_unity ) holds
(M "**" (App ((SignGenOp (f,A,F)) * E))) . s = (M "**" (App ((SignGenOp (f,A,F)) * (E * p)))) . (s * p)
let p be Permutation of (dom E); :: thesis: for s being FinSequence st s in doms ((SignGenOp (f,A,F)) * E) & ( len s >= 1 or M is having_a_unity ) holds
(M "**" (App ((SignGenOp (f,A,F)) * E))) . s = (M "**" (App ((SignGenOp (f,A,F)) * (E * p)))) . (s * p)
let s be FinSequence; :: thesis: ( s in doms ((SignGenOp (f,A,F)) * E) & ( len s >= 1 or M is having_a_unity ) implies (M "**" (App ((SignGenOp (f,A,F)) * E))) . s = (M "**" (App ((SignGenOp (f,A,F)) * (E * p)))) . (s * p) )
assume A2: ( s in doms ((SignGenOp (f,A,F)) * E) & ( len s >= 1 or M is having_a_unity ) ) ; :: thesis: (M "**" (App ((SignGenOp (f,A,F)) * E))) . s = (M "**" (App ((SignGenOp (f,A,F)) * (E * p)))) . (s * p)
set Ep = E * p;
set sp = s * p;
s * p in doms ((SignGenOp (f,A,F)) * (E * p)) by A2, Th110;
then s * p in dom (App ((SignGenOp (f,A,F)) * (E * p))) by Def9;
then A3: (M "**" (App ((SignGenOp (f,A,F)) * (E * p)))) . (s * p) = M "**" ((App ((SignGenOp (f,A,F)) * (E * p))) . (s * p)) by Def10;
A4: ( len s = len ((SignGenOp (f,A,F)) * E) & len ((SignGenOp (f,A,F)) * E) = len E ) by Th47, A2, CARD_1:def 7;
len s = len ((App ((SignGenOp (f,A,F)) * E)) . s) by Def9, A2;
then A5: dom E = dom ((App ((SignGenOp (f,A,F)) * E)) . s) by A4, FINSEQ_3:29;
s in dom (App ((SignGenOp (f,A,F)) * E)) by A2, Def9;
then A6: (M "**" (App ((SignGenOp (f,A,F)) * E))) . s = M "**" ((App ((SignGenOp (f,A,F)) * E)) . s) by Def10;
A7: ( M is having_a_unity or len ((App ((SignGenOp (f,A,F)) * E)) . s) >= 1 ) by A2, Def9;
(App ((SignGenOp (f,A,F)) * (E * p))) . (s * p) = ((App ((SignGenOp (f,A,F)) * E)) . s) * p by A2, Th111;
hence (M "**" (App ((SignGenOp (f,A,F)) * E))) . s = (M "**" (App ((SignGenOp (f,A,F)) * (E * p)))) . (s * p) by A3, A6, A1, FINSOP_1:7, A5, A7; :: thesis: verum