consider f being Homomorphism of (F . i),(ProjGroup (F,i)) such that
A1: ( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) ) by Lm1;
set F2 = 1ProdHom (F,i);
for x being Element of (F . i) holds f . x = (1ProdHom (F,i)) . x by Def3, A1;
hence 1ProdHom (F,i) is bijective by A1, FUNCT_2:63; :: thesis: verum