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;

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 ) )

hence
homography (N1 * N2) = h1 (*) h2
by FUNCT_1:def 11; :: thesis: verum(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

end;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;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