let D be non empty set ; 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; 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; ( 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 )
; 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
; verum