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:34
.= d by Lm4
.= g . ((the_unity_wrt g),d) by A1, SETWISEO:15
.= g . ((g "**" F),d) by A1, A2, Def1 ;
:: thesis: verum