let I be non empty set ; :: thesis: for i being Element of I
for F being Group-Family of I holds proj (F,i) is onto
let i be Element of I; :: thesis: for F being Group-Family of I holds proj (F,i) is onto
let F be Group-Family of I; :: thesis: proj (F,i) is onto
for y being object st y in the carrier of (F . i) holds
ex x being object st
( x in the carrier of (product F) & y = (proj (F,i)) . x )

proof

let y be object ; :: thesis: ( y in the carrier of (F . i) implies ex x being object st
( x in the carrier of (product F) & y = (proj (F,i)) . x ) )
assume y in the carrier of (F . i) ; :: thesis: ex x being object st
( x in the carrier of (product F) & y = (proj (F,i)) . x )
then reconsider yy = y as Element of (F . i) ;
(1ProdHom (F,i)) . yy in ProjGroup (F,i) ;
then (1ProdHom (F,i)) . yy in ProjSet (F,i) by GROUP_12:def 2;
then consider x being Function, g being Element of (F . i) such that
A1: ( x = (1ProdHom (F,i)) . yy & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) by GROUP_12:2;
the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
then dom (1_ (product F)) = I by PARTFUN1:def 2;
then A2: y = ((1_ (product F)) +* (i,y)) . i by FUNCT_7:31
.= g by A1, GROUP_12:def 3 ;
A3: x in product F by A1, GROUP_2:41;
take x ; :: thesis: ( x in the carrier of (product F) & y = (proj (F,i)) . x )
thus x in the carrier of (product F) by A3; :: thesis: y = (proj (F,i)) . x
thus y = (proj (F,i)) . x by Def13, A1, A2, A3; :: thesis: verum

end;

then rng (proj (F,i)) = the carrier of (F . i) by FUNCT_2:10;
hence proj (F,i) is onto by FUNCT_2:def 3; :: thesis: verum