let D be non empty set ; :: thesis: for d being Element of D
for F being FinSequence of D
for g being BinOp of D st g is associative & ( g is having_a_unity or len F >= 1 ) holds
g "**" (<*d*> ^ F) = g . (d,(g "**" F))
let d be Element of D; :: thesis: for F being FinSequence of D
for g being BinOp of D st g is associative & ( g is having_a_unity or len F >= 1 ) holds
g "**" (<*d*> ^ F) = g . (d,(g "**" F))
let F be FinSequence of D; :: thesis: for g being BinOp of D st g is associative & ( g is having_a_unity or len F >= 1 ) holds
g "**" (<*d*> ^ F) = g . (d,(g "**" F))
let g be BinOp of D; :: thesis: ( g is associative & ( g is having_a_unity or len F >= 1 ) implies g "**" (<*d*> ^ F) = g . (d,(g "**" F)) )
A1: len <*d*> = 1 by FINSEQ_1:39;
assume ( g is associative & ( g is having_a_unity or len F >= 1 ) ) ; :: thesis: g "**" (<*d*> ^ F) = g . (d,(g "**" F))
hence g "**" (<*d*> ^ F) = g . ((g "**" <*d*>),(g "**" F)) by A1, Th5
.= g . (d,(g "**" F)) by Lm4 ;
:: thesis: verum