let I be non empty set ; :: thesis: for F1, F2 being Group-Family of I
for f being Homomorphism-Family of F1,F2 holds Ker (product f) = product (Ker f)
let F1, F2 be Group-Family of I; :: thesis: for f being Homomorphism-Family of F1,F2 holds Ker (product f) = product (Ker f)
let f be Homomorphism-Family of F1,F2; :: thesis: Ker (product f) = product (Ker f)
for g being Element of (product F1) holds
( g in Ker (product f) iff g in product (Ker f) )

proof

let g be Element of (product F1); :: thesis: ( g in Ker (product f) iff g in product (Ker f) )

hereby :: thesis: ( g in product (Ker f) implies g in Ker (product f) )

assume A1: g in Ker (product f) ; :: thesis: g in product (Ker f)
A2: dom g = I by GROUP_19:3;
for i being Element of I holds g . i in (Ker f) . i

proof

let i be Element of I; :: thesis: g . i in (Ker f) . i
B1: ( dom (product f) = the carrier of (product F1) & dom (proj (F1,i)) = the carrier of (product F1) ) by FUNCT_2:def 1;
B2: ((proj (F2,i)) * (product f)) . g = ((f . i) * (proj (F1,i))) . g by Def15
.= (f . i) . ((proj (F1,i)) . g) by B1, FUNCT_1:13
.= (f . i) . (g . i) by Def13 ;
((proj (F2,i)) * (product f)) . g = (proj (F2,i)) . ((product f) . g) by B1, FUNCT_1:13
.= (proj (F2,i)) . (1_ (product F2)) by A1, GROUP_6:41
.= (1_ (product F2)) . i by Def13
.= 1_ (F2 . i) by GROUP_7:6 ;
then g /. i in Ker (f . i) by B2, GROUP_6:41;
hence g . i in (Ker f) . i by Def16; :: thesis: verum

end;

hence g in product (Ker f) by A2, Th47; :: thesis: verum

end;

assume A1: g in product (Ker f) ; :: thesis: g in Ker (product f)
A2: ( dom (1_ (product F2)) = I & dom ((product f) . g) = I & dom g = I ) by GROUP_19:3;
for i being Element of I holds ((product f) . g) . i = (1_ (product F2)) . i

proof

let i be Element of I; :: thesis: ((product f) . g) . i = (1_ (product F2)) . i
B1: ( dom (proj (F1,i)) = the carrier of (product F1) & dom (product f) = the carrier of (product F1) ) by FUNCT_2:def 1;
g . i in (Ker f) . i by A1, GROUP_19:5;
then B2: g . i in Ker (f . i) by Def16;
B3: ((proj (F2,i)) * (product f)) . g = ((f . i) * (proj (F1,i))) . g by Def15
.= (f . i) . ((proj (F1,i)) . g) by B1, FUNCT_1:13
.= (f . i) . (g . i) by Def13 ;
((proj (F2,i)) * (product f)) . g = (proj (F2,i)) . ((product f) . g) by B1, FUNCT_1:13
.= ((product f) . g) . i by Def13 ;
then ((product f) . g) . i = (f . i) . (g /. i) by B3
.= 1_ (F2 . i) by B2, GROUP_6:41 ;
hence ((product f) . g) . i = (1_ (product F2)) . i by GROUP_7:6; :: thesis: verum

end;

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

end;

hence Ker (product f) = product (Ker f) by GROUP_2:def 6; :: thesis: verum