let K be Field; :: thesis: for n being Nat

for M1, M2, M3, M4 being Matrix of n,K st M3 is_reverse_of M1 & M4 is_reverse_of M2 holds

M3 * M4 is_reverse_of M2 * M1

let n be Nat; :: thesis: for M1, M2, M3, M4 being Matrix of n,K st M3 is_reverse_of M1 & M4 is_reverse_of M2 holds

M3 * M4 is_reverse_of M2 * M1

let M1, M2, M3, M4 be Matrix of n,K; :: thesis: ( M3 is_reverse_of M1 & M4 is_reverse_of M2 implies M3 * M4 is_reverse_of M2 * M1 )

A1: width M1 = n by MATRIX_0:24;

A2: ( width M2 = n & len M1 = n ) by MATRIX_0:24;

A3: len M3 = n by MATRIX_0:24;

A4: ( width M3 = n & len M4 = n ) by MATRIX_0:24;

assume that

A5: M3 is_reverse_of M1 and

A6: M4 is_reverse_of M2 ; :: thesis: M3 * M4 is_reverse_of M2 * M1

width (M2 * M1) = n by MATRIX_0:24;

then A7: (M2 * M1) * (M3 * M4) = ((M2 * M1) * M3) * M4 by A3, A4, MATRIX_3:33

.= (M2 * (M1 * M3)) * M4 by A1, A2, A3, MATRIX_3:33

.= (M2 * (1. (K,n))) * M4 by A5

.= M2 * M4 by MATRIX_3:19

.= 1. (K,n) by A6 ;

A8: width M4 = n by MATRIX_0:24;

A9: len M2 = n by MATRIX_0:24;

width (M3 * M4) = n by MATRIX_0:24;

then (M3 * M4) * (M2 * M1) = ((M3 * M4) * M2) * M1 by A2, A9, MATRIX_3:33

.= (M3 * (M4 * M2)) * M1 by A9, A8, A4, MATRIX_3:33

.= (M3 * (1. (K,n))) * M1 by A6

.= M3 * M1 by MATRIX_3:19

.= 1. (K,n) by A5 ;

hence M3 * M4 is_reverse_of M2 * M1 by A7; :: thesis: verum

for M1, M2, M3, M4 being Matrix of n,K st M3 is_reverse_of M1 & M4 is_reverse_of M2 holds

M3 * M4 is_reverse_of M2 * M1

let n be Nat; :: thesis: for M1, M2, M3, M4 being Matrix of n,K st M3 is_reverse_of M1 & M4 is_reverse_of M2 holds

M3 * M4 is_reverse_of M2 * M1

let M1, M2, M3, M4 be Matrix of n,K; :: thesis: ( M3 is_reverse_of M1 & M4 is_reverse_of M2 implies M3 * M4 is_reverse_of M2 * M1 )

A1: width M1 = n by MATRIX_0:24;

A2: ( width M2 = n & len M1 = n ) by MATRIX_0:24;

A3: len M3 = n by MATRIX_0:24;

A4: ( width M3 = n & len M4 = n ) by MATRIX_0:24;

assume that

A5: M3 is_reverse_of M1 and

A6: M4 is_reverse_of M2 ; :: thesis: M3 * M4 is_reverse_of M2 * M1

width (M2 * M1) = n by MATRIX_0:24;

then A7: (M2 * M1) * (M3 * M4) = ((M2 * M1) * M3) * M4 by A3, A4, MATRIX_3:33

.= (M2 * (M1 * M3)) * M4 by A1, A2, A3, MATRIX_3:33

.= (M2 * (1. (K,n))) * M4 by A5

.= M2 * M4 by MATRIX_3:19

.= 1. (K,n) by A6 ;

A8: width M4 = n by MATRIX_0:24;

A9: len M2 = n by MATRIX_0:24;

width (M3 * M4) = n by MATRIX_0:24;

then (M3 * M4) * (M2 * M1) = ((M3 * M4) * M2) * M1 by A2, A9, MATRIX_3:33

.= (M3 * (M4 * M2)) * M1 by A9, A8, A4, MATRIX_3:33

.= (M3 * (1. (K,n))) * M1 by A6

.= M3 * M1 by MATRIX_3:19

.= 1. (K,n) by A5 ;

hence M3 * M4 is_reverse_of M2 * M1 by A7; :: thesis: verum