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 or len F >= 1 ) 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 or len F >= 1 ) 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 or len F >= 1 ) holds
g "**" (F ^ <*d*>) = g . ((g "**" F),d)
let g be BinOp of D; :: thesis: ( ( g is having_a_unity or len F >= 1 ) implies g "**" (F ^ <*d*>) = g . ((g "**" F),d) )
( len F >= 1 or len F = 0 ) by NAT_1:14;
hence ( ( g is having_a_unity or len F >= 1 ) implies g "**" (F ^ <*d*>) = g . ((g "**" F),d) ) by Lm5, Lm6; :: thesis: verum