let A be set ; 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 ; 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; 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; ( 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
; A --> a is_a_unity_wrt (o,D) .: A
now 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);
( ((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
;
((o,D) .: A) . (f,(A --> a)) = fthus ((o,D) .: A) . (
f,
(A --> a)) =
o .: (
f,
(A --> a))
by Def2
.=
o [:] (
f,
a)
by A2, FUNCOP_1:26
.=
f
by A1, Th5
;
verum end;
hence
A --> a is_a_unity_wrt (o,D) .: A
by BINOP_1:3; verum