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