A1: now :: thesis: for g being Element of G st g in {(1_ G)} holds

g " in {(1_ G)}

g " in {(1_ G)}

let g be Element of G; :: thesis: ( g in {(1_ G)} implies g " in {(1_ G)} )

assume g in {(1_ G)} ; :: thesis: g " in {(1_ G)}

then g = 1_ G by TARSKI:def 1;

then g " = 1_ G by GROUP_1:8;

hence g " in {(1_ G)} by TARSKI:def 1; :: thesis: verum

end;assume g in {(1_ G)} ; :: thesis: g " in {(1_ G)}

then g = 1_ G by TARSKI:def 1;

then g " = 1_ G by GROUP_1:8;

hence g " in {(1_ G)} by TARSKI:def 1; :: thesis: verum

now :: thesis: for g1, g2 being Element of G st g1 in {(1_ G)} & g2 in {(1_ G)} holds

g1 * g2 in {(1_ G)}

hence
ex bg1 * g2 in {(1_ G)}

let g1, g2 be Element of G; :: thesis: ( g1 in {(1_ G)} & g2 in {(1_ G)} implies g1 * g2 in {(1_ G)} )

assume ( g1 in {(1_ G)} & g2 in {(1_ G)} ) ; :: thesis: g1 * g2 in {(1_ G)}

then ( g1 = 1_ G & g2 = 1_ G ) by TARSKI:def 1;

then g1 * g2 = 1_ G by GROUP_1:def 4;

hence g1 * g2 in {(1_ G)} by TARSKI:def 1; :: thesis: verum

end;assume ( g1 in {(1_ G)} & g2 in {(1_ G)} ) ; :: thesis: g1 * g2 in {(1_ G)}

then ( g1 = 1_ G & g2 = 1_ G ) by TARSKI:def 1;

then g1 * g2 = 1_ G by GROUP_1:def 4;

hence g1 * g2 in {(1_ G)} by TARSKI:def 1; :: thesis: verum