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 holds doms ((SignGenOp (f,A,F)) * E) = doms ((len f),(card F))
let A be BinOp of D; :: thesis: for f being FinSequence of D
for F being finite set
for E being Enumeration of F holds doms ((SignGenOp (f,A,F)) * E) = doms ((len f),(card F))
let f be FinSequence of D; :: thesis: for F being finite set
for E being Enumeration of F holds doms ((SignGenOp (f,A,F)) * E) = doms ((len f),(card F))
let F be finite set ; :: thesis: for E being Enumeration of F holds doms ((SignGenOp (f,A,F)) * E) = doms ((len f),(card F))
let E be Enumeration of F; :: thesis: doms ((SignGenOp (f,A,F)) * E) = doms ((len f),(card F))
A1: ( len ((SignGenOp (f,A,F)) * E) = len E & len E = card F ) by CARD_1:def 7;
thus doms ((SignGenOp (f,A,F)) * E) c= doms ((len f),(card F)) :: according to XBOOLE_0:def 10 :: thesis: doms ((len f),(card F)) c= doms ((SignGenOp (f,A,F)) * E)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in doms ((SignGenOp (f,A,F)) * E) or x in doms ((len f),(card F)) )
assume A2: x in doms ((SignGenOp (f,A,F)) * E) ; :: thesis: x in doms ((len f),(card F))
reconsider x = x as FinSequence by A2;
A3: len x = len ((SignGenOp (f,A,F)) * E) by A2, Th47;
rng x c= Seg (len f)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng x or y in Seg (len f) )
assume y in rng x ; :: thesis: y in Seg (len f)
then consider i being object such that
A4: ( i in dom x & y = x . i ) by FUNCT_1:def 3;
reconsider i = i as Nat by A4;
A5: x . i in dom (((SignGenOp (f,A,F)) * E) . i) by A4, A2, Th47;
((SignGenOp (f,A,F)) * E) . i <> {} by A4, A2, Th47;
then i in dom ((SignGenOp (f,A,F)) * E) by FUNCT_1:def 2;
then ((SignGenOp (f,A,F)) * E) . i = SignGen (f,A,(E . i)) by Th80;
then x . i in dom f by A5, Def11;
hence y in Seg (len f) by A4, FINSEQ_1:def 3; :: thesis: verum

end;

then reconsider x = x as FinSequence of Seg (len f) by FINSEQ_1:def 4;
x in (Seg (len f)) * by FINSEQ_1:def 11;
hence x in doms ((len f),(card F)) by A1, A3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in doms ((len f),(card F)) or x in doms ((SignGenOp (f,A,F)) * E) )
assume A6: x in doms ((len f),(card F)) ; :: thesis: x in doms ((SignGenOp (f,A,F)) * E)
consider s being Element of (Seg (len f)) * such that
A7: ( x = s & len s = card F ) by A6;
A8: ( rng s c= Seg (len f) & Seg (len f) = dom f ) by FINSEQ_1:def 3;
for i being Nat st i in dom s holds
s . i in dom (((SignGenOp (f,A,F)) * E) . i)

proof

let i be Nat; :: thesis: ( i in dom s implies s . i in dom (((SignGenOp (f,A,F)) * E) . i) )
assume A9: i in dom s ; :: thesis: s . i in dom (((SignGenOp (f,A,F)) * E) . i)
A10: s . i in rng s by A9, FUNCT_1:def 3;
dom s = dom ((SignGenOp (f,A,F)) * E) by A1, A7, FINSEQ_3:29;
then ((SignGenOp (f,A,F)) * E) . i = SignGen (f,A,(E . i)) by A9, Th80;
then dom (((SignGenOp (f,A,F)) * E) . i) = dom f by Def11;
hence s . i in dom (((SignGenOp (f,A,F)) * E) . i) by A8, A10; :: thesis: verum

end;

hence x in doms ((SignGenOp (f,A,F)) * E) by A7, A1, Th47; :: thesis: verum