let D be non empty set ; for d1, d2 being Element of D
for F being BinOp of D
for u being Function of D,D holds
( (F * ((id D),u)) . (d1,d2) = F . (d1,(u . d2)) & (F * (u,(id D))) . (d1,d2) = F . ((u . d1),d2) )
let d1, d2 be Element of D; for F being BinOp of D
for u being Function of D,D holds
( (F * ((id D),u)) . (d1,d2) = F . (d1,(u . d2)) & (F * (u,(id D))) . (d1,d2) = F . ((u . d1),d2) )
let F be BinOp of D; for u being Function of D,D holds
( (F * ((id D),u)) . (d1,d2) = F . (d1,(u . d2)) & (F * (u,(id D))) . (d1,d2) = F . ((u . d1),d2) )
let u be Function of D,D; ( (F * ((id D),u)) . (d1,d2) = F . (d1,(u . d2)) & (F * (u,(id D))) . (d1,d2) = F . ((u . d1),d2) )
( (id D) . d1 = d1 & (id D) . d2 = d2 )
;
hence
( (F * ((id D),u)) . (d1,d2) = F . (d1,(u . d2)) & (F * (u,(id D))) . (d1,d2) = F . ((u . d1),d2) )
by Th80; verum