let I be non empty set ; :: thesis: for F being Group-Family of I
for i, j being Element of I st i <> j holds
(proj (F,j)) * (1ProdHom (F,i)) = 1: ((F . i),(F . j))
let F be Group-Family of I; :: thesis: for i, j being Element of I st i <> j holds
(proj (F,j)) * (1ProdHom (F,i)) = 1: ((F . i),(F . j))
let i, j be Element of I; :: thesis: ( i <> j implies (proj (F,j)) * (1ProdHom (F,i)) = 1: ((F . i),(F . j)) )
assume A1: i <> j ; :: thesis: (proj (F,j)) * (1ProdHom (F,i)) = 1: ((F . i),(F . j))
set U = the carrier of (F . i);
A2: ( dom (1: ((F . i),(F . j))) = the carrier of (F . i) & dom ((proj (F,j)) * (1ProdHom (F,i))) = the carrier of (F . i) )

proof

thus dom (1: ((F . i),(F . j))) = the carrier of (F . i) ; :: thesis: dom ((proj (F,j)) * (1ProdHom (F,i))) = the carrier of (F . i)
B1: rng (1ProdHom (F,i)) c= the carrier of (ProjGroup (F,i)) by RELAT_1:def 19;
the carrier of (ProjGroup (F,i)) c= the carrier of (product F) by GROUP_2:def 5;
then 1ProdHom (F,i) is the carrier of (product F) -valued by B1, XBOOLE_1:1, RELAT_1:def 19;
then dom ((proj (F,j)) * (1ProdHom (F,i))) = dom (1ProdHom (F,i)) by FUNCT_2:123;
hence dom ((proj (F,j)) * (1ProdHom (F,i))) = the carrier of (F . i) by FUNCT_2:def 1; :: thesis: verum

end;

for x being Element of the carrier of (F . i) holds ((proj (F,j)) * (1ProdHom (F,i))) . x = (1: ((F . i),(F . j))) . x

proof

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

end;

hence (proj (F,j)) * (1ProdHom (F,i)) = 1: ((F . i),(F . j)) by A2; :: thesis: verum