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
( g in Ker (product f) iff for i being Element of I holds g in Ker (f . i) )
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
( g in Ker (product f) iff for i being Element of I holds g in Ker (f . i) )
let G be Group; :: thesis: for f being Homomorphism-Family of G,F
for g being Element of G holds
( g in Ker (product f) iff for i being Element of I holds g in Ker (f . i) )
let f be Homomorphism-Family of G,F; :: thesis: for g being Element of G holds
( g in Ker (product f) iff for i being Element of I holds g in Ker (f . i) )
let g be Element of G; :: thesis: ( g in Ker (product f) iff for i being Element of I holds g in Ker (f . i) )
thus ( g in Ker (product f) implies for i being Element of I holds g in Ker (f . i) ) :: thesis: ( ( for i being Element of I holds g in Ker (f . i) ) implies g in Ker (product f) )

proof

assume A1: g in Ker (product f) ; :: thesis: for i being Element of I holds g in Ker (f . i)
let i be Element of I; :: thesis: g in Ker (f . i)
(product f) . g = 1_ (product F) by A1, GROUP_6:41;
then 1_ (F . i) = ((product f) . g) . i by Th42
.= (f . i) . g by Def14 ;
hence g in Ker (f . i) by GROUP_6:41; :: thesis: verum

end;

thus ( ( for i being Element of I holds g in Ker (f . i) ) implies g in Ker (product f) ) :: thesis: verum

proof

assume A1: for i being Element of I holds g in Ker (f . i) ; :: thesis: g in Ker (product f)
A2: for i being Element of I holds (f . i) . g = 1_ (F . i)

proof

let i be Element of I; :: thesis: (f . i) . g = 1_ (F . i)
g in Ker (f . i) by A1;
hence (f . i) . g = 1_ (F . i) by GROUP_6:41; :: thesis: verum

end;

for i being Element of I holds ((product f) . g) . i = 1_ (F . i)

proof

let i be Element of I; :: thesis: ((product f) . g) . i = 1_ (F . i)
((product f) . g) . i = (f . i) . g by Def14
.= 1_ (F . i) by A2 ;
hence ((product f) . g) . i = 1_ (F . i) ; :: thesis: verum

end;

then (product f) . g = 1_ (product F) by Th42;
hence g in Ker (product f) by GROUP_6:41; :: thesis: verum

end;