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
proof
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;
take x ; :: according to QUANTAL1:def 3 :: thesis: for a being Element of G holds a * x = x
thus for a being Element of G holds a * x = x by TARSKI:def 1; :: thesis: verum