let X be set ; :: thesis: for D being non empty set
for B being BinOp of D
for f being FinSequence of D st dom f c= X holds
SignGen (f,B,X) = (the_inverseOp_wrt B) * f
let D be non empty set ; :: thesis: for B being BinOp of D
for f being FinSequence of D st dom f c= X holds
SignGen (f,B,X) = (the_inverseOp_wrt B) * f
let B be BinOp of D; :: thesis: for f being FinSequence of D st dom f c= X holds
SignGen (f,B,X) = (the_inverseOp_wrt B) * f
let f be FinSequence of D; :: thesis: ( dom f c= X implies SignGen (f,B,X) = (the_inverseOp_wrt B) * f )
assume A1: dom f c= X ; :: thesis: SignGen (f,B,X) = (the_inverseOp_wrt B) * f
( rng f c= D & D = dom (the_inverseOp_wrt B) ) by FUNCT_2:def 1;
then A2: ( dom ((the_inverseOp_wrt B) * f) = dom f & dom f = dom (SignGen (f,B,X)) ) by Def11, RELAT_1:27;
for k being Nat st k in dom (SignGen (f,B,X)) holds
(SignGen (f,B,X)) . k = ((the_inverseOp_wrt B) * f) . k

proof

let k be Nat; :: thesis: ( k in dom (SignGen (f,B,X)) implies (SignGen (f,B,X)) . k = ((the_inverseOp_wrt B) * f) . k )
assume A3: k in dom (SignGen (f,B,X)) ; :: thesis: (SignGen (f,B,X)) . k = ((the_inverseOp_wrt B) * f) . k
(SignGen (f,B,X)) . k = (the_inverseOp_wrt B) . (f . k) by A1, A3, A2, Def11;
hence (SignGen (f,B,X)) . k = ((the_inverseOp_wrt B) * f) . k by A3, A2, FUNCT_1:12; :: thesis: verum

end;

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