let X be set ; :: thesis: for D being non empty set
for B being BinOp of D
for f being FinSequence of D st B is having_a_unity & B is associative & B is having_an_inverseOp holds
SignGen ((SignGen (f,B,X)),B,X) = f
let D be non empty set ; :: thesis: for B being BinOp of D
for f being FinSequence of D st B is having_a_unity & B is associative & B is having_an_inverseOp holds
SignGen ((SignGen (f,B,X)),B,X) = f
let B be BinOp of D; :: thesis: for f being FinSequence of D st B is having_a_unity & B is associative & B is having_an_inverseOp holds
SignGen ((SignGen (f,B,X)),B,X) = f
let f be FinSequence of D; :: thesis: ( B is having_a_unity & B is associative & B is having_an_inverseOp implies SignGen ((SignGen (f,B,X)),B,X) = f )
set C = SignGen (f,B,X);
set I = the_inverseOp_wrt B;
assume A1: ( B is having_a_unity & B is associative & B is having_an_inverseOp ) ; :: thesis: SignGen ((SignGen (f,B,X)),B,X) = f
A2: ( len (SignGen ((SignGen (f,B,X)),B,X)) = len (SignGen (f,B,X)) & len (SignGen (f,B,X)) = len f ) by CARD_1:def 7;
A3: ( dom f = dom (SignGen (f,B,X)) & dom (SignGen (f,B,X)) = dom (SignGen ((SignGen (f,B,X)),B,X)) ) by Def11;
for k being Nat st 1 <= k & k <= len f holds
(SignGen ((SignGen (f,B,X)),B,X)) . k = f . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len f implies (SignGen ((SignGen (f,B,X)),B,X)) . k = f . k )
assume A4: ( 1 <= k & k <= len f ) ; :: thesis: (SignGen ((SignGen (f,B,X)),B,X)) . k = f . k
A5: k in dom f by A4, FINSEQ_3:25;
then A6: f . k = f /. k by PARTFUN1:def 6;

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

suppose A7: k in X ; :: thesis: (SignGen ((SignGen (f,B,X)),B,X)) . k = f . k

then (SignGen (f,B,X)) . k = (the_inverseOp_wrt B) . (f . k) by A5, A3, Def11;
then (SignGen ((SignGen (f,B,X)),B,X)) . k = (the_inverseOp_wrt B) . ((the_inverseOp_wrt B) . (f /. k)) by A5, A7, A6, A3, Def11;
hence (SignGen ((SignGen (f,B,X)),B,X)) . k = f . k by A1, A6, FINSEQOP:62; :: thesis: verum

end;

suppose A8: not k in X ; :: thesis: (SignGen ((SignGen (f,B,X)),B,X)) . k = f . k

then (SignGen (f,B,X)) . k = f . k by A5, A3, Def11;
hence (SignGen ((SignGen (f,B,X)),B,X)) . k = f . k by A5, A8, A3, Def11; :: thesis: verum

end;

end;

end;

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