let i, I be set ; :: thesis: for f, g being Function

for F being Group-like associative multMagma-Family of I

for x being Element of (product F)

for G being Group

for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds

g . i = y "

let f, g be Function; :: thesis: for F being Group-like associative multMagma-Family of I

for x being Element of (product F)

for G being Group

for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds

g . i = y "

let F be Group-like associative multMagma-Family of I; :: thesis: for x being Element of (product F)

for G being Group

for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds

g . i = y "

let x be Element of (product F); :: thesis: for G being Group

for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds

g . i = y "

let G be Group; :: thesis: for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds

g . i = y "

let y be Element of G; :: thesis: ( i in I & G = F . i & f = x & g = x " & f . i = y implies g . i = y " )

assume that

A1: i in I and

A2: G = F . i and

A3: f = x and

A4: g = x " and

A5: f . i = y ; :: thesis: g . i = y "

set GP = product F;

A6: the multF of (product F) . (g,f) = (x ") * x by A3, A4

.= 1_ (product F) by GROUP_1:def 5 ;

x " in the carrier of (product F) ;

then A7: g in product (Carrier F) by A4, Def2;

then reconsider gi = g . i as Element of G by A1, A2, Lm1;

x in the carrier of (product F) ;

then A8: f in product (Carrier F) by A3, Def2;

then ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of (product F) . (g,f) & h . i = the multF of Fi . ((g . i),(f . i)) ) by A1, A7, Def2;

then A9: gi * y = 1_ G by A1, A2, A5, A6, Th6;

A10: the multF of (product F) . (f,g) = x * (x ") by A3, A4

.= 1_ (product F) by GROUP_1:def 5 ;

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of (product F) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) by A1, A8, A7, Def2;

then y * gi = 1_ G by A1, A2, A5, A10, Th6;

hence g . i = y " by A9, GROUP_1:def 5; :: thesis: verum

for F being Group-like associative multMagma-Family of I

for x being Element of (product F)

for G being Group

for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds

g . i = y "

let f, g be Function; :: thesis: for F being Group-like associative multMagma-Family of I

for x being Element of (product F)

for G being Group

for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds

g . i = y "

let F be Group-like associative multMagma-Family of I; :: thesis: for x being Element of (product F)

for G being Group

for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds

g . i = y "

let x be Element of (product F); :: thesis: for G being Group

for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds

g . i = y "

let G be Group; :: thesis: for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds

g . i = y "

let y be Element of G; :: thesis: ( i in I & G = F . i & f = x & g = x " & f . i = y implies g . i = y " )

assume that

A1: i in I and

A2: G = F . i and

A3: f = x and

A4: g = x " and

A5: f . i = y ; :: thesis: g . i = y "

set GP = product F;

A6: the multF of (product F) . (g,f) = (x ") * x by A3, A4

.= 1_ (product F) by GROUP_1:def 5 ;

x " in the carrier of (product F) ;

then A7: g in product (Carrier F) by A4, Def2;

then reconsider gi = g . i as Element of G by A1, A2, Lm1;

x in the carrier of (product F) ;

then A8: f in product (Carrier F) by A3, Def2;

then ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of (product F) . (g,f) & h . i = the multF of Fi . ((g . i),(f . i)) ) by A1, A7, Def2;

then A9: gi * y = 1_ G by A1, A2, A5, A6, Th6;

A10: the multF of (product F) . (f,g) = x * (x ") by A3, A4

.= 1_ (product F) by GROUP_1:def 5 ;

ex Fi being non empty multMagma ex h being Function st

( Fi = F . i & h = the multF of (product F) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) by A1, A8, A7, Def2;

then y * gi = 1_ G by A1, A2, A5, A10, Th6;

hence g . i = y " by A9, GROUP_1:def 5; :: thesis: verum