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_{1}( 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_{1}(i,j)
from MATRIX_0:sch 1();

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

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

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

end;

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)) ) )

( 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;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

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)) ) )

( 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;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