let D be non empty set ; :: thesis: for b being BinOp of D
for d, d1, d2 being Element of D holds b "**" <%d,d1,d2%> = b . (b . d,d1),d2
let b be BinOp of D; :: thesis: for d, d1, d2 being Element of D holds b "**" <%d,d1,d2%> = b . (b . d,d1),d2
let d, d1, d2 be Element of D; :: thesis: b "**" <%d,d1,d2%> = b . (b . d,d1),d2
set F = <%d,d1,d2%>;
len <%d,d1,d2%> = 3 by AFINSQ_1:43;
then consider f being Function of NAT ,D such that
A1: f . 0 = <%d,d1,d2%> . 0 and
A2: for n being Element of NAT st n + 1 < 3 holds
f . (n + 1) = b . (f . n),(<%d,d1,d2%> . (n + 1)) and
A3: b "**" <%d,d1,d2%> = f . (3 - 1) by Def3;
( f . (0 + 1) = b . (f . 0 ),(<%d,d1,d2%> . (0 + 1)) & f . (1 + 1) = b . (f . 1),(<%d,d1,d2%> . (1 + 1)) & <%d,d1,d2%> . 0 = d & <%d,d1,d2%> . 1 = d1 & <%d,d1,d2%> . 2 = d2 ) by A2, AFINSQ_1:43;
hence b "**" <%d,d1,d2%> = b . (b . d,d1),d2 by A1, A3; :: thesis: verum