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 and
A3: len F = len G and
A4: 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:15
.= g . ((g "**" G),(the_unity_wrt g)) by A1, A2, A3, Def1
.= g . ((g "**" G),(g "**" H)) by A1, A2, A4, Def1 ; :: thesis: verum