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%>;
A1: <%d,d1,d2%> . 0 = d by AFINSQ_1:39;
A2: <%d,d1,d2%> . 1 = d1 by AFINSQ_1:39;
len <%d,d1,d2%> = 3 by AFINSQ_1:39;
then consider f being Function of NAT,D such that
A3: f . 0 = <%d,d1,d2%> . 0 and
A4: for n being Nat st n + 1 < 3 holds
f . (n + 1) = b . ((f . n),(<%d,d1,d2%> . (n + 1))) and
A5: b "**" <%d,d1,d2%> = f . (3 - 1) by Def9;
A6: f . (1 + 1) = b . ((f . 1),(<%d,d1,d2%> . (1 + 1))) by A4;
f . (0 + 1) = b . ((f . 0),(<%d,d1,d2%> . (0 + 1))) by A4;
hence b "**" <%d,d1,d2%> = b . ((b . (d,d1)),d2) by A3, A5, A6, A1, A2, AFINSQ_1:39; :: thesis: verum