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: o .:^2 is uniquely-decomposable
thus o .:^2 is having_a_unity by A1, Th54; :: according to MONOID_0:def 9 :: thesis: for b₁, b₂ being Element of bool D holds
( not (o .:^2 ) . b₁,b₂ = the_unity_wrt (o .:^2 ) or ( b₁ = b₂ & b₂ = the_unity_wrt (o .:^2 ) ) )
set a = the_unity_wrt o;
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 ) )
A4: ( the_unity_wrt (o .:^2 ) = {(the_unity_wrt o)} & o .: [:A,B:] = (o .:^2 ) . A,B & the_unity_wrt o in {(the_unity_wrt o)} ) by A1, Th45, Th54, TARSKI:def 1;
then dom o meets [:A,B:] by A3, RELAT_1:151;
then (dom o) /\ [:A,B:] <> {} by XBOOLE_0:def 7;
then [:A,B:] <> {} ;
then A5: ( A <> {} & B <> {} & A c= D & B c= D ) by ZFMISC_1:113;
consider a1 being Element of A, a2 being Element of B;
reconsider a1 = a1, a2 = a2 as Element of D by A5, TARSKI:def 3;
o . a1,a2 in {(the_unity_wrt o)} by A3, A4, A5, Th46;
then o . a1,a2 = the_unity_wrt o by TARSKI:def 1;
then A6: ( a1 = a2 & a2 = the_unity_wrt o & {a1} c= A & {a2} c= B ) by A2, A5, ZFMISC_1:37;
A7: A c= {(the_unity_wrt o)}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in {(the_unity_wrt o)} )
assume A8: x in A ; :: thesis: x in {(the_unity_wrt o)}
then reconsider c = x as Element of D ;
o . c,a2 in {(the_unity_wrt o)} by A3, A4, A5, A8, Th46;
then o . c,a2 = the_unity_wrt o by TARSKI:def 1;
then c = a2 by A2;
hence x in {(the_unity_wrt o)} by A6, TARSKI:def 1; :: thesis: verum

end;

B c= {(the_unity_wrt o)}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in {(the_unity_wrt o)} )
assume A9: x in B ; :: thesis: x in {(the_unity_wrt o)}
then reconsider c = x as Element of D ;
o . a1,c in {(the_unity_wrt o)} by A3, A4, A5, A9, Th46;
then o . a1,c = the_unity_wrt o by TARSKI:def 1;
then c = the_unity_wrt o by A2;
hence x in {(the_unity_wrt o)} by TARSKI:def 1; :: thesis: verum

end;

then ( A = {(the_unity_wrt o)} & B = {(the_unity_wrt o)} ) by A6, A7, XBOOLE_0:def 10;
hence ( A = B & B = the_unity_wrt (o .:^2 ) ) by A1, Th54; :: thesis: verum