let N1, N2 be invertible Matrix of 3,F_Real; :: thesis: for h1, h2 being Element of EnsHomography3 st h1 = homography N1 & h2 = homography N2 holds
homography (N1 * N2) = h1 (*) h2
let h1, h2 be Element of EnsHomography3 ; :: thesis: ( h1 = homography N1 & h2 = homography N2 implies homography (N1 * N2) = h1 (*) h2 )
assume that
A1: h1 = homography N1 and
A2: h2 = homography N2 ; :: thesis: homography (N1 * N2) = h1 (*) h2
consider M1, M2 being invertible Matrix of 3,F_Real such that
A3: h1 = homography M1 and
A4: h2 = homography M2 and
A5: h1 (*) h2 = homography (M1 * M2) by Def01;
reconsider h12 = h1 (*) h2 as Function of (ProjectiveSpace (TOP-REAL 3)),(ProjectiveSpace (TOP-REAL 3)) by A5;

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

dom (homography (N1 * N2)) = the carrier of (ProjectiveSpace (TOP-REAL 3)) by FUNCT_2:def 1;
hence dom (homography (N1 * N2)) = dom h12 by FUNCT_2:def 1; :: thesis: for x being object st x in dom (homography (N1 * N2)) holds
(homography (N1 * N2)) . x = h12 . x
thus for x being object st x in dom (homography (N1 * N2)) holds
(homography (N1 * N2)) . x = h12 . x :: thesis: verum

proof

let x be object ; :: thesis: ( x in dom (homography (N1 * N2)) implies (homography (N1 * N2)) . x = h12 . x )
assume x in dom (homography (N1 * N2)) ; :: thesis: (homography (N1 * N2)) . x = h12 . x
then reconsider xf = x as Element of (ProjectiveSpace (TOP-REAL 3)) ;
(homography (N1 * N2)) . xf = (homography N1) . ((homography N2) . xf) by Th14
.= h12 . xf by A3, A4, A5, A1, A2, Th14 ;
hence (homography (N1 * N2)) . x = h12 . x ; :: thesis: verum

end;

end;

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