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 A1: ( g is having_a_unity & len F = 0 ) ; :: thesis: g "**" (F ^ <*d*>) = g . (g "**" F),d
then ( F = <*> D & {} = <*> D ) ;
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, Def1 ;
:: thesis: verum