set C = SignGenOp (f,A,(bool F));
set E = the Enumeration of bool F;
take IT = M $$ (([#] (dom ((SignGenOp (f,A,(bool F))) * the Enumeration of bool F))),(A "**" ((SignGenOp (f,A,(bool F))) * the Enumeration of bool F))); :: thesis: for E being Enumeration of bool F holds IT = M $$ (([#] (dom ((SignGenOp (f,A,(bool F))) * E))),(A "**" ((SignGenOp (f,A,(bool F))) * E)))
let G be Enumeration of bool F; :: thesis: IT = M $$ (([#] (dom ((SignGenOp (f,A,(bool F))) * G))),(A "**" ((SignGenOp (f,A,(bool F))) * G)))
A2: ( rng the Enumeration of bool F = bool F & bool F = rng G ) by RLAFFIN3:def 1;
then consider s being Function such that
A3: ( dom s = dom the Enumeration of bool F & rng s = dom G & s is one-to-one & the Enumeration of bool F = G * s ) by RFINSEQ:26, CLASSES1:77;
A4: the Enumeration of bool F,G are_fiberwise_equipotent by A2, RFINSEQ:26;
( len ((SignGenOp (f,A,(bool F))) * the Enumeration of bool F) = len the Enumeration of bool F & len G = len ((SignGenOp (f,A,(bool F))) * G) ) by CARD_1:def 7;
then A5: ( dom ((SignGenOp (f,A,(bool F))) * the Enumeration of bool F) = dom the Enumeration of bool F & dom the Enumeration of bool F = dom G & dom G = dom ((SignGenOp (f,A,(bool F))) * G) ) by A4, RFINSEQ:3, FINSEQ_3:30;
A6: (A "**" ((SignGenOp (f,A,(bool F))) * the Enumeration of bool F)) | (dom s) = A "**" ((SignGenOp (f,A,(bool F))) * the Enumeration of bool F) by A3, A5;
A7: ( dom (A "**" ((SignGenOp (f,A,(bool F))) * G)) = dom G & dom (A "**" ((SignGenOp (f,A,(bool F))) * the Enumeration of bool F)) = dom the Enumeration of bool F ) by A5, FUNCT_2:def 1;
for x being object st x in dom s holds
(A "**" ((SignGenOp (f,A,(bool F))) * the Enumeration of bool F)) . x = ((A "**" ((SignGenOp (f,A,(bool F))) * G)) * s) . x

proof

let x be object ; :: thesis: ( x in dom s implies (A "**" ((SignGenOp (f,A,(bool F))) * the Enumeration of bool F)) . x = ((A "**" ((SignGenOp (f,A,(bool F))) * G)) * s) . x )
assume A8: x in dom s ; :: thesis: (A "**" ((SignGenOp (f,A,(bool F))) * the Enumeration of bool F)) . x = ((A "**" ((SignGenOp (f,A,(bool F))) * G)) * s) . x
reconsider i = x as Nat by A8, A3;
A9: s . i in dom G by A3, A8, FUNCT_1:11;
thus ((A "**" ((SignGenOp (f,A,(bool F))) * G)) * s) . x = (A "**" ((SignGenOp (f,A,(bool F))) * G)) . (s . i) by A8, FUNCT_1:13
.= A "**" (((SignGenOp (f,A,(bool F))) * G) . (s . i)) by A9, A5, Def10
.= A "**" ((SignGenOp (f,A,(bool F))) . (G . (s . i))) by A9, FUNCT_1:13
.= A "**" ((SignGenOp (f,A,(bool F))) . ( the Enumeration of bool F . i)) by A8, A3, FUNCT_1:13
.= A "**" (((SignGenOp (f,A,(bool F))) * the Enumeration of bool F) . i) by A8, A3, FUNCT_1:13
.= (A "**" ((SignGenOp (f,A,(bool F))) * the Enumeration of bool F)) . x by A8, A3, A5, Def10 ; :: thesis: verum

end;

then A "**" ((SignGenOp (f,A,(bool F))) * the Enumeration of bool F) = (A "**" ((SignGenOp (f,A,(bool F))) * G)) * s by A3, RELAT_1:27, A7;
hence IT = M $$ (([#] (dom ((SignGenOp (f,A,(bool F))) * G))),(A "**" ((SignGenOp (f,A,(bool F))) * G))) by A6, A3, A5, A1, SETWOP_2:5; :: thesis: verum