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

x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) ) by A1; :: thesis: verum

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

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

end;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

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

hence
( ( 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);

end;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

hence
x = (1_ (product F)) +* (i,g)
by A7, FUNCT_1:2; :: thesis: verumx . j0 = ((1_ (product F)) +* (i,g)) . j0

let j0 be object ; :: thesis: ( j0 in dom x implies x . b_{1} = ((1_ (product F)) +* (i,g)) . b_{1} )

assume j0 in dom x ; :: thesis: x . b_{1} = ((1_ (product F)) +* (i,g)) . b_{1}

then reconsider j = j0 as Element of I by A5;

end;assume j0 in dom x ; :: thesis: x . b

then reconsider j = j0 as Element of I by A5;

x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) ) by A1; :: thesis: verum