let D be non empty set ; :: thesis: for d being Element of D
for g being BinOp of D
for k, l being 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 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 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 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))) )
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:123;
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, Th5; :: thesis: verum