let D be non empty set ; :: thesis: for d being Element of D
for g being BinOp of D holds g "**" <*d*> = d
let d be Element of D; :: thesis: for g being BinOp of D holds g "**" <*d*> = d
let g be BinOp of D; :: thesis: g "**" <*d*> = d
A1: len <*d*> = 1 by FINSEQ_1:39;
then ex f being sequence of D st
( f . 1 = <*d*> . 1 & ( for n being Nat st 0 <> n & n < len <*d*> holds
f . (n + 1) = g . ((f . n),(<*d*> . (n + 1))) ) & g "**" <*d*> = f . (len <*d*>) ) by Def1;
hence g "**" <*d*> = d by A1; :: thesis: verum