let i be Nat; :: thesis: for D being non empty set
for B being BinOp of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F st ( i in dom E or i in dom ((SignGenOp (f,B,F)) * E) ) holds
((SignGenOp (f,B,F)) * E) . i = SignGen (f,B,(E . i))
let D be non empty set ; :: thesis: for B being BinOp of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F st ( i in dom E or i in dom ((SignGenOp (f,B,F)) * E) ) holds
((SignGenOp (f,B,F)) * E) . i = SignGen (f,B,(E . i))
let B be BinOp of D; :: thesis: for f being FinSequence of D
for F being finite set
for E being Enumeration of F st ( i in dom E or i in dom ((SignGenOp (f,B,F)) * E) ) holds
((SignGenOp (f,B,F)) * E) . i = SignGen (f,B,(E . i))
let f be FinSequence of D; :: thesis: for F being finite set
for E being Enumeration of F st ( i in dom E or i in dom ((SignGenOp (f,B,F)) * E) ) holds
((SignGenOp (f,B,F)) * E) . i = SignGen (f,B,(E . i))
let F be finite set ; :: thesis: for E being Enumeration of F st ( i in dom E or i in dom ((SignGenOp (f,B,F)) * E) ) holds
((SignGenOp (f,B,F)) * E) . i = SignGen (f,B,(E . i))
let E be Enumeration of F; :: thesis: ( ( i in dom E or i in dom ((SignGenOp (f,B,F)) * E) ) implies ((SignGenOp (f,B,F)) * E) . i = SignGen (f,B,(E . i)) )
assume A1: ( i in dom E or i in dom ((SignGenOp (f,B,F)) * E) ) ; :: thesis: ((SignGenOp (f,B,F)) * E) . i = SignGen (f,B,(E . i))
set C = SignGenOp (f,B,F);
i in dom ((SignGenOp (f,B,F)) * E)

proof

assume A2: not i in dom ((SignGenOp (f,B,F)) * E) ; :: thesis: contradiction
then ( E . i in rng E & rng E = F & F = dom (SignGenOp (f,B,F)) ) by A1, FUNCT_2:def 1, FUNCT_1:def 3, RLAFFIN3:def 1;
hence contradiction by A2, A1, FUNCT_1:11; :: thesis: verum

end;

then ( ((SignGenOp (f,B,F)) * E) . i = (SignGenOp (f,B,F)) . (E . i) & E . i in dom (SignGenOp (f,B,F)) & dom (SignGenOp (f,B,F)) = F ) by FUNCT_1:11, FUNCT_1:12, FUNCT_2:def 1;
hence ((SignGenOp (f,B,F)) * E) . i = SignGen (f,B,(E . i)) by Def12; :: thesis: verum