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