let K be Field; for A being Matrix of K holds (0. (K,(len A),(len A))) * A = 0. (K,(len A),(width A))
let A be Matrix of K; (0. (K,(len A),(len A))) * A = 0. (K,(len A),(width A))
per cases
( len A > 0 or len A = 0 )
by NAT_1:3;
suppose A1:
len A > 0
;
(0. (K,(len A),(len A))) * A = 0. (K,(len A),(width A))set B =
(0. (K,(len A),(len A))) * A;
A2:
width (- ((0. (K,(len A),(len A))) * A)) = width ((0. (K,(len A),(len A))) * A)
by MATRIX_3:def 2;
A3:
len (0. (K,(len A),(len A))) = len A
by MATRIX_0:def 2;
then A4:
width (0. (K,(len A),(len A))) = len A
by A1, MATRIX_0:20;
then A5:
len ((0. (K,(len A),(len A))) * A) = len A
by A3, MATRIX_3:def 4;
A6:
width ((0. (K,(len A),(len A))) * A) = width A
by A4, MATRIX_3:def 4;
(0. (K,(len A),(len A))) * A =
((0. (K,(len A),(len A))) + (0. (K,(len A),(len A)))) * A
by MATRIX_3:4
.=
((0. (K,(len A),(len A))) * A) + ((0. (K,(len A),(len A))) * A)
by A1, A3, A4, MATRIX_4:63
;
then
(
len (- ((0. (K,(len A),(len A))) * A)) = len ((0. (K,(len A),(len A))) * A) &
0. (
K,
(len A),
(width A))
= (((0. (K,(len A),(len A))) * A) + ((0. (K,(len A),(len A))) * A)) + (- ((0. (K,(len A),(len A))) * A)) )
by A5, A6, MATRIX_3:def 2, MATRIX_4:2;
then 0. (
K,
(len A),
(width A)) =
((0. (K,(len A),(len A))) * A) + (((0. (K,(len A),(len A))) * A) - ((0. (K,(len A),(len A))) * A))
by A2, MATRIX_3:3
.=
(0. (K,(len A),(len A))) * A
by A5, A2, MATRIX_4:20
;
hence
(0. (K,(len A),(len A))) * A = 0. (
K,
(len A),
(width A))
;
verum end; suppose A7:
len A = 0
;
(0. (K,(len A),(len A))) * A = 0. (K,(len A),(width A))then
len (0. (K,(len A),(len A))) = 0
by MATRIX_0:def 2;
then
width (0. (K,(len A),(len A))) = len A
by A7, MATRIX_0:def 3;
then A8:
len ((0. (K,(len A),(len A))) * A) = len (0. (K,(len A),(len A)))
by MATRIX_3:def 4;
(
len (0. (K,(len A),(len A))) = len A &
len (0. (K,(len A),(width A))) = len A )
by MATRIX_0:def 2;
hence
(0. (K,(len A),(len A))) * A = 0. (
K,
(len A),
(width A))
by A7, A8, CARD_2:64;
verum end;