set Gi = F . i;
the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
then A3: dom (1_ (product F)) = I by PARTFUN1:def 4;
A2: dom ((1_ (product F)) +* (i,(1_ (F . i)))) = dom (1_ (product F)) by FUNCT_7:32;
set FG = (1_ (product F)) +* (i,(1_ (F . i)));
reconsider FG = (1_ (product F)) +* (i,(1_ (F . i))) as I -defined Function by A2, A3, RELAT_1:def 18;

now

let j be Element of I; :: thesis: FG . b₁ = 1_ (F . b₁)

per cases ( j <> i or j = i ) ;

suppose C1: j <> i ; :: thesis: FG . b₁ = 1_ (F . b₁)

thus FG . j = (1_ (product F)) . j by FUNCT_7:34, C1
.= 1_ (F . j) by GROUP_7:9 ; :: thesis: verum

end;

suppose j = i ; :: thesis: FG . b₁ = 1_ (F . b₁)

hence FG . j = 1_ (F . j) by FUNCT_7:33, A3; :: thesis: verum

end;

end;

end;

hence not ProjSet (F,i) is empty by defPrj; :: thesis: verum