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