ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st
( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) ) by Lm1;
hence ex b₁ being Homomorphism of (F . i),(ProjGroup (F,i)) st
for x being Element of (F . i) holds b₁ . x = (1_ (product F)) +* (i,x) ; :: thesis: verum