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) )

A1: now :: thesis: ( x = (1_ (product F)) +* (i,g) implies ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) )

assume A2: 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) ) )
A3: the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
thus A4: dom x = dom (1_ (product F)) by A2, FUNCT_7:30
.= I by A3, PARTFUN1:def 2 ; :: 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 A2, FUNCT_7:30;
hence x . i = g by A2, A4, FUNCT_7:31; :: 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 A2, FUNCT_7:32;
hence x . j = 1_ (F . j) by GROUP_7:6; :: thesis: verum

end;

end;

now :: thesis: ( dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) implies x = (1_ (product F)) +* (i,g) )

assume A5: ( 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 A6: dom (1_ (product F)) = I by PARTFUN1:def 2;
A7: dom ((1_ (product F)) +* (i,g)) = dom x by A5, A6, FUNCT_7:30;
set FG = (1_ (product F)) +* (i,g);

now :: thesis: for j0 being object st j0 in dom x holds
x . j0 = ((1_ (product F)) +* (i,g)) . j0

let j0 be object ; :: 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 A5;

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

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

then x . j = 1_ (F . j) by A5;
hence x . j0 = (1_ (product F)) . j by GROUP_7:6
.= ((1_ (product F)) +* (i,g)) . j0 by A8, FUNCT_7:32 ;
:: 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 A6, A5, FUNCT_7:31; :: thesis: verum

end;

end;

end;

hence x = (1_ (product F)) +* (i,g) by A7, FUNCT_1:2; :: 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 A1; :: thesis: verum