let D be non empty set ; :: thesis: for A being BinOp of D
for f being FinSequence of D
for F being finite set
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) holds
((App ((SignGenOp (f,A,F)) * E)) . s) * p = (App ((SignGenOp (f,A,F)) * (E * p))) . (s * p)
let A be BinOp of D; :: thesis: for f being FinSequence of D
for F being finite set
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) holds
((App ((SignGenOp (f,A,F)) * E)) . s) * p = (App ((SignGenOp (f,A,F)) * (E * p))) . (s * p)
let f be FinSequence of D; :: thesis: for F being finite set
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) holds
((App ((SignGenOp (f,A,F)) * E)) . s) * p = (App ((SignGenOp (f,A,F)) * (E * p))) . (s * p)
let F be finite set ; :: 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) holds
((App ((SignGenOp (f,A,F)) * E)) . s) * p = (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) holds
((App ((SignGenOp (f,A,F)) * E)) . s) * p = (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) holds
((App ((SignGenOp (f,A,F)) * E)) . s) * p = (App ((SignGenOp (f,A,F)) * (E * p))) . (s * p)
set C = SignGenOp (f,A,F);
let s be FinSequence; :: thesis: ( s in doms ((SignGenOp (f,A,F)) * E) implies ((App ((SignGenOp (f,A,F)) * E)) . s) * p = (App ((SignGenOp (f,A,F)) * (E * p))) . (s * p) )
assume A1: s in doms ((SignGenOp (f,A,F)) * E) ; :: thesis: ((App ((SignGenOp (f,A,F)) * E)) . s) * p = (App ((SignGenOp (f,A,F)) * (E * p))) . (s * p)
A2: s * p in doms ((SignGenOp (f,A,F)) * (E * p)) by A1, Th110;
then reconsider sp = s * p as FinSequence ;
A3: ( len s = len ((SignGenOp (f,A,F)) * E) & len ((SignGenOp (f,A,F)) * E) = len E ) by Th47, A1, CARD_1:def 7;
then A4: ( dom E = dom ((SignGenOp (f,A,F)) * E) & dom ((SignGenOp (f,A,F)) * E) = dom s ) by FINSEQ_3:30;
A5: ( dom p = dom E & dom E = rng p ) by FUNCT_2:52, FUNCT_2:def 3;
then A6: dom sp = dom s by A4, RELAT_1:27;
A7: len ((App ((SignGenOp (f,A,F)) * (E * p))) . sp) = len sp by A2, Def9;
then A8: dom ((App ((SignGenOp (f,A,F)) * (E * p))) . sp) = dom sp by FINSEQ_3:29;
len ((App ((SignGenOp (f,A,F)) * E)) . s) = len s by A1, Def9;
then A9: dom ((App ((SignGenOp (f,A,F)) * E)) . s) = dom s by FINSEQ_3:29;
then A10: dom (((App ((SignGenOp (f,A,F)) * E)) . s) * p) = dom p by A5, A3, FINSEQ_3:30, RELAT_1:27;
for i being Nat st i in dom ((App ((SignGenOp (f,A,F)) * (E * p))) . sp) holds
(((App ((SignGenOp (f,A,F)) * E)) . s) * p) . i = ((App ((SignGenOp (f,A,F)) * (E * p))) . sp) . i

proof

let i be Nat; :: thesis: ( i in dom ((App ((SignGenOp (f,A,F)) * (E * p))) . sp) implies (((App ((SignGenOp (f,A,F)) * E)) . s) * p) . i = ((App ((SignGenOp (f,A,F)) * (E * p))) . sp) . i )
assume A11: i in dom ((App ((SignGenOp (f,A,F)) * (E * p))) . sp) ; :: thesis: (((App ((SignGenOp (f,A,F)) * E)) . s) * p) . i = ((App ((SignGenOp (f,A,F)) * (E * p))) . sp) . i
i in dom sp by A7, FINSEQ_3:29, A11;
then A12: ( ((App ((SignGenOp (f,A,F)) * (E * p))) . sp) . i = (((SignGenOp (f,A,F)) * (E * p)) . i) . (sp . i) & sp . i = s . (p . i) ) by A2, Def9, FUNCT_1:12;
A13: ( i in dom p & p . i in dom s ) by A11, A8, FUNCT_1:11;
( (((App ((SignGenOp (f,A,F)) * E)) . s) * p) . i = ((App ((SignGenOp (f,A,F)) * E)) . s) . (p . i) & i in dom p & p . i in dom ((App ((SignGenOp (f,A,F)) * E)) . s) ) by A5, A4, A11, A8, A10, A6, FUNCT_1:11, FUNCT_1:12;
then A14: (((App ((SignGenOp (f,A,F)) * E)) . s) * p) . i = (((SignGenOp (f,A,F)) * E) . (p . i)) . (sp . i) by A1, Def9, A9, A12;
((SignGenOp (f,A,F)) * E) . (p . i) = (((SignGenOp (f,A,F)) * E) * p) . i by A13, FUNCT_1:13;
hence (((App ((SignGenOp (f,A,F)) * E)) . s) * p) . i = ((App ((SignGenOp (f,A,F)) * (E * p))) . sp) . i by RELAT_1:36, A12, A14; :: thesis: verum

end;

hence ((App ((SignGenOp (f,A,F)) * E)) . s) * p = (App ((SignGenOp (f,A,F)) * (E * p))) . (s * p) by A8, A10, A4, FUNCT_2:52, A6; :: thesis: verum