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 having_a_unity & len F = 0 holds
g "**" (F ^ <*d*>) = g . (g "**" F),d
let d be Element of D; :: thesis: for F being FinSequence of D
for g being BinOp of D st g is having_a_unity & len F = 0 holds
g "**" (F ^ <*d*>) = g . (g "**" F),d
let F be FinSequence of D; :: thesis: for g being BinOp of D st g is having_a_unity & len F = 0 holds
g "**" (F ^ <*d*>) = g . (g "**" F),d
let g be BinOp of D; :: thesis: ( g is having_a_unity & len F = 0 implies g "**" (F ^ <*d*>) = g . (g "**" F),d )
assume that
A1: g is having_a_unity and
A2: len F = 0 ; :: thesis: g "**" (F ^ <*d*>) = g . (g "**" F),d
F = <*> D by A2;
hence g "**" (F ^ <*d*>) = g "**" <*d*> by FINSEQ_1:47
.= d by Lm4
.= g . (the_unity_wrt g),d by A1, SETWISEO:23
.= g . (g "**" F),d by A1, A2, Def1 ;
:: thesis: verum