let x, y, z be Element of EnsHomography3 ; :: thesis: (x (*) y) (*) z = x (*) (y (*) z)
x in EnsHomography3 ;
then consider Nx being invertible Matrix of 3,F_Real such that
A2: x = homography Nx ;
y in EnsHomography3 ;
then consider Ny being invertible Matrix of 3,F_Real such that
A3: y = homography Ny ;
z in EnsHomography3 ;
then consider Nz being invertible Matrix of 3,F_Real such that
A4: z = homography Nz ;
A5: ( width Nx = 3 & len Ny = 3 & width Ny = 3 & len Nz = 3 ) by MATRIX_0:24;
y (*) z = homography (Ny * Nz) by A3, A4, Th18;
then A6: x (*) (y (*) z) = homography (Nx * (Ny * Nz)) by A2, Th18
.= homography ((Nx * Ny) * Nz) by A5, MATRIX_3:33 ;
x (*) y = homography (Nx * Ny) by A2, A3, Th18;
hence (x (*) y) (*) z = x (*) (y (*) z) by A6, A4, Th18; :: thesis: verum