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