thus not GroupLineHomography3 is empty ; :: thesis: ( GroupLineHomography3 is associative & GroupLineHomography3 is Group-like )
thus GroupLineHomography3 is associative :: thesis: GroupLineHomography3 is Group-like

proof

let x, y, z be Element of GroupLineHomography3; :: according to GROUP_1:def 3 :: thesis: (x * y) * z = x * (y * z)
reconsider xf = x, yf = y, zf = z as Element of EnsLineHomography3 ;
A7: x * y = xf (*) yf by Def04;
A8: (x * y) * z = (xf (*) yf) (*) zf by Def04, A7;
y * z = yf (*) zf by Def04;
then x * (y * z) = xf (*) (yf (*) zf) by Def04;
hence (x * y) * z = x * (y * z) by A8, Th17; :: thesis: verum

end;

take e ; :: according to GROUP_1:def 2 :: thesis: for b₁ being Element of the carrier of GroupLineHomography3 holds
( b₁ * e = b₁ & e * b₁ = b₁ & ex b₂ being Element of the carrier of GroupLineHomography3 st
( b₁ * b₂ = e & b₂ * b₁ = e ) )
let h be Element of GroupLineHomography3; :: thesis: ( h * e = h & e * h = h & ex b₁ being Element of the carrier of GroupLineHomography3 st
( h * b₁ = e & b₁ * h = e ) )
thus ( h * e = h & e * h = h ) by Lm1; :: thesis: ex b₁ being Element of the carrier of GroupLineHomography3 st
( h * b₁ = e & b₁ * h = e )
h in EnsLineHomography3 ;
then consider N being invertible Matrix of 3,F_Real such that
A9: h = line_homography N ;
reconsider Ng = N ~ as invertible Matrix of 3,F_Real ;
line_homography Ng in EnsLineHomography3 ;
then reconsider g = line_homography Ng as Element of GroupLineHomography3 ;
take g ; :: thesis: ( h * g = e & g * h = e )
thus ( h * g = e & g * h = e ) by A9, Lm2; :: thesis: verum