set G = GroupHomography3 ;
homography (1. (F_Real,3)) in GroupHomography3 by ANPROJ_9:def 1, ANPROJ_9:def 4;
then reconsider e = homography (1. (F_Real,3)) as Element of GroupHomography3 ;

now :: thesis: for h being Element of GroupHomography3 holds
( h * e = h & e * h = h )

let h be Element of GroupHomography3; :: thesis: ( h * e = h & e * h = h )
h in EnsHomography3 by ANPROJ_9:def 4;
then consider N being invertible Matrix of 3,F_Real such that
A1: h = homography N by ANPROJ_9:def 1;
( h in EnsHomography3 & e in EnsHomography3 ) by A1, ANPROJ_9:def 1;
then reconsider h1 = h, h2 = e as Element of EnsHomography3 ;
thus h * e = h1 (*) h2 by ANPROJ_9:def 3, ANPROJ_9:def 4
.= homography (N * (1. (F_Real,3))) by A1, ANPROJ_9:18
.= h by A1, MATRIX_3:19 ; :: thesis: e * h = h
thus e * h = h2 (*) h1 by ANPROJ_9:def 3, ANPROJ_9:def 4
.= homography ((1. (F_Real,3)) * N) by A1, ANPROJ_9:18
.= h by A1, MATRIX_3:18 ; :: thesis: verum

end;

hence homography (1. (F_Real,3)) = 1_ GroupHomography3 by GROUP_1:4; :: thesis: homography (1. (F_Real,3)) = 1_ SubGroupK-isometry
hence homography (1. (F_Real,3)) = 1_ SubGroupK-isometry by GROUP_2:44; :: thesis: verum