let D be non empty set ; for d being Element of D
for F being BinOp of D
for i, j being Nat st F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) holds
F "**" ((i + j) |-> d) = F . ((F "**" (i |-> d)),(F "**" (j |-> d)))
let d be Element of D; for F being BinOp of D
for i, j being Nat st F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) holds
F "**" ((i + j) |-> d) = F . ((F "**" (i |-> d)),(F "**" (j |-> d)))
let F be BinOp of D; for i, j being Nat st F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) holds
F "**" ((i + j) |-> d) = F . ((F "**" (i |-> d)),(F "**" (j |-> d)))
let i, j be Nat; ( F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) implies F "**" ((i + j) |-> d) = F . ((F "**" (i |-> d)),(F "**" (j |-> d))) )
assume A1:
F is associative
; ( ( not ( i >= 1 & j >= 1 ) & not F is having_a_unity ) or F "**" ((i + j) |-> d) = F . ((F "**" (i |-> d)),(F "**" (j |-> d))) )
set p1 = i |-> d;
set p2 = j |-> d;
assume
( ( i >= 1 & j >= 1 ) or F is having_a_unity )
; F "**" ((i + j) |-> d) = F . ((F "**" (i |-> d)),(F "**" (j |-> d)))
then
( ( len (i |-> d) >= 1 & len (j |-> d) >= 1 ) or F is having_a_unity )
by CARD_1:def 7;
then
F "**" ((i |-> d) ^ (j |-> d)) = F . ((F "**" (i |-> d)),(F "**" (j |-> d)))
by A1, FINSOP_1:5;
hence
F "**" ((i + j) |-> d) = F . ((F "**" (i |-> d)),(F "**" (j |-> d)))
by FINSEQ_2:123; verum