let X be set ; :: thesis: for D being non empty set
for B being BinOp of D
for f being FinSequence of D holds SignGen (f,B,X) = SignGen (f,B,(X /\ (dom f)))
let D be non empty set ; :: thesis: for B being BinOp of D
for f being FinSequence of D holds SignGen (f,B,X) = SignGen (f,B,(X /\ (dom f)))
let B be BinOp of D; :: thesis: for f being FinSequence of D holds SignGen (f,B,X) = SignGen (f,B,(X /\ (dom f)))
let f be FinSequence of D; :: thesis: SignGen (f,B,X) = SignGen (f,B,(X /\ (dom f)))
A1: ( dom (SignGen (f,B,X)) = dom f & dom f = dom (SignGen (f,B,(X /\ (dom f)))) ) by Def11;
for i being Nat st i in dom (SignGen (f,B,X)) holds
(SignGen (f,B,X)) . i = (SignGen (f,B,(X /\ (dom f)))) . i

proof

let i be Nat; :: thesis: ( i in dom (SignGen (f,B,X)) implies (SignGen (f,B,X)) . i = (SignGen (f,B,(X /\ (dom f)))) . i )
assume A2: i in dom (SignGen (f,B,X)) ; :: thesis: (SignGen (f,B,X)) . i = (SignGen (f,B,(X /\ (dom f)))) . i

per cases ( i in X or not i in X ) ;

suppose i in X ; :: thesis: (SignGen (f,B,X)) . i = (SignGen (f,B,(X /\ (dom f)))) . i

then ( (SignGen (f,B,X)) . i = (the_inverseOp_wrt B) . (f . i) & i in X /\ (dom f) ) by Def11, A1, XBOOLE_0:def 4, A2;
hence (SignGen (f,B,X)) . i = (SignGen (f,B,(X /\ (dom f)))) . i by Def11, A1, A2; :: thesis: verum

end;

suppose not i in X ; :: thesis: (SignGen (f,B,X)) . i = (SignGen (f,B,(X /\ (dom f)))) . i

then ( (SignGen (f,B,X)) . i = f . i & not i in X /\ (dom f) ) by Def11, XBOOLE_0:def 4, A2;
hence (SignGen (f,B,X)) . i = (SignGen (f,B,(X /\ (dom f)))) . i by Def11, A1, A2; :: thesis: verum

end;

end;

end;

hence SignGen (f,B,X) = SignGen (f,B,(X /\ (dom f))) by A1; :: thesis: verum