let X be set ; :: thesis: for D being non empty set

for o being BinOp of D

for a being Element of D st a is_a_unity_wrt o holds

( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X )

let D be non empty set ; :: thesis: for o being BinOp of D

for a being Element of D st a is_a_unity_wrt o holds

( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X )

let o be BinOp of D; :: thesis: for a being Element of D st a is_a_unity_wrt o holds

( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X )

let a be Element of D; :: thesis: ( a is_a_unity_wrt o implies ( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X ) )

assume A1: a is_a_unity_wrt o ; :: thesis: ( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X )

thus o .: [:{a},X:] c= D /\ X :: according to XBOOLE_0:def 10 :: thesis: ( D /\ X c= o .: [:{a},X:] & o .: [:X,{a}:] = D /\ X )

thus D /\ X c= o .: [:{a},X:] :: thesis: o .: [:X,{a}:] = D /\ X

for o being BinOp of D

for a being Element of D st a is_a_unity_wrt o holds

( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X )

let D be non empty set ; :: thesis: for o being BinOp of D

for a being Element of D st a is_a_unity_wrt o holds

( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X )

let o be BinOp of D; :: thesis: for a being Element of D st a is_a_unity_wrt o holds

( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X )

let a be Element of D; :: thesis: ( a is_a_unity_wrt o implies ( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X ) )

assume A1: a is_a_unity_wrt o ; :: thesis: ( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X )

thus o .: [:{a},X:] c= D /\ X :: according to XBOOLE_0:def 10 :: thesis: ( D /\ X c= o .: [:{a},X:] & o .: [:X,{a}:] = D /\ X )

proof

A9:
dom o = [:D,D:]
by FUNCT_2:def 1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in o .: [:{a},X:] or x in D /\ X )

assume x in o .: [:{a},X:] ; :: thesis: x in D /\ X

then consider y being object such that

A2: y in dom o and

A3: y in [:{a},X:] and

A4: x = o . y by FUNCT_1:def 6;

reconsider y = y as Element of [:D,D:] by A2;

A5: x = o . ((y `1),(y `2)) by A4, MCART_1:21;

A6: y = [(y `1),(y `2)] by MCART_1:21;

then y `1 in {a} by A3, ZFMISC_1:87;

then A7: y `1 = a by TARSKI:def 1;

A8: o . (a,(y `2)) = y `2 by A1, BINOP_1:3;

y `2 in X by A3, A6, ZFMISC_1:87;

hence x in D /\ X by A5, A8, A7, XBOOLE_0:def 4; :: thesis: verum

end;assume x in o .: [:{a},X:] ; :: thesis: x in D /\ X

then consider y being object such that

A2: y in dom o and

A3: y in [:{a},X:] and

A4: x = o . y by FUNCT_1:def 6;

reconsider y = y as Element of [:D,D:] by A2;

A5: x = o . ((y `1),(y `2)) by A4, MCART_1:21;

A6: y = [(y `1),(y `2)] by MCART_1:21;

then y `1 in {a} by A3, ZFMISC_1:87;

then A7: y `1 = a by TARSKI:def 1;

A8: o . (a,(y `2)) = y `2 by A1, BINOP_1:3;

y `2 in X by A3, A6, ZFMISC_1:87;

hence x in D /\ X by A5, A8, A7, XBOOLE_0:def 4; :: thesis: verum

thus D /\ X c= o .: [:{a},X:] :: thesis: o .: [:X,{a}:] = D /\ X

proof

thus
o .: [:X,{a}:] c= D /\ X
:: according to XBOOLE_0:def 10 :: thesis: D /\ X c= o .: [:X,{a}:]
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D /\ X or x in o .: [:{a},X:] )

A10: a in {a} by TARSKI:def 1;

assume A11: x in D /\ X ; :: thesis: x in o .: [:{a},X:]

then reconsider d = x as Element of D by XBOOLE_0:def 4;

A12: x = o . (a,d) by A1, BINOP_1:3

.= o . [a,x] ;

x in X by A11, XBOOLE_0:def 4;

then [a,d] in [:{a},X:] by A10, ZFMISC_1:87;

hence x in o .: [:{a},X:] by A9, A12, FUNCT_1:def 6; :: thesis: verum

end;A10: a in {a} by TARSKI:def 1;

assume A11: x in D /\ X ; :: thesis: x in o .: [:{a},X:]

then reconsider d = x as Element of D by XBOOLE_0:def 4;

A12: x = o . (a,d) by A1, BINOP_1:3

.= o . [a,x] ;

x in X by A11, XBOOLE_0:def 4;

then [a,d] in [:{a},X:] by A10, ZFMISC_1:87;

hence x in o .: [:{a},X:] by A9, A12, FUNCT_1:def 6; :: thesis: verum

proof

thus
D /\ X c= o .: [:X,{a}:]
:: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in o .: [:X,{a}:] or x in D /\ X )

assume x in o .: [:X,{a}:] ; :: thesis: x in D /\ X

then consider y being object such that

A13: y in dom o and

A14: y in [:X,{a}:] and

A15: x = o . y by FUNCT_1:def 6;

reconsider y = y as Element of [:D,D:] by A13;

A16: x = o . ((y `1),(y `2)) by A15, MCART_1:21;

A17: y = [(y `1),(y `2)] by MCART_1:21;

then y `2 in {a} by A14, ZFMISC_1:87;

then A18: y `2 = a by TARSKI:def 1;

A19: o . ((y `1),a) = y `1 by A1, BINOP_1:3;

y `1 in X by A14, A17, ZFMISC_1:87;

hence x in D /\ X by A16, A19, A18, XBOOLE_0:def 4; :: thesis: verum

end;assume x in o .: [:X,{a}:] ; :: thesis: x in D /\ X

then consider y being object such that

A13: y in dom o and

A14: y in [:X,{a}:] and

A15: x = o . y by FUNCT_1:def 6;

reconsider y = y as Element of [:D,D:] by A13;

A16: x = o . ((y `1),(y `2)) by A15, MCART_1:21;

A17: y = [(y `1),(y `2)] by MCART_1:21;

then y `2 in {a} by A14, ZFMISC_1:87;

then A18: y `2 = a by TARSKI:def 1;

A19: o . ((y `1),a) = y `1 by A1, BINOP_1:3;

y `1 in X by A14, A17, ZFMISC_1:87;

hence x in D /\ X by A16, A19, A18, XBOOLE_0:def 4; :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D /\ X or x in o .: [:X,{a}:] )

A20: a in {a} by TARSKI:def 1;

assume A21: x in D /\ X ; :: thesis: x in o .: [:X,{a}:]

then reconsider d = x as Element of D by XBOOLE_0:def 4;

A22: x = o . (d,a) by A1, BINOP_1:3

.= o . [x,a] ;

x in X by A21, XBOOLE_0:def 4;

then [d,a] in [:X,{a}:] by A20, ZFMISC_1:87;

hence x in o .: [:X,{a}:] by A9, A22, FUNCT_1:def 6; :: thesis: verum

end;A20: a in {a} by TARSKI:def 1;

assume A21: x in D /\ X ; :: thesis: x in o .: [:X,{a}:]

then reconsider d = x as Element of D by XBOOLE_0:def 4;

A22: x = o . (d,a) by A1, BINOP_1:3

.= o . [x,a] ;

x in X by A21, XBOOLE_0:def 4;

then [d,a] in [:X,{a}:] by A20, ZFMISC_1:87;

hence x in o .: [:X,{a}:] by A9, A22, FUNCT_1:def 6; :: thesis: verum