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) )
assume A1: ( g is associative & ( g is having_a_unity or len F >= 1 ) ) ; :: thesis: g "**" (<*d*> ^ F) = g . d,(g "**" F)
len <*d*> = 1 by FINSEQ_1:56;
hence g "**" (<*d*> ^ F) = g . (g "**" <*d*>),(g "**" F) by A1, Th6
.= g . d,(g "**" F) by Lm4 ;
:: thesis: verum