let x, y, z be Element of EnsLineHomography3 ; (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; verum