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:18;
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