let I be non empty set ; :: thesis: for F being Group-like associative multMagma-Family of I
for i being Element of I
for g1 being Element of ()
for z1 being Element of (F . i) st g1 = (1_ ()) +* (i,z1) holds
g1 " = (1_ ()) +* (i,(z1 "))

let F be Group-like associative multMagma-Family of I; :: thesis: for i being Element of I
for g1 being Element of ()
for z1 being Element of (F . i) st g1 = (1_ ()) +* (i,z1) holds
g1 " = (1_ ()) +* (i,(z1 "))

let i be Element of I; :: thesis: for g1 being Element of ()
for z1 being Element of (F . i) st g1 = (1_ ()) +* (i,z1) holds
g1 " = (1_ ()) +* (i,(z1 "))

let g1 be Element of (); :: thesis: for z1 being Element of (F . i) st g1 = (1_ ()) +* (i,z1) holds
g1 " = (1_ ()) +* (i,(z1 "))

let z1 be Element of (F . i); :: thesis: ( g1 = (1_ ()) +* (i,z1) implies g1 " = (1_ ()) +* (i,(z1 ")) )
assume A1: g1 = (1_ ()) +* (i,z1) ; :: thesis: g1 " = (1_ ()) +* (i,(z1 "))
set x1 = g1;
A2: ( g1 = g1 & dom g1 = I & g1 . i = z1 & ( for j being Element of I st j <> i holds
g1 . j = 1_ (F . j) ) ) by ;
set x12 = g1 " ;
the carrier of () = product () by GROUP_7:def 2;
then A3: dom (g1 ") = I by PARTFUN1:def 2;
A4: (g1 ") . i = z1 " by ;
A5: for j being Element of I st i <> j holds
(g1 ") . j = 1_ (F . j)
proof
let j be Element of I; :: thesis: ( i <> j implies (g1 ") . j = 1_ (F . j) )
assume i <> j ; :: thesis: (g1 ") . j = 1_ (F . j)
then g1 . j = 1_ (F . j) by ;
hence (g1 ") . j = (1_ (F . j)) " by GROUP_7:8
.= 1_ (F . j) by GROUP_1:8 ;
:: thesis: verum
end;
thus g1 " = (1_ ()) +* (i,(z1 ")) by A3, A4, A5, Th1; :: thesis: verum