let n, m be Nat; :: thesis: for x being FinSequence of REAL st len x = m & n > 0 & m > 0 holds
(0_Rmatrix (n,m)) * x = 0* n
let x be FinSequence of REAL ; :: thesis: ( len x = m & n > 0 & m > 0 implies (0_Rmatrix (n,m)) * x = 0* n )
assume that
A1: len x = m and
A2: n > 0 and
A3: m > 0 ; :: thesis: (0_Rmatrix (n,m)) * x = 0* n
A4: width (0_Rmatrix (n,m)) = m by A2, MATRIX_0:23;
then A5: len ((0_Rmatrix (n,m)) * x) = len (0_Rmatrix (n,m)) by A1, A3, Th61;
A6: len (0_Rmatrix (n,m)) = n by A2, MATRIX_0:23;
then (0_Rmatrix (n,m)) * x = ((0_Rmatrix (n,m)) + (0_Rmatrix (n,m))) * x by A2, A4, Th36
.= ((0_Rmatrix (n,m)) * x) + ((0_Rmatrix (n,m)) * x) by A1, A3, A6, A4, Th63 ;
then 0* n = (((0_Rmatrix (n,m)) * x) + ((0_Rmatrix (n,m)) * x)) - ((0_Rmatrix (n,m)) * x) by A6, A5, Th3;
hence (0_Rmatrix (n,m)) * x = 0* n by A5, Th14; :: thesis: verum