let D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( (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 ) by FUNCT_1:35;
hence ( (F * (id D),u) . d1,d2 = F . d1,(u . d2) & (F * u,(id D)) . d1,d2 = F . (u . d1),d2 ) by Th86; :: thesis: verum