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

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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( ( 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 ) ; :: thesis: 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; :: thesis: verum