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_{1} being Homomorphism of (F . i),(ProjGroup (F,i)) st

for x being Element of (F . i) holds b_{1} . x = (1_ (product F)) +* (i,x)
; :: thesis: verum

( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) ) by Lm1;

hence ex b

for x being Element of (F . i) holds b