set x = the set ;

set f = the BinOp of { the set };

take G = multMagma(# { the set }, the BinOp of { the set } #); :: thesis: G is with_zero

reconsider x = the set as Element of G by TARSKI:def 1;

thus G is with_left-zero :: according to QUANTAL1:def 4 :: thesis: G is with_right-zero

thus for a being Element of G holds a * x = x by TARSKI:def 1; :: thesis: verum

set f = the BinOp of { the set };

take G = multMagma(# { the set }, the BinOp of { the set } #); :: thesis: G is with_zero

reconsider x = the set as Element of G by TARSKI:def 1;

thus G is with_left-zero :: according to QUANTAL1:def 4 :: thesis: G is with_right-zero

proof

take
x
; :: according to QUANTAL1:def 3 :: thesis: for a being Element of G holds a * x = x
take
x
; :: according to QUANTAL1:def 2 :: thesis: for b being Element of G holds x * b = x

thus for b being Element of G holds x * b = x by TARSKI:def 1; :: thesis: verum

end;thus for b being Element of G holds x * b = x by TARSKI:def 1; :: thesis: verum

thus for a being Element of G holds a * x = x by TARSKI:def 1; :: thesis: verum