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 H1( 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) = H1(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;