let D be non empty set ; :: thesis: for F, G, H being FinSequence of D
for g being BinOp of D st g is having_a_unity & len F = 0 & len F = len G & len F = len H holds
g "**" F = g . (g "**" G),(g "**" H)
let F, G, H be FinSequence of D; :: thesis: for g being BinOp of D st g is having_a_unity & len F = 0 & len F = len G & len F = len H holds
g "**" F = g . (g "**" G),(g "**" H)
let g be BinOp of D; :: thesis: ( g is having_a_unity & len F = 0 & len F = len G & len F = len H implies g "**" F = g . (g "**" G),(g "**" H) )
assume that
A1: g is having_a_unity and
A2: ( len F = 0 & len F = len G & len F = len H ) ; :: thesis: g "**" F = g . (g "**" G),(g "**" H)
thus g "**" F = the_unity_wrt g by A1, A2, Def1
.= g . (the_unity_wrt g),(the_unity_wrt g) by A1, SETWISEO:23
.= g . (g "**" G),(the_unity_wrt g) by A1, A2, Def1
.= g . (g "**" G),(g "**" H) by A1, A2, Def1 ; :: thesis: verum