let D be non empty set ; :: thesis: for B, A being BinOp of D
for f being FinSequence of D
for F being finite set st A is having_a_unity holds
for E being Enumeration of F
for s being FinSequence st F = {} & s in doms ((SignGenOp (f,B,F)) * E) holds
(A "**" (App ((SignGenOp (f,B,F)) * E))) . s = the_unity_wrt A
let B, A be BinOp of D; :: thesis: for f being FinSequence of D
for F being finite set st A is having_a_unity holds
for E being Enumeration of F
for s being FinSequence st F = {} & s in doms ((SignGenOp (f,B,F)) * E) holds
(A "**" (App ((SignGenOp (f,B,F)) * E))) . s = the_unity_wrt A
let f be FinSequence of D; :: thesis: for F being finite set st A is having_a_unity holds
for E being Enumeration of F
for s being FinSequence st F = {} & s in doms ((SignGenOp (f,B,F)) * E) holds
(A "**" (App ((SignGenOp (f,B,F)) * E))) . s = the_unity_wrt A
let F be finite set ; :: thesis: ( A is having_a_unity implies for E being Enumeration of F
for s being FinSequence st F = {} & s in doms ((SignGenOp (f,B,F)) * E) holds
(A "**" (App ((SignGenOp (f,B,F)) * E))) . s = the_unity_wrt A )
assume A1: A is having_a_unity ; :: thesis: for E being Enumeration of F
for s being FinSequence st F = {} & s in doms ((SignGenOp (f,B,F)) * E) holds
(A "**" (App ((SignGenOp (f,B,F)) * E))) . s = the_unity_wrt A
let E be Enumeration of F; :: thesis: for s being FinSequence st F = {} & s in doms ((SignGenOp (f,B,F)) * E) holds
(A "**" (App ((SignGenOp (f,B,F)) * E))) . s = the_unity_wrt A
let s be FinSequence; :: thesis: ( F = {} & s in doms ((SignGenOp (f,B,F)) * E) implies (A "**" (App ((SignGenOp (f,B,F)) * E))) . s = the_unity_wrt A )
assume A2: ( F = {} & s in doms ((SignGenOp (f,B,F)) * E) ) ; :: thesis: (A "**" (App ((SignGenOp (f,B,F)) * E))) . s = the_unity_wrt A
( len s = len ((SignGenOp (f,B,F)) * E) & len ((SignGenOp (f,B,F)) * E) = len E & len E = card F ) by A2, Th47;
then A3: ( (SignGenOp (f,B,F)) * E = {} & s = {} ) by A2;
s in dom (App ((SignGenOp (f,B,F)) * E)) by A2, Def9;
hence (A "**" (App ((SignGenOp (f,B,F)) * E))) . s = A "**" (<*> D) by A3, Th59, Def10
.= the_unity_wrt A by FINSOP_1:10, A1 ;
:: thesis: verum