set Gi = F . i;

the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;

then A1: dom (1_ (product F)) = I by PARTFUN1:def 2;

A2: dom ((1_ (product F)) +* (i,(1_ (F . i)))) = dom (1_ (product F)) by FUNCT_7:30;

set FG = (1_ (product F)) +* (i,(1_ (F . i)));

reconsider FG = (1_ (product F)) +* (i,(1_ (F . i))) as I -defined Function by A2, A1, RELAT_1:def 18;

the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;

then A1: dom (1_ (product F)) = I by PARTFUN1:def 2;

A2: dom ((1_ (product F)) +* (i,(1_ (F . i)))) = dom (1_ (product F)) by FUNCT_7:30;

set FG = (1_ (product F)) +* (i,(1_ (F . i)));

reconsider FG = (1_ (product F)) +* (i,(1_ (F . i))) as I -defined Function by A2, A1, RELAT_1:def 18;

now :: thesis: for j being Element of I holds FG . j = 1_ (F . j)

hence
not ProjSet (F,i) is empty
by Def1; :: thesis: verumlet j be Element of I; :: thesis: FG . b_{1} = 1_ (F . b_{1})

end;