let D be non empty set ; :: thesis: for F being FinSequence of D
for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) & 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 ( g is having_a_unity or len F >= 1 ) & 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: ( ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative implies g "**" F = g $$ (findom F),((NAT --> (the_unity_wrt g)) +* F) )
( len F = 0 or len F >= 1 ) by NAT_1:14;
hence ( ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative implies g "**" F = g $$ (findom F),((NAT --> (the_unity_wrt g)) +* F) ) by Lm1, Lm2; :: thesis: verum