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 FINSEQ_1:def 18;
then F "**" ((i |-> d) ^ (j |-> d)) = F . (F "**" (i |-> d)),(F "**" (j |-> d)) by A1, FINSOP_1:6;
hence F "**" ((i + j) |-> d) = F . (F "**" (i |-> d)),(F "**" (j |-> d)) by FINSEQ_2:143; :: thesis: verum