let I be non empty set ; :: thesis: for i being Element of I
for F being Group-Family of I holds (proj (F,i)) * (1ProdHom (F,i)) = id the carrier of (F . i)
let i be Element of I; :: thesis: for F being Group-Family of I holds (proj (F,i)) * (1ProdHom (F,i)) = id the carrier of (F . i)
let F be Group-Family of I; :: thesis: (proj (F,i)) * (1ProdHom (F,i)) = id the carrier of (F . i)
set U = the carrier of (F . i);
A1: 1ProdHom (F,i) is Homomorphism of (F . i),(product F) by GROUP_19:6;
for x being Element of the carrier of (F . i) holds ((proj (F,i)) * (1ProdHom (F,i))) . x = x

proof

let x be Element of the carrier of (F . i); :: thesis: ((proj (F,i)) * (1ProdHom (F,i))) . x = x
B1: dom (1_ (product F)) = I by GROUP_19:3;
B2: (1ProdHom (F,i)) . x = (1_ (product F)) +* (i,x) by GROUP_12:def 3;
(1ProdHom (F,i)) . x in ProjGroup (F,i) ;
then (1ProdHom (F,i)) . x in product F by GROUP_2:40;
then B3: (proj (F,i)) . ((1_ (product F)) +* (i,x)) = ((1_ (product F)) +* (i,x)) . i by B2, Def13;
dom (1ProdHom (F,i)) = the carrier of (F . i) by FUNCT_2:def 1;
then ((proj (F,i)) * (1ProdHom (F,i))) . x = (proj (F,i)) . ((1ProdHom (F,i)) . x) by FUNCT_1:13
.= (proj (F,i)) . ((1_ (product F)) +* (i,x)) by GROUP_12:def 3
.= x by B1, B3, FUNCT_7:31 ;
hence ((proj (F,i)) * (1ProdHom (F,i))) . x = x ; :: thesis: verum

end;

hence (proj (F,i)) * (1ProdHom (F,i)) = id the carrier of (F . i) by A1, FUNCT_2:124; :: thesis: verum