let D be non empty set ; :: thesis: for d being Element of D

for F being BinOp of D

for u being UnOp of D st F is having_a_unity holds

(F * ((id D),u)) . ((the_unity_wrt F),d) = u . d

let d be Element of D; :: thesis: for F being BinOp of D

for u being UnOp of D st F is having_a_unity holds

(F * ((id D),u)) . ((the_unity_wrt F),d) = u . d

let F be BinOp of D; :: thesis: for u being UnOp of D st F is having_a_unity holds

(F * ((id D),u)) . ((the_unity_wrt F),d) = u . d

let u be UnOp of D; :: thesis: ( F is having_a_unity implies (F * ((id D),u)) . ((the_unity_wrt F),d) = u . d )

assume A1: F is having_a_unity ; :: thesis: (F * ((id D),u)) . ((the_unity_wrt F),d) = u . d

set e = the_unity_wrt F;

thus (F * ((id D),u)) . ((the_unity_wrt F),d) = F . ((the_unity_wrt F),(u . d)) by Th81

.= u . d by A1, SETWISEO:15 ; :: thesis: verum

for F being BinOp of D

for u being UnOp of D st F is having_a_unity holds

(F * ((id D),u)) . ((the_unity_wrt F),d) = u . d

let d be Element of D; :: thesis: for F being BinOp of D

for u being UnOp of D st F is having_a_unity holds

(F * ((id D),u)) . ((the_unity_wrt F),d) = u . d

let F be BinOp of D; :: thesis: for u being UnOp of D st F is having_a_unity holds

(F * ((id D),u)) . ((the_unity_wrt F),d) = u . d

let u be UnOp of D; :: thesis: ( F is having_a_unity implies (F * ((id D),u)) . ((the_unity_wrt F),d) = u . d )

assume A1: F is having_a_unity ; :: thesis: (F * ((id D),u)) . ((the_unity_wrt F),d) = u . d

set e = the_unity_wrt F;

thus (F * ((id D),u)) . ((the_unity_wrt F),d) = F . ((the_unity_wrt F),(u . d)) by Th81

.= u . d by A1, SETWISEO:15 ; :: thesis: verum