let D be non empty set ; :: thesis: for B being BinOp of D
for f being FinSequence of D holds SignGen (f,B,{}) = f
let B be BinOp of D; :: thesis: for f being FinSequence of D holds SignGen (f,B,{}) = f
let f be FinSequence of D; :: thesis: SignGen (f,B,{}) = f
{} misses dom f ;
hence SignGen (f,B,{}) = f by Th70; :: thesis: verum