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

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