let D be non empty set ; for b being BinOp of D
for d1, d2 being Element of D holds b "**" <%d1,d2%> = b . (d1,d2)
let b be BinOp of D; for d1, d2 being Element of D holds b "**" <%d1,d2%> = b . (d1,d2)
let d1, d2 be Element of D; b "**" <%d1,d2%> = b . (d1,d2)
len <%d1,d2%> = 2
by AFINSQ_1:38;
then consider f being sequence of D such that
A1:
f . 0 = <%d1,d2%> . 0
and
A2:
for n being Nat st n + 1 < 2 holds
f . (n + 1) = b . ((f . n),(<%d1,d2%> . (n + 1)))
and
A3:
b "**" <%d1,d2%> = f . (2 - 1)
by Def8;
f . (zz + 1) = b . ((f . zz),(<%d1,d2%> . (zz + 1)))
by A2;
hence
b "**" <%d1,d2%> = b . (d1,d2)
by A1, A3; verum