let D be non empty set ; :: thesis: for A being BinOp of D
for f being FinSequence of D
for F1, F2 being finite set
for E1 being Enumeration of F1
for E2 being Enumeration of F2 st card F1 = card F2 & ( for i being Nat st i in dom E1 holds
(dom f) /\ (E1 . i) = (dom f) /\ (E2 . i) ) holds
(SignGenOp (f,A,F1)) * E1 = (SignGenOp (f,A,F2)) * E2
let A be BinOp of D; :: thesis: for f being FinSequence of D
for F1, F2 being finite set
for E1 being Enumeration of F1
for E2 being Enumeration of F2 st card F1 = card F2 & ( for i being Nat st i in dom E1 holds
(dom f) /\ (E1 . i) = (dom f) /\ (E2 . i) ) holds
(SignGenOp (f,A,F1)) * E1 = (SignGenOp (f,A,F2)) * E2
let f be FinSequence of D; :: thesis: for F1, F2 being finite set
for E1 being Enumeration of F1
for E2 being Enumeration of F2 st card F1 = card F2 & ( for i being Nat st i in dom E1 holds
(dom f) /\ (E1 . i) = (dom f) /\ (E2 . i) ) holds
(SignGenOp (f,A,F1)) * E1 = (SignGenOp (f,A,F2)) * E2
let F1, F2 be finite set ; :: thesis: for E1 being Enumeration of F1
for E2 being Enumeration of F2 st card F1 = card F2 & ( for i being Nat st i in dom E1 holds
(dom f) /\ (E1 . i) = (dom f) /\ (E2 . i) ) holds
(SignGenOp (f,A,F1)) * E1 = (SignGenOp (f,A,F2)) * E2
let E1 be Enumeration of F1; :: thesis: for E2 being Enumeration of F2 st card F1 = card F2 & ( for i being Nat st i in dom E1 holds
(dom f) /\ (E1 . i) = (dom f) /\ (E2 . i) ) holds
(SignGenOp (f,A,F1)) * E1 = (SignGenOp (f,A,F2)) * E2
let E2 be Enumeration of F2; :: thesis: ( card F1 = card F2 & ( for i being Nat st i in dom E1 holds
(dom f) /\ (E1 . i) = (dom f) /\ (E2 . i) ) implies (SignGenOp (f,A,F1)) * E1 = (SignGenOp (f,A,F2)) * E2 )
assume that
A1: card F1 = card F2 and
A2: for i being Nat st i in dom E1 holds
(dom f) /\ (E1 . i) = (dom f) /\ (E2 . i) ; :: thesis: (SignGenOp (f,A,F1)) * E1 = (SignGenOp (f,A,F2)) * E2
set C1 = SignGenOp (f,A,F1);
set C2 = SignGenOp (f,A,F2);
A3: ( len ((SignGenOp (f,A,F1)) * E1) = len E1 & len E1 = card F1 & len ((SignGenOp (f,A,F2)) * E2) = len E2 & len E2 = card F2 ) by CARD_1:def 7;
for i being Nat st 1 <= i & i <= len E1 holds
((SignGenOp (f,A,F1)) * E1) . i = ((SignGenOp (f,A,F2)) * E2) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len E1 implies ((SignGenOp (f,A,F1)) * E1) . i = ((SignGenOp (f,A,F2)) * E2) . i )
assume A4: ( 1 <= i & i <= len E1 ) ; :: thesis: ((SignGenOp (f,A,F1)) * E1) . i = ((SignGenOp (f,A,F2)) * E2) . i
then A5: ( i in dom E1 & i in dom E2 ) by A1, A3, FINSEQ_3:25;
hence ((SignGenOp (f,A,F1)) * E1) . i = SignGen (f,A,(E1 . i)) by Th80
.= SignGen (f,A,((dom f) /\ (E1 . i))) by Th89
.= SignGen (f,A,((dom f) /\ (E2 . i))) by A4, A2, FINSEQ_3:25
.= SignGen (f,A,(E2 . i)) by Th89
.= ((SignGenOp (f,A,F2)) * E2) . i by Th80, A5 ;
:: thesis: verum

end;

hence (SignGenOp (f,A,F1)) * E1 = (SignGenOp (f,A,F2)) * E2 by A1, A3; :: thesis: verum