let X be set ; :: thesis: for D being non empty set
for B being BinOp of D
for f being FinSequence of D
for E being Enumeration of {X} holds (SignGenOp (f,B,{X})) * E = <*(SignGen (f,B,X))*>
let D be non empty set ; :: thesis: for B being BinOp of D
for f being FinSequence of D
for E being Enumeration of {X} holds (SignGenOp (f,B,{X})) * E = <*(SignGen (f,B,X))*>
let B be BinOp of D; :: thesis: for f being FinSequence of D
for E being Enumeration of {X} holds (SignGenOp (f,B,{X})) * E = <*(SignGen (f,B,X))*>
let f be FinSequence of D; :: thesis: for E being Enumeration of {X} holds (SignGenOp (f,B,{X})) * E = <*(SignGen (f,B,X))*>
let E be Enumeration of {X}; :: thesis: (SignGenOp (f,B,{X})) * E = <*(SignGen (f,B,X))*>
A1: ( X in {X} & {X} = dom (SignGenOp (f,B,{X})) & E = <*X*> ) by Th77, FUNCT_2:def 1, TARSKI:def 1;
then (SignGenOp (f,B,{X})) * E = <*((SignGenOp (f,B,{X})) . X)*> by FINSEQ_2:34;
hence (SignGenOp (f,B,{X})) * E = <*(SignGen (f,B,X))*> by A1, Def12; :: thesis: verum