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
s * p in doms ((SignGenOp (f,A,F)) * (E * 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
s * p in doms ((SignGenOp (f,A,F)) * (E * 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
s * p in doms ((SignGenOp (f,A,F)) * (E * 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
s * p in doms ((SignGenOp (f,A,F)) * (E * 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
s * p in doms ((SignGenOp (f,A,F)) * (E * p))
let p be Permutation of (dom E); :: thesis: for s being FinSequence st s in doms ((SignGenOp (f,A,F)) * E) holds
s * p in doms ((SignGenOp (f,A,F)) * (E * p))
let s be FinSequence; :: thesis: ( s in doms ((SignGenOp (f,A,F)) * E) implies s * p in doms ((SignGenOp (f,A,F)) * (E * p)) )
assume A1: s in doms ((SignGenOp (f,A,F)) * E) ; :: thesis: s * p in doms ((SignGenOp (f,A,F)) * (E * p))
reconsider Ep = E * p as Enumeration of F by Th109;
A2: ( len ((SignGenOp (f,A,F)) * Ep) = len Ep & len Ep = card F ) by CARD_1:def 7;
A3: ( len s = len ((SignGenOp (f,A,F)) * E) & len ((SignGenOp (f,A,F)) * E) = len E & len E = card F ) by Th47, A1, CARD_1:def 7;
then A4: dom E = dom s by FINSEQ_3:30;
( dom p = dom E & dom E = rng p ) by FUNCT_2:52, FUNCT_2:def 3;
then A5: ( dom (s * p) = dom s & dom s = Seg (len s) ) by A4, RELAT_1:27, FINSEQ_1:def 3;
reconsider sp = s * p as FinSequence by A4;
A6: len sp = len s by A5, FINSEQ_3:29;
for i being Nat st i in dom sp holds
sp . i in dom (((SignGenOp (f,A,F)) * Ep) . i)

proof

let i be Nat; :: thesis: ( i in dom sp implies sp . i in dom (((SignGenOp (f,A,F)) * Ep) . i) )
assume i in dom sp ; :: thesis: sp . i in dom (((SignGenOp (f,A,F)) * Ep) . i)
then A7: ( i in dom p & p . i in dom s ) by FUNCT_1:11;
then A8: ( s . (p . i) in dom (((SignGenOp (f,A,F)) * E) . (p . i)) & s . (p . i) = sp . i ) by A1, Th47, FUNCT_1:13;
((SignGenOp (f,A,F)) * E) . (p . i) = (((SignGenOp (f,A,F)) * E) * p) . i by A7, FUNCT_1:13
.= ((SignGenOp (f,A,F)) * Ep) . i by RELAT_1:36 ;
hence sp . i in dom (((SignGenOp (f,A,F)) * Ep) . i) by A8; :: thesis: verum

end;

hence s * p in doms ((SignGenOp (f,A,F)) * (E * p)) by A2, A3, A6, Th47; :: thesis: verum