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

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