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