let D be non empty set ; :: thesis: for d being Element of D
for g being BinOp of D
for k, l being Element of NAT st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds
g "**" ((k + l) |-> d) = g . (g "**" (k |-> d)),(g "**" (l |-> d))
let d be Element of D; :: thesis: for g being BinOp of D
for k, l being Element of NAT st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds
g "**" ((k + l) |-> d) = g . (g "**" (k |-> d)),(g "**" (l |-> d))
let g be BinOp of D; :: thesis: for k, l being Element of NAT st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds
g "**" ((k + l) |-> d) = g . (g "**" (k |-> d)),(g "**" (l |-> d))
let k, l be Element of NAT ; :: thesis: ( g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) implies g "**" ((k + l) |-> d) = g . (g "**" (k |-> d)),(g "**" (l |-> d)) )
( k <> 0 & l <> 0 implies ( len (k |-> d) <> 0 & len (l |-> d) <> 0 ) ) by FINSEQ_1:def 18;
then A1: ( k <> 0 & l <> 0 implies ( len (k |-> d) >= 1 & len (l |-> d) >= 1 ) ) by NAT_1:14;
(k + l) |-> d = (k |-> d) ^ (l |-> d) by FINSEQ_2:143;
hence ( g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) implies g "**" ((k + l) |-> d) = g . (g "**" (k |-> d)),(g "**" (l |-> d)) ) by A1, Th6; :: thesis: verum