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 A1: ( o is having_a_unity & ( 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
hence o,D .: A is having_a_unity by Th11; :: according to MONOID_0:def 9 :: thesis: for b₁, b₂ being Element of Funcs A,D holds
( not (o,D .: A) . b₁,b₂ = the_unity_wrt (o,D .: A) or ( b₁ = b₂ & b₂ = 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 A2: (o,D .: A) . f,g = the_unity_wrt (o,D .: A) ; :: thesis: ( f = g & g = the_unity_wrt (o,D .: A) )
A3: ( (o,D .: A) . f,g = o .: f,g & the_unity_wrt (o,D .: A) = A --> (the_unity_wrt o) ) by A1, Def2, Th11;
A4: ( dom (A --> (the_unity_wrt o)) = A & dom f = A & dom g = A & dom (o .: f,g) = A ) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in A implies f . x = g . x )
assume A5: x in A ; :: thesis: f . x = g . x
then reconsider a = f . x, b = g . x as Element of D by FUNCT_2:7;
( (o .: f,g) . x = o . a,b & (A --> (the_unity_wrt o)) . x = the_unity_wrt o ) by A4, A5, FUNCOP_1:13, FUNCOP_1:28;
hence f . x = g . x by A1, A2, A3; :: thesis: verum

end;

hence f = g by A4, FUNCT_1:9; :: thesis: g = the_unity_wrt (o,D .: A)

now

let x be set ; :: thesis: ( x in A implies g . x = (A --> (the_unity_wrt o)) . x )
assume A6: 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:7;
( (o .: f,g) . x = o . a,b & (A --> (the_unity_wrt o)) . x = the_unity_wrt o ) by A4, A6, FUNCOP_1:13, FUNCOP_1:28;
hence g . x = (A --> (the_unity_wrt o)) . x by A1, A2, A3; :: thesis: verum

end;

hence g = the_unity_wrt (o,D .: A) by A3, A4, FUNCT_1:9; :: thesis: verum