let D be non empty set ; :: thesis: for F being FinSequence of D
for g being BinOp of D st len F = 0 & g is having_a_unity & g is associative & g is commutative holds
g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))
let F be FinSequence of D; :: thesis: for g being BinOp of D st len F = 0 & g is having_a_unity & g is associative & g is commutative holds
g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))
let g be BinOp of D; :: thesis: ( len F = 0 & g is having_a_unity & g is associative & g is commutative implies g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) )
assume that
A1: len F = 0 and
A2: g is having_a_unity and
A3: ( g is associative & g is commutative ) ; :: thesis: g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))
F = {} by A1;
then A4: dom F = {}. NAT ;
thus g "**" F = the_unity_wrt g by A1, A2, Def1
.= g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) by A2, A3, A4, SETWISEO:31 ; :: thesis: verum