let p be FinSequence of REAL ; :: thesis: for N, M being Matrix of 3,REAL st len p = 3 holds
|((N * p),(M * (N * p)))| = |(p,((((N @) * M) * N) * p))|
let N, M be Matrix of 3,REAL; :: thesis: ( len p = 3 implies |((N * p),(M * (N * p)))| = |(p,((((N @) * M) * N) * p))| )
assume A1: len p = 3 ; :: thesis: |((N * p),(M * (N * p)))| = |(p,((((N @) * M) * N) * p))|
A2: len N = 3 by MATRIX_0:24;
A3: len M = 3 by MATRIX_0:24;
A4: width N = 3 by MATRIX_0:24;
A5: width M = 3 by MATRIX_0:24;
( width N = len p & len p > 0 ) by A1, MATRIX_0:24;
then ( width M = len (N * p) & len (N * p) > 0 ) by A2, A4, A5, MATRIXR1:61;
then len (M * (N * p)) = len N by A2, A3, MATRIXR1:61;
then |((N * p),(M * (N * p)))| = |(p,((N @) * (M * (N * p))))| by A2, A4, A1, MATRPROB:48
.= |(p,((((N @) * M) * N) * p))| by A1, Lm01 ;
hence |((N * p),(M * (N * p)))| = |(p,((((N @) * M) * N) * p))| ; :: thesis: verum