let G be non empty multMagma ; ( G is invertible iff for a, b being Element of G ex r, l being Element of G st
( a * r = b & l * a = b ) )
thus
( G is invertible implies for a, b being Element of G ex r, l being Element of G st
( a * r = b & l * a = b ) )
( ( for a, b being Element of G ex r, l being Element of G st
( a * r = b & l * a = b ) ) implies G is invertible )proof
assume A1:
for
a,
b being
Element of
G ex
r,
l being
Element of
G st
(
H2(
G)
. (
a,
r)
= b &
H2(
G)
. (
l,
a)
= b )
;
MONOID_0:def 5,
MONOID_0:def 16 for a, b being Element of G ex r, l being Element of G st
( a * r = b & l * a = b )
let a,
b be
Element of
G;
ex r, l being Element of G st
( a * r = b & l * a = b )
consider r,
l being
Element of
G such that A2:
(
H2(
G)
. (
a,
r)
= b &
H2(
G)
. (
l,
a)
= b )
by A1;
take
r
;
ex l being Element of G st
( a * r = b & l * a = b )
take
l
;
( a * r = b & l * a = b )
thus
(
a * r = b &
l * a = b )
by A2;
verum
end;
assume A3:
for a, b being Element of G ex r, l being Element of G st
( a * r = b & l * a = b )
; G is invertible
let a be Element of G; MONOID_0:def 5,MONOID_0:def 16 for b being Element of the carrier of G ex r, l being Element of the carrier of G st
( the multF of G . (a,r) = b & the multF of G . (l,a) = b )
let b be Element of G; ex r, l being Element of the carrier of G st
( the multF of G . (a,r) = b & the multF of G . (l,a) = b )
consider r, l being Element of G such that
A4:
( a * r = b & l * a = b )
by A3;
take
r
; ex l being Element of the carrier of G st
( the multF of G . (a,r) = b & the multF of G . (l,a) = b )
take
l
; ( the multF of G . (a,r) = b & the multF of G . (l,a) = b )
thus
( the multF of G . (a,r) = b & the multF of G . (l,a) = b )
by A4; verum