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 b_{1}, b_{2} being Element of bool D holds

( not (o .:^2) . (b_{1},b_{2}) = the_unity_wrt (o .:^2) or ( b_{1} = b_{2} & b_{2} = 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)}

{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

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 b

( not (o .:^2) . (b

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

A13:
B c= {(the_unity_wrt o)}
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;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

proof

A15:
a1 = a2
by A2, A9;
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;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

{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