let B be AbGroup; :: thesis: multMagma(# the carrier of B, the addF of B #) is commutative Group

set G = multMagma(# the carrier of B, the addF of B #);

A1: for a, b being Element of multMagma(# the carrier of B, the addF of B #)

for x, y being Element of B st a = x & b = y holds

a * b = x + y ;

A2: ( multMagma(# the carrier of B, the addF of B #) is associative & multMagma(# the carrier of B, the addF of B #) is Group-like )

set G = multMagma(# the carrier of B, the addF of B #);

A1: for a, b being Element of multMagma(# the carrier of B, the addF of B #)

for x, y being Element of B st a = x & b = y holds

a * b = x + y ;

A2: ( multMagma(# the carrier of B, the addF of B #) is associative & multMagma(# the carrier of B, the addF of B #) is Group-like )

proof

reconsider e = 0. B as Element of multMagma(# the carrier of B, the addF of B #) ;

thus for a, b, c being Element of multMagma(# the carrier of B, the addF of B #) holds (a * b) * c = a * (b * c) :: according to GROUP_1:def 3 :: thesis: multMagma(# the carrier of B, the addF of B #) is Group-like_{1} being Element of the carrier of multMagma(# the carrier of B, the addF of B #) holds

( b_{1} * e = b_{1} & e * b_{1} = b_{1} & ex b_{2} being Element of the carrier of multMagma(# the carrier of B, the addF of B #) st

( b_{1} * b_{2} = e & b_{2} * b_{1} = e ) )

let a be Element of multMagma(# the carrier of B, the addF of B #); :: thesis: ( a * e = a & e * a = a & ex b_{1} being Element of the carrier of multMagma(# the carrier of B, the addF of B #) st

( a * b_{1} = e & b_{1} * a = e ) )

reconsider x = a as Element of B ;

thus a * e = x + (0. B)

.= a by RLVECT_1:4 ; :: thesis: ( e * a = a & ex b_{1} being Element of the carrier of multMagma(# the carrier of B, the addF of B #) st

( a * b_{1} = e & b_{1} * a = e ) )

reconsider b = - x as Element of multMagma(# the carrier of B, the addF of B #) ;

thus e * a = x + (0. B) by A1

.= a by RLVECT_1:4 ; :: thesis: ex b_{1} being Element of the carrier of multMagma(# the carrier of B, the addF of B #) st

( a * b_{1} = e & b_{1} * a = e )

take b ; :: thesis: ( a * b = e & b * a = e )

thus a * b = x + (- x)

.= e by RLVECT_1:5 ; :: thesis: b * a = e

thus b * a = x + (- x) by A1

.= e by RLVECT_1:5 ; :: thesis: verum

end;thus for a, b, c being Element of multMagma(# the carrier of B, the addF of B #) holds (a * b) * c = a * (b * c) :: according to GROUP_1:def 3 :: thesis: multMagma(# the carrier of B, the addF of B #) is Group-like

proof

take
e
; :: according to GROUP_1:def 2 :: thesis: for b
let a, b, c be Element of multMagma(# the carrier of B, the addF of B #); :: thesis: (a * b) * c = a * (b * c)

reconsider x = a, y = b, z = c as Element of B ;

thus (a * b) * c = (x + y) + z

.= x + (y + z) by RLVECT_1:def 3

.= a * (b * c) ; :: thesis: verum

end;reconsider x = a, y = b, z = c as Element of B ;

thus (a * b) * c = (x + y) + z

.= x + (y + z) by RLVECT_1:def 3

.= a * (b * c) ; :: thesis: verum

( b

( b

let a be Element of multMagma(# the carrier of B, the addF of B #); :: thesis: ( a * e = a & e * a = a & ex b

( a * b

reconsider x = a as Element of B ;

thus a * e = x + (0. B)

.= a by RLVECT_1:4 ; :: thesis: ( e * a = a & ex b

( a * b

reconsider b = - x as Element of multMagma(# the carrier of B, the addF of B #) ;

thus e * a = x + (0. B) by A1

.= a by RLVECT_1:4 ; :: thesis: ex b

( a * b

take b ; :: thesis: ( a * b = e & b * a = e )

thus a * b = x + (- x)

.= e by RLVECT_1:5 ; :: thesis: b * a = e

thus b * a = x + (- x) by A1

.= e by RLVECT_1:5 ; :: thesis: verum

now :: thesis: for a, b being Element of multMagma(# the carrier of B, the addF of B #) holds a * b = b * a

hence
multMagma(# the carrier of B, the addF of B #) is commutative Group
by A2, GROUP_1:def 12; :: thesis: verumlet a, b be Element of multMagma(# the carrier of B, the addF of B #); :: thesis: a * b = b * a

reconsider x = a, y = b as Element of B ;

thus a * b = y + x by A1

.= b * a ; :: thesis: verum

end;reconsider x = a, y = b as Element of B ;

thus a * b = y + x by A1

.= b * a ; :: thesis: verum