let D be non empty set ; 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; 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; 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; ( 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; verum