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

let x be set ; :: 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 5;
then reconsider b = f . x as Element of D ;
thus (o [;] a,f) . x = o . a,b by A3, A4, FUNCOP_1:42
.= f . x by A1, BINOP_1:11 ; :: thesis: verum

end;

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

now

let x be set ; :: 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 5;
then reconsider b = f . x as Element of D ;
thus (o [:] f,a) . x = o . b,a by A5, A6, FUNCOP_1:35
.= f . x by A1, BINOP_1:11 ; :: thesis: verum

end;

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