let A be set ; :: thesis: for D being non empty set
for a being Element of D
for o being BinOp of D st a is_a_unity_wrt o holds
A --> a is_a_unity_wrt (o,D) .: A
let D be non empty set ; :: thesis: for a being Element of D
for o being BinOp of D st a is_a_unity_wrt o holds
A --> a is_a_unity_wrt (o,D) .: A
let a be Element of D; :: thesis: for o being BinOp of D st a is_a_unity_wrt o holds
A --> a is_a_unity_wrt (o,D) .: A
let o be BinOp of D; :: thesis: ( a is_a_unity_wrt o implies A --> a is_a_unity_wrt (o,D) .: A )
set e = A --> a;
set F = (o,D) .: A;
assume A1: a is_a_unity_wrt o ; :: thesis: A --> a is_a_unity_wrt (o,D) .: A

now :: thesis: for f being Element of Funcs (A,D) holds
( ((o,D) .: A) . ((A --> a),f) = f & ((o,D) .: A) . (f,(A --> a)) = f )

let f be Element of Funcs (A,D); :: thesis: ( ((o,D) .: A) . ((A --> a),f) = f & ((o,D) .: A) . (f,(A --> a)) = f )
A2: dom f = A by FUNCT_2:def 1;
thus ((o,D) .: A) . ((A --> a),f) = o .: ((A --> a),f) by Def2
.= o [;] (a,f) by A2, FUNCOP_1:31
.= f by A1, Th5 ; :: thesis: ((o,D) .: A) . (f,(A --> a)) = f
thus ((o,D) .: A) . (f,(A --> a)) = o .: (f,(A --> a)) by Def2
.= o [:] (f,a) by A2, FUNCOP_1:26
.= f by A1, Th5 ; :: thesis: verum

end;

hence A --> a is_a_unity_wrt (o,D) .: A by BINOP_1:3; :: thesis: verum