let n, m be 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_0:23;
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_0:23;
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, 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