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),(len E))
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),(len E))
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),(len E))
let F be finite set ; :: thesis: for E being Enumeration of F holds doms ((SignGenOp (f,A,F)) * E) = doms ((len f),(len E))
let E be Enumeration of F; :: thesis: doms ((SignGenOp (f,A,F)) * E) = doms ((len f),(len E))
len E = card F by CARD_1:def 7;
hence doms ((SignGenOp (f,A,F)) * E) = doms ((len f),(len E)) by Th106; :: thesis: verum