thus not GroupHomography3 is empty ; :: thesis:
thus GroupHomography3 is associative :: thesis:
proof
let x, y, z be Element of GroupHomography3; :: according to GROUP_1:def 3 :: thesis: (x * y) * z = x * (y * z)
reconsider xf = x, yf = y, zf = z as Element of EnsHomography3 ;
A7: x * y = xf (*) yf by Def02;
A8: (x * y) * z = (xf (*) yf) (*) zf by ;
y * z = yf (*) zf by Def02;
then x * (y * z) = xf (*) (yf (*) zf) by Def02;
hence (x * y) * z = x * (y * z) by ; :: thesis: verum
end;
take e ; :: according to GROUP_1:def 2 :: thesis: for b1 being Element of the carrier of GroupHomography3 holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of GroupHomography3 st
( b1 * b2 = e & b2 * b1 = e ) )

let h be Element of GroupHomography3; :: thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of GroupHomography3 st
( h * b1 = e & b1 * h = e ) )

thus ( h * e = h & e * h = h ) by Lm1; :: thesis: ex b1 being Element of the carrier of GroupHomography3 st
( h * b1 = e & b1 * h = e )

h in EnsHomography3 ;
then consider N being invertible Matrix of 3,F_Real such that
A9: h = homography N ;
reconsider Ng = N ~ as invertible Matrix of 3,F_Real ;
homography Ng in EnsHomography3 ;
then reconsider g = homography Ng as Element of GroupHomography3 ;
take g ; :: thesis: ( h * g = e & g * h = e )
thus ( h * g = e & g * h = e ) by ; :: thesis: verum