let D be non empty set ; :: thesis: for b being BinOp of D
for d being Element of D holds b "**" <%d%> = d
let b be BinOp of D; :: thesis: for d being Element of D holds b "**" <%d%> = d
let d be Element of D; :: thesis: b "**" <%d%> = d
len <%d%> = 1 by AFINSQ_1:33;
then ex f being sequence of D st
( f . 0 = <%d%> . 0 & ( for n being Nat st n + 1 < len <%d%> holds
f . (n + 1) = b . ((f . n),(<%d%> . (n + 1))) ) & b "**" <%d%> = f . (1 - 1) ) by Def8;
hence b "**" <%d%> = d ; :: thesis: verum