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 ;
then reconsider b = f . x as Element of D ;
thus (o [;] (a,f)) . x = o . (a,b) by
.= f . x by ; :: thesis: verum
end;
hence o [;] (a,f) = f by ; :: 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 ;
then reconsider b = f . x as Element of D ;
thus (o [:] (f,a)) . x = o . (b,a) by
.= f . x by ; :: thesis: verum
end;
hence o [:] (f,a) = f by ; :: thesis: verum