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

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