let n, m be Element of NAT ; :: thesis: for x being FinSequence of REAL st len x = n & n > 0 holds
x * (0_Rmatrix n,m) = 0* m
let x be FinSequence of REAL ; :: thesis: ( len x = n & n > 0 implies x * (0_Rmatrix n,m) = 0* m )
assume that
A1: len x = n and
A2: n > 0 ; :: thesis: x * (0_Rmatrix n,m) = 0* m
A3: len (0_Rmatrix n,m) = n by A2, MATRIX_1:24;
then A4: len (x * (0_Rmatrix n,m)) = width (0_Rmatrix n,m) by A1, Th62;
A5: width (0_Rmatrix n,m) = m by A2, MATRIX_1:24;
then x * (0_Rmatrix n,m) = x * ((0_Rmatrix n,m) + (0_Rmatrix n,m)) by A2, A3, Th36
.= (x * (0_Rmatrix n,m)) + (x * (0_Rmatrix n,m)) by A1, A2, A5, A3, Th64 ;
then 0* m = ((x * (0_Rmatrix n,m)) + (x * (0_Rmatrix n,m))) - (x * (0_Rmatrix n,m)) by A5, A4, Th3;
hence x * (0_Rmatrix n,m) = 0* m by A4, Th14; :: thesis: verum