let I be non empty set ; :: thesis: for F being Group-like associative multMagma-Family of I
for i being Element of I
for x being Function
for g being Element of (F . i) holds
( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) )
let F be Group-like associative multMagma-Family of I; :: thesis: for i being Element of I
for x being Function
for g being Element of (F . i) holds
( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) )
let i be Element of I; :: thesis: for x being Function
for g being Element of (F . i) holds
( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) )
let x be Function; :: thesis: for g being Element of (F . i) holds
( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) )
let g be Element of (F . i); :: thesis: ( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) )

L: now

assume R1: x = (1_ (product F)) +* (i,g) ; :: thesis: ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) )
W1: the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
thus W2: dom x = dom (1_ (product F)) by R1, FUNCT_7:32
.= I by PARTFUN1:def 4, W1 ; :: thesis: ( x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) )
dom x = dom (1_ (product F)) by R1, FUNCT_7:32;
hence x . i = g by R1, FUNCT_7:33, W2; :: thesis: for j being Element of I st j <> i holds
x . j = 1_ (F . j)
thus for j being Element of I st j <> i holds
x . j = 1_ (F . j) :: thesis: verum

proof

let j be Element of I; :: thesis: ( j <> i implies x . j = 1_ (F . j) )
assume j <> i ; :: thesis: x . j = 1_ (F . j)
then x . j = (1_ (product F)) . j by R1, FUNCT_7:34;
hence x . j = 1_ (F . j) by GROUP_7:9; :: thesis: verum

end;

end;

now

assume AS1: ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) ; :: thesis: x = (1_ (product F)) +* (i,g)
the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
then A3: dom (1_ (product F)) = I by PARTFUN1:def 4;
A2: dom ((1_ (product F)) +* (i,g)) = dom x by AS1, A3, FUNCT_7:32;
set FG = (1_ (product F)) +* (i,g);

now

let j0 be set ; :: thesis: ( j0 in dom x implies x . b₁ = ((1_ (product F)) +* (i,g)) . b₁ )
assume j0 in dom x ; :: thesis: x . b₁ = ((1_ (product F)) +* (i,g)) . b₁
then reconsider j = j0 as Element of I by AS1;

per cases ( j <> i or j = i ) ;

suppose C1: j <> i ; :: thesis: x . b₁ = ((1_ (product F)) +* (i,g)) . b₁

then x . j = 1_ (F . j) by AS1;
hence x . j0 = (1_ (product F)) . j by GROUP_7:9
.= ((1_ (product F)) +* (i,g)) . j0 by FUNCT_7:34, C1 ;
:: thesis: verum

end;

suppose j = i ; :: thesis: x . b₁ = ((1_ (product F)) +* (i,g)) . b₁

hence x . j0 = ((1_ (product F)) +* (i,g)) . j0 by FUNCT_7:33, A3, AS1; :: thesis: verum

end;

end;

end;

hence x = (1_ (product F)) +* (i,g) by A2, FUNCT_1:9; :: thesis: verum

end;

hence ( ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) ) by L; :: thesis: verum