let A be set ; :: thesis: for D being non empty set
for a being Element of D
for o being BinOp of D
for f being Function of A,D st a is_a_unity_wrt o holds
( o [;] (a,f) = f & o [:] (f,a) = f )
let D be non empty set ; :: thesis: for a being Element of D
for o being BinOp of D
for f being Function of A,D st a is_a_unity_wrt o holds
( o [;] (a,f) = f & o [:] (f,a) = f )
let a be Element of D; :: thesis: for o being BinOp of D
for f being Function of A,D st a is_a_unity_wrt o holds
( o [;] (a,f) = f & o [:] (f,a) = f )
let o be BinOp of D; :: thesis: for f being Function of A,D st a is_a_unity_wrt o holds
( o [;] (a,f) = f & o [:] (f,a) = f )
let f be Function of A,D; :: thesis: ( a is_a_unity_wrt o implies ( o [;] (a,f) = f & o [:] (f,a) = f ) )
assume A1: a is_a_unity_wrt o ; :: thesis: ( o [;] (a,f) = f & o [:] (f,a) = f )
A2: dom f = A by FUNCT_2:def 1;
A3: dom (o [;] (a,f)) = A by FUNCT_2:def 1;

now :: thesis: for x being object st x in A holds
(o [;] (a,f)) . x = f . x

let x be object ; :: thesis: ( x in A implies (o [;] (a,f)) . x = f . x )
assume A4: x in A ; :: thesis: (o [;] (a,f)) . x = f . x
then f . x in rng f by A2, FUNCT_1:def 3;
then reconsider b = f . x as Element of D ;
thus (o [;] (a,f)) . x = o . (a,b) by A3, A4, FUNCOP_1:32
.= f . x by A1, BINOP_1:3 ; :: thesis: verum

end;

hence o [;] (a,f) = f by A3, A2, FUNCT_1:2; :: thesis: o [:] (f,a) = f
A5: dom (o [:] (f,a)) = A by FUNCT_2:def 1;

now :: thesis: for x being object st x in A holds
(o [:] (f,a)) . x = f . x

let x be object ; :: thesis: ( x in A implies (o [:] (f,a)) . x = f . x )
assume A6: x in A ; :: thesis: (o [:] (f,a)) . x = f . x
then f . x in rng f by A2, FUNCT_1:def 3;
then reconsider b = f . x as Element of D ;
thus (o [:] (f,a)) . x = o . (b,a) by A5, A6, FUNCOP_1:27
.= f . x by A1, BINOP_1:3 ; :: thesis: verum

end;

hence o [:] (f,a) = f by A5, A2, FUNCT_1:2; :: thesis: verum