let D be non empty set ; :: thesis: for d being Element of D
for g being BinOp of D holds g "**" (2 |-> d) = g . d,d
let d be Element of D; :: thesis: for g being BinOp of D holds g "**" (2 |-> d) = g . d,d
let g be BinOp of D; :: thesis: g "**" (2 |-> d) = g . d,d
thus g "**" (2 |-> d) = g "**" <*d,d*> by FINSEQ_2:75
.= g . d,d by Th13 ; :: thesis: verum