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 holds the carrier of (Ker (product f)) = meet { the carrier of (Ker (f . i)) where i is Element of I : verum }
let F be Group-Family of I; :: thesis: for G being Group
for f being Homomorphism-Family of G,F holds the carrier of (Ker (product f)) = meet { the carrier of (Ker (f . i)) where i is Element of I : verum }
let G be Group; :: thesis: for f being Homomorphism-Family of G,F holds the carrier of (Ker (product f)) = meet { the carrier of (Ker (f . i)) where i is Element of I : verum }
let f be Homomorphism-Family of G,F; :: thesis: the carrier of (Ker (product f)) = meet { the carrier of (Ker (f . i)) where i is Element of I : verum }
set Fam = { the carrier of (Ker (f . i)) where i is Element of I : verum } ;
A1: { the carrier of (Ker (f . i)) where i is Element of I : verum } <> {}

proof

set i = the Element of I;
the carrier of (Ker (f . the Element of I)) in { the carrier of (Ker (f . i)) where i is Element of I : verum } ;
hence { the carrier of (Ker (f . i)) where i is Element of I : verum } <> {} ; :: thesis: verum

end;

A3: for g being object holds
( g in Ker (product f) iff for A being set st A in { the carrier of (Ker (f . i)) where i is Element of I : verum } holds
g in A )

proof

let g be object ; :: thesis: ( g in Ker (product f) iff for A being set st A in { the carrier of (Ker (f . i)) where i is Element of I : verum } holds
g in A )

hereby :: thesis: ( ( for A being set st A in { the carrier of (Ker (f . i)) where i is Element of I : verum } holds
g in A ) implies g in Ker (product f) )

assume B1: g in Ker (product f) ; :: thesis: for A being set st A in { the carrier of (Ker (f . i)) where i is Element of I : verum } holds
g in A
let A be set ; :: thesis: ( A in { the carrier of (Ker (f . i)) where i is Element of I : verum } implies g in A )
assume A in { the carrier of (Ker (f . i)) where i is Element of I : verum } ; :: thesis: g in A
then consider i1 being Element of I such that
B2: A = the carrier of (Ker (f . i1)) ;
( g in G & g in Ker (product f) ) by B1, GROUP_2:40;
then g in Ker (f . i1) by Th43;
hence g in A by B2; :: thesis: verum

end;

assume B1: for A being set st A in { the carrier of (Ker (f . i)) where i is Element of I : verum } holds
g in A ; :: thesis: g in Ker (product f)
( g in G & ( for i being Element of I holds g in Ker (f . i) ) )

proof

ex x being object st x in { the carrier of (Ker (f . i)) where i is Element of I : verum } by A1, XBOOLE_0:def 1;
then consider A0 being set such that
B2: A0 in { the carrier of (Ker (f . i)) where i is Element of I : verum } ;
consider i0 being Element of I such that
B3: A0 = the carrier of (Ker (f . i0)) by B2;
g in Ker (f . i0) by B1, B2, B3;
hence g in G by GROUP_2:40; :: 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)
the carrier of (Ker (f . i)) in { the carrier of (Ker (f . i)) where i is Element of I : verum } ;
hence g in Ker (f . i) by B1; :: thesis: verum

end;

hence g in Ker (product f) by Th43; :: thesis: verum

end;

A4: for g being object holds
( g in Ker (product f) iff g in meet { the carrier of (Ker (f . i)) where i is Element of I : verum } )

proof

let g be object ; :: thesis: ( g in Ker (product f) iff g in meet { the carrier of (Ker (f . i)) where i is Element of I : verum } )
( g in Ker (product f) iff for A being set st A in { the carrier of (Ker (f . i)) where i is Element of I : verum } holds
g in A ) by A3;
hence ( g in Ker (product f) iff g in meet { the carrier of (Ker (f . i)) where i is Element of I : verum } ) by A1, SETFAM_1:def 1; :: thesis: verum

end;

for g being object holds
( g in the carrier of (Ker (product f)) iff g in meet { the carrier of (Ker (f . i)) where i is Element of I : verum } )

proof

let g be object ; :: thesis: ( g in the carrier of (Ker (product f)) iff g in meet { the carrier of (Ker (f . i)) where i is Element of I : verum } )
( g in the carrier of (Ker (product f)) iff g in Ker (product f) ) ;
hence ( g in the carrier of (Ker (product f)) iff g in meet { the carrier of (Ker (f . i)) where i is Element of I : verum } ) by A4; :: thesis: verum

end;

hence the carrier of (Ker (product f)) = meet { the carrier of (Ker (f . i)) where i is Element of I : verum } by TARSKI:2; :: thesis: verum