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:61
.= g . (d,d) by Th12 ; :: thesis: verum