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;

A5: dom (o [:] (f,a)) = A by FUNCT_2:def 1;

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

hence
o [;] (a,f) = f
by A3, A2, FUNCT_1:2; :: thesis: o [:] (f,a) = f(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;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

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

hence
o [:] (f,a) = f
by A5, A2, FUNCT_1:2; :: thesis: verum(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;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