let H be 1 -element addMagma ; :: thesis: ( H is addGroup-like & H is add-associative & H is Abelian )
thus H is addGroup-like :: thesis: ( H is add-associative & H is Abelian )
proof
now :: thesis: ex e being Element of H st
for h being Element of H holds
( h + e = h & e + h = h & ex g being Element of H st
( h + g = e & g + h = e ) )
set e = the Element of H;
take e = the Element of H; :: thesis: for h being Element of H holds
( h + e = h & e + h = h & ex g being Element of H st
( h + g = e & g + h = e ) )
let h be Element of H; :: thesis: ( h + e = h & e + h = h & ex g being Element of H st
( h + g = e & g + h = e ) )
thus ( h + e = h & e + h = h ) by STRUCT_0:def 10; :: thesis: ex g being Element of H st
( h + g = e & g + h = e )
take g = e; :: thesis: ( h + g = e & g + h = e )
thus ( h + g = e & g + h = e ) by STRUCT_0:def 10; :: thesis: verum
end;
hence H is addGroup-like ; :: thesis: verum
end;
thus H is add-associative by STRUCT_0:def 10; :: thesis: H is Abelian
thus H is Abelian by STRUCT_0:def 10; :: thesis: verum