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