let I, i be set ; :: thesis: for f, g being Function
for F being Group-like associative multMagma-Family of
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
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 ; :: 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 A1: ( i in I & G = F . i & f = x & g = x " & f . i = y ) ; :: thesis: g . i = y "
set GP = product F;
( x in the carrier of (product F) & x " in the carrier of (product F) ) ;
then A2: ( f in product (Carrier F) & g in product (Carrier F) ) by A1, Def2;
then reconsider gi = g . i as Element of G by A1, Lm1;
consider Fi being non empty multMagma , h being Function such that
A3: ( Fi = F . i & h = the multF of (product F) . f,g & h . i = the multF of Fi . (f . i),(g . i) ) by A1, A2, Def2;
the multF of (product F) . f,g = x * (x " ) by A1
.= 1_ (product F) by GROUP_1:def 6 ;
then A4: y * gi = 1_ G by A1, A3, Th9;
consider Fi being non empty multMagma , h being Function such that
A5: ( Fi = F . i & h = the multF of (product F) . g,f & h . i = the multF of Fi . (g . i),(f . i) ) by A1, A2, Def2;
the multF of (product F) . g,f = (x " ) * x by A1
.= 1_ (product F) by GROUP_1:def 6 ;
then gi * y = 1_ G by A1, A5, Th9;
hence g . i = y " by A4, GROUP_1:def 6; :: thesis: verum