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

proof

let i be Nat; :: thesis: ( i in dom f implies (SignGen (f,B,X)) . i = f . i )
assume A3: i in dom f ; :: thesis: (SignGen (f,B,X)) . i = f . i
not i in X by A3, A1, XBOOLE_0:3;
hence (SignGen (f,B,X)) . i = f . i by A2, A3, Def11; :: thesis: verum

end;

hence SignGen (f,B,X) = f by A2; :: thesis: verum