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_0: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_0:23;
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_0:25;
len B = 0 by A1, A3, MATRIX_0:def 3;
then width B = 0 by MATRIX_0:def 3;
then width M = width B by A4, MATRIX_0:def 3;
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;