let K be Field; :: thesis: for A, B being Matrix of K st width A = len B holds
ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * i,j = (Line A,i) "*" (Col B,j) ) )
let A, B be Matrix of K; :: thesis: ( width A = len B implies ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * i,j = (Line A,i) "*" (Col B,j) ) ) )
assume A1: width A = len B ; :: thesis: ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * i,j = (Line A,i) "*" (Col B,j) ) )
deffunc H₁( Nat, Nat) -> Element of the carrier of K = (Line A,$1) "*" (Col B,$2);
consider M being Matrix of len A, width B,the carrier of K such that
A2: for i, j being Nat st [i,j] in Indices M holds
M * i,j = H₁(i,j) from MATRIX_1:sch 1();

per cases ( len A > 0 or len A = 0 ) ;

suppose len A > 0 ; :: thesis: ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * i,j = (Line A,i) "*" (Col B,j) ) )

then ( len M = len A & width M = width B ) by MATRIX_1:24;
hence ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * i,j = (Line A,i) "*" (Col B,j) ) ) by A2; :: thesis: verum

end;

suppose A3: len A = 0 ; :: thesis: ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * i,j = (Line A,i) "*" (Col B,j) ) )

then A4: len M = 0 by MATRIX_1:26;
len B = 0 by A1, A3, MATRIX_1:def 4;
then width B = 0 by MATRIX_1:def 4;
then width M = width B by A4, MATRIX_1:def 4;
hence ex C being Matrix of K st
( len C = len A & width C = width B & ( for i, j being Nat st [i,j] in Indices C holds
C * i,j = (Line A,i) "*" (Col B,j) ) ) by A2, A3, A4; :: thesis: verum

end;

end;