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 )
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
proof
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;
take e ; :: according to GROUP_1:def 2 :: thesis: for b1 being Element of the carrier of multMagma(# the carrier of B, the addF of B #) holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of multMagma(# the carrier of B, the addF of B #) st
( b1 * b2 = e & b2 * b1 = e ) )
let a be Element of multMagma(# the carrier of B, the addF of B #); :: thesis: ( a * e = a & e * a = a & ex b1 being Element of the carrier of multMagma(# the carrier of B, the addF of B #) st
( a * b1 = e & b1 * 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 b1 being Element of the carrier of multMagma(# the carrier of B, the addF of B #) st
( a * b1 = e & b1 * 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 b1 being Element of the carrier of multMagma(# the carrier of B, the addF of B #) st
( a * b1 = e & b1 * 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;
now :: thesis: for a, b being Element of multMagma(# the carrier of B, the addF of B #) holds a * b = b * a
let 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;
hence multMagma(# the carrier of B, the addF of B #) is commutative Group by A2, GROUP_1:def 12; :: thesis: verum