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 )

proof

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;

A9: dom o = [:D,D:] by FUNCT_2:def 1;
thus D /\ X c= o .: [:{a},X:] :: thesis: o .: [:X,{a}:] = D /\ X

proof

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;

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

proof

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;

thus D /\ X c= o .: [:X,{a}:] :: 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;