let D be non empty set ; :: thesis: 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; :: thesis: for d1, d2 being Element of D holds b "**" <%d1,d2%> = b . (d1,d2)
let d1, d2 be Element of D; :: thesis: b "**" <%d1,d2%> = b . (d1,d2)
A1: <%d1,d2%> . 0 = d1 by AFINSQ_1:38;
len <%d1,d2%> = 2 by AFINSQ_1:38;
then consider f being Function of NAT,D such that
A2: f . 0 = <%d1,d2%> . 0 and
A3: for n being Nat st n + 1 < 2 holds
f . (n + 1) = b . ((f . n),(<%d1,d2%> . (n + 1))) and
A4: b "**" <%d1,d2%> = f . (2 - 1) by Def9;
f . (0 + 1) = b . ((f . 0),(<%d1,d2%> . (0 + 1))) by A3;
hence b "**" <%d1,d2%> = b . (d1,d2) by A2, A4, A1, AFINSQ_1:38; :: thesis: verum