let N1, N2 be invertible Matrix of 3,F_Real; :: thesis: for h1, h2 being Element of EnsLineHomography3 st h1 = line_homography N1 & h2 = line_homography N2 holds
line_homography (N1 * N2) = h1 (*) h2
let h1, h2 be Element of EnsLineHomography3 ; :: thesis: ( h1 = line_homography N1 & h2 = line_homography N2 implies line_homography (N1 * N2) = h1 (*) h2 )
assume that
A1: h1 = line_homography N1 and
A2: h2 = line_homography N2 ; :: thesis: line_homography (N1 * N2) = h1 (*) h2
consider M1, M2 being invertible Matrix of 3,F_Real such that
A3: h1 = line_homography M1 and
A4: h2 = line_homography M2 and
A5: h1 (*) h2 = line_homography (M1 * M2) by Def03;
reconsider h12 = h1 (*) h2 as Function of the Lines of (IncProjSp_of real_projective_plane), the Lines of (IncProjSp_of real_projective_plane) by A5;

now :: thesis: ( dom (line_homography (N1 * N2)) = dom h12 & ( for x being object st x in dom (line_homography (N1 * N2)) holds
(line_homography (N1 * N2)) . x = h12 . x ) )

dom (line_homography (N1 * N2)) = the Lines of (IncProjSp_of real_projective_plane) by FUNCT_2:def 1;
hence dom (line_homography (N1 * N2)) = dom h12 by FUNCT_2:def 1; :: thesis: for x being object st x in dom (line_homography (N1 * N2)) holds
(line_homography (N1 * N2)) . x = h12 . x
thus for x being object st x in dom (line_homography (N1 * N2)) holds
(line_homography (N1 * N2)) . x = h12 . x :: thesis: verum

proof

let x be object ; :: thesis: ( x in dom (line_homography (N1 * N2)) implies (line_homography (N1 * N2)) . x = h12 . x )
assume x in dom (line_homography (N1 * N2)) ; :: thesis: (line_homography (N1 * N2)) . x = h12 . x
then reconsider xf = x as Element of the Lines of (IncProjSp_of real_projective_plane) ;
(line_homography (N1 * N2)) . xf = (line_homography N1) . ((line_homography N2) . xf) by Th13
.= h12 . xf by A3, A4, A5, A1, A2, Th13 ;
hence (line_homography (N1 * N2)) . x = h12 . x ; :: thesis: verum

end;

end;

hence line_homography (N1 * N2) = h1 (*) h2 by FUNCT_1:def 11; :: thesis: verum