for h being Element of GroupLineHomography3 holds
( h * e = h & e * h = h ) by Lm1;
hence 1_ GroupLineHomography3 = line_homography (1. (F_Real,3)) by GROUP_1:4; :: thesis: verum