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

let o be BinOp of D; :: thesis: ( o is uniquely-decomposable implies o .:^2 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:
thus o .:^2 is having_a_unity by ; :: according to MONOID_0:def 9 :: thesis: for b1, b2 being Element of bool D holds
( not (o .:^2) . (b1,b2) = the_unity_wrt (o .:^2) or ( b1 = b2 & b2 = the_unity_wrt (o .:^2) ) )

let A, B be Subset of D; :: thesis: ( not (o .:^2) . (A,B) = the_unity_wrt (o .:^2) or ( A = B & B = the_unity_wrt (o .:^2) ) )
assume A3: (o .:^2) . (A,B) = the_unity_wrt (o .:^2) ; :: thesis: ( A = B & B = the_unity_wrt (o .:^2) )
set a = the_unity_wrt o;
A4: the_unity_wrt (o .:^2) = {()} by ;
set a1 = the Element of A;
set a2 = the Element of B;
o .: [:A,B:] = (o .:^2) . (A,B) by Th44;
then dom o meets [:A,B:] by ;
then (dom o) /\ [:A,B:] <> {} ;
then A5: [:A,B:] <> {} ;
then A6: A <> {} by ZFMISC_1:90;
A7: B <> {} by ;
then reconsider a1 = the Element of A, a2 = the Element of B as Element of D by ;
A8: {a1} c= A by ;
o . (a1,a2) in {()} by A3, A4, A6, A7, Th45;
then A9: o . (a1,a2) = the_unity_wrt o by TARSKI:def 1;
then A10: a2 = the_unity_wrt o by A2;
A11: A c= {()}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in {()} )
assume A12: x in A ; :: thesis: x in {()}
then reconsider c = x as Element of D ;
o . (c,a2) in {()} by A3, A4, A7, A12, Th45;
then o . (c,a2) = the_unity_wrt o by TARSKI:def 1;
then c = a2 by A2;
hence x in {()} by ; :: thesis: verum
end;
A13: B c= {()}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in {()} )
assume A14: x in B ; :: thesis: x in {()}
then reconsider c = x as Element of D ;
o . (a1,c) in {()} by A3, A4, A6, A14, Th45;
then o . (a1,c) = the_unity_wrt o by TARSKI:def 1;
then c = the_unity_wrt o by A2;
hence x in {()} by TARSKI:def 1; :: thesis: verum
end;
A15: a1 = a2 by A2, A9;
{a2} c= B by ;
then B = {()} by ;
hence ( A = B & B = the_unity_wrt (o .:^2) ) by A1, A15, A10, A8, A11, Th53; :: thesis: verum