let I be non empty set ; :: thesis: for F being Group-Family of I
for G being Group
for f being Homomorphism-Family of G,F
for g being Element of G holds
( ( for i being Element of I holds ((product f) . g) . i = 1_ (F . i) ) iff (product f) . g = 1_ (product F) )
let F be Group-Family of I; :: thesis: for G being Group
for f being Homomorphism-Family of G,F
for g being Element of G holds
( ( for i being Element of I holds ((product f) . g) . i = 1_ (F . i) ) iff (product f) . g = 1_ (product F) )
let G be Group; :: thesis: for f being Homomorphism-Family of G,F
for g being Element of G holds
( ( for i being Element of I holds ((product f) . g) . i = 1_ (F . i) ) iff (product f) . g = 1_ (product F) )
let f be Homomorphism-Family of G,F; :: thesis: for g being Element of G holds
( ( for i being Element of I holds ((product f) . g) . i = 1_ (F . i) ) iff (product f) . g = 1_ (product F) )
let g be Element of G; :: thesis: ( ( for i being Element of I holds ((product f) . g) . i = 1_ (F . i) ) iff (product f) . g = 1_ (product F) )
thus ( ( for i being Element of I holds ((product f) . g) . i = 1_ (F . i) ) implies (product f) . g = 1_ (product F) ) :: thesis: ( (product f) . g = 1_ (product F) implies for i being Element of I holds ((product f) . g) . i = 1_ (F . i) )

proof

assume A1: for i being Element of I holds ((product f) . g) . i = 1_ (F . i) ; :: thesis: (product f) . g = 1_ (product F)
set s = (product f) . g;
A2: for i being set st i in I holds
ex FG being non empty Group-like multMagma st
( FG = F . i & ((product f) . g) . i = 1_ FG )

proof

let i be set ; :: thesis: ( i in I implies ex FG being non empty Group-like multMagma st
( FG = F . i & ((product f) . g) . i = 1_ FG ) )
assume i in I ; :: thesis: ex FG being non empty Group-like multMagma st
( FG = F . i & ((product f) . g) . i = 1_ FG )
then reconsider ii = i as Element of I ;
take FG = F . ii; :: thesis: ( FG = F . i & ((product f) . g) . i = 1_ FG )
thus ( FG = F . i & ((product f) . g) . i = 1_ FG ) by A1; :: thesis: verum

end;

(product f) . g is ManySortedSet of I

proof

(product f) . g is Element of product (Carrier F) by GROUP_7:def 2;
hence (product f) . g is ManySortedSet of I ; :: thesis: verum

end;

hence (product f) . g = 1_ (product F) by A2, GROUP_7:5; :: thesis: verum

end;

thus ( (product f) . g = 1_ (product F) implies for i being Element of I holds ((product f) . g) . i = 1_ (F . i) ) by GROUP_7:6; :: thesis: verum