let A be set ; :: thesis: for D being non empty set

for o being BinOp of D st o is uniquely-decomposable holds

(o,D) .: A is uniquely-decomposable

let D be non empty set ; :: thesis: for o being BinOp of D st o is uniquely-decomposable holds

(o,D) .: A is uniquely-decomposable

let o be BinOp of D; :: thesis: ( o is uniquely-decomposable implies (o,D) .: A is uniquely-decomposable )

assume that

A1: o is having_a_unity and

A2: for a, b being Element of D st o . (a,b) = the_unity_wrt o holds

( a = b & b = the_unity_wrt o ) ; :: according to MONOID_0:def 9 :: thesis: (o,D) .: A is uniquely-decomposable

A3: the_unity_wrt ((o,D) .: A) = A --> (the_unity_wrt o) by A1, Th10;

thus (o,D) .: A is having_a_unity by A1, Th10; :: according to MONOID_0:def 9 :: thesis: for b_{1}, b_{2} being Element of Funcs (A,D) holds

( not ((o,D) .: A) . (b_{1},b_{2}) = the_unity_wrt ((o,D) .: A) or ( b_{1} = b_{2} & b_{2} = the_unity_wrt ((o,D) .: A) ) )

let f, g be Element of Funcs (A,D); :: thesis: ( not ((o,D) .: A) . (f,g) = the_unity_wrt ((o,D) .: A) or ( f = g & g = the_unity_wrt ((o,D) .: A) ) )

assume A4: ((o,D) .: A) . (f,g) = the_unity_wrt ((o,D) .: A) ; :: thesis: ( f = g & g = the_unity_wrt ((o,D) .: A) )

A5: dom (o .: (f,g)) = A by FUNCT_2:def 1;

A6: ((o,D) .: A) . (f,g) = o .: (f,g) by Def2;

dom f = A by FUNCT_2:def 1;

hence f = g by A11, A7, FUNCT_1:2; :: thesis: g = the_unity_wrt ((o,D) .: A)

dom (A --> (the_unity_wrt o)) = A ;

hence g = the_unity_wrt ((o,D) .: A) by A3, A11, A9, FUNCT_1:2; :: thesis: verum

for o being BinOp of D st o is uniquely-decomposable holds

(o,D) .: A is uniquely-decomposable

let D be non empty set ; :: thesis: for o being BinOp of D st o is uniquely-decomposable holds

(o,D) .: A is uniquely-decomposable

let o be BinOp of D; :: thesis: ( o is uniquely-decomposable implies (o,D) .: A is uniquely-decomposable )

assume that

A1: o is having_a_unity and

A2: for a, b being Element of D st o . (a,b) = the_unity_wrt o holds

( a = b & b = the_unity_wrt o ) ; :: according to MONOID_0:def 9 :: thesis: (o,D) .: A is uniquely-decomposable

A3: the_unity_wrt ((o,D) .: A) = A --> (the_unity_wrt o) by A1, Th10;

thus (o,D) .: A is having_a_unity by A1, Th10; :: according to MONOID_0:def 9 :: thesis: for b

( not ((o,D) .: A) . (b

let f, g be Element of Funcs (A,D); :: thesis: ( not ((o,D) .: A) . (f,g) = the_unity_wrt ((o,D) .: A) or ( f = g & g = the_unity_wrt ((o,D) .: A) ) )

assume A4: ((o,D) .: A) . (f,g) = the_unity_wrt ((o,D) .: A) ; :: thesis: ( f = g & g = the_unity_wrt ((o,D) .: A) )

A5: dom (o .: (f,g)) = A by FUNCT_2:def 1;

A6: ((o,D) .: A) . (f,g) = o .: (f,g) by Def2;

A7: now :: thesis: for x being object st x in A holds

f . x = g . x

f . x = g . x

let x be object ; :: thesis: ( x in A implies f . x = g . x )

assume A8: x in A ; :: thesis: f . x = g . x

then reconsider a = f . x, b = g . x as Element of D by FUNCT_2:5;

( (o .: (f,g)) . x = o . (a,b) & (A --> (the_unity_wrt o)) . x = the_unity_wrt o ) by A5, A8, FUNCOP_1:7, FUNCOP_1:22;

hence f . x = g . x by A2, A4, A6, A3; :: thesis: verum

end;assume A8: x in A ; :: thesis: f . x = g . x

then reconsider a = f . x, b = g . x as Element of D by FUNCT_2:5;

( (o .: (f,g)) . x = o . (a,b) & (A --> (the_unity_wrt o)) . x = the_unity_wrt o ) by A5, A8, FUNCOP_1:7, FUNCOP_1:22;

hence f . x = g . x by A2, A4, A6, A3; :: thesis: verum

A9: now :: thesis: for x being object st x in A holds

g . x = (A --> (the_unity_wrt o)) . x

A11:
dom g = A
by FUNCT_2:def 1;g . x = (A --> (the_unity_wrt o)) . x

let x be object ; :: thesis: ( x in A implies g . x = (A --> (the_unity_wrt o)) . x )

assume A10: x in A ; :: thesis: g . x = (A --> (the_unity_wrt o)) . x

then reconsider a = f . x, b = g . x as Element of D by FUNCT_2:5;

( (o .: (f,g)) . x = o . (a,b) & (A --> (the_unity_wrt o)) . x = the_unity_wrt o ) by A5, A10, FUNCOP_1:7, FUNCOP_1:22;

hence g . x = (A --> (the_unity_wrt o)) . x by A2, A4, A6, A3; :: thesis: verum

end;assume A10: x in A ; :: thesis: g . x = (A --> (the_unity_wrt o)) . x

then reconsider a = f . x, b = g . x as Element of D by FUNCT_2:5;

( (o .: (f,g)) . x = o . (a,b) & (A --> (the_unity_wrt o)) . x = the_unity_wrt o ) by A5, A10, FUNCOP_1:7, FUNCOP_1:22;

hence g . x = (A --> (the_unity_wrt o)) . x by A2, A4, A6, A3; :: thesis: verum

dom f = A by FUNCT_2:def 1;

hence f = g by A11, A7, FUNCT_1:2; :: thesis: g = the_unity_wrt ((o,D) .: A)

dom (A --> (the_unity_wrt o)) = A ;

hence g = the_unity_wrt ((o,D) .: A) by A3, A11, A9, FUNCT_1:2; :: thesis: verum