let K be Field; :: thesis:
let A, B be Matrix of K; :: thesis:
assume that
A1: width A = len B and
A2: len B > 0 ; :: thesis:
set aa = the addF of K;
set mm = the multF of K;
set a = addFinS K;
set KK = the carrier of K;
reconsider m = len B, w = width B as Nat ;
let i be Nat; :: thesis:
assume A3: i in Seg (len A) ; :: thesis:
deffunc H₁( Nat) -> Element of (width B) -tuples_on the carrier of K = (A * i,$1) * (Line B,$1);
consider P being FinSequence such that
A4: len P = len B and
A5: for k being Nat st k in dom P holds
P . k = H₁(k) from FINSEQ_1:sch 2();
A6: dom P = dom B by A4, FINSEQ_3:31
.= Seg (len B) by FINSEQ_1:def 3 ;
rng P c= the carrier of K *

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng P ; :: thesis:
then consider x being set such that
A7: x in dom P and
A8: y = P . x by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A7;
P . x = (A * i,x) * (Line B,x) by A5, A7;
hence y in the carrier of K * by A8, FINSEQ_1:def 11; :: thesis:

end;

then reconsider P = P as FinSequence of the carrier of K * by FINSEQ_1:def 4;
A9: m >= 1 by A2, NAT_1:14;
then consider F being Function of NAT ,(the carrier of K * ) such that
A10: F . 1 = P . 1 and
A11: for n being Element of NAT st 0 <> n & n < len P holds
F . (n + 1) = (addFinS K) . (F . n),(P . (n + 1)) and
A12: (addFinS K) "**" P = F . (len P) by A4, FINSOP_1:def 1;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= m implies for F1 being FinSequence of the carrier of K st F . $1 = F1 holds
( len F1 = w & ( for j being Element of NAT st j in Seg w holds
ex LC being FinSequence of the carrier of K st
( LC = (mlt (Line A,i),(Col B,j)) | (Seg $1) & the addF of K "**" LC = F1 . j ) ) ) );
A13: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A14: S₁[k] ; :: thesis:
set k1 = k + 1;
assume that
A15: 1 <= k + 1 and
A16: k + 1 <= m ; :: thesis:
A17: k + 1 in Seg m by A15, A16;
let Fk1 be FinSequence of the carrier of K; :: thesis:
assume A18: F . (k + 1) = Fk1 ; :: thesis:

per cases ;

suppose A19: k = 0 ; :: thesis:

then A20: P . 1 = (A * i,1) * (Line B,1) by A5, A6, A17;
A21: len (Line B,1) = w by MATRIX_1:def 8;
hence len Fk1 = w by A10, A18, A19, A20, Lm5; :: thesis:
let j be Element of NAT ; :: thesis:
assume A22: j in Seg w ; :: thesis:
len Fk1 = w by A10, A18, A19, A20, A21, Lm5;
then A23: j in dom Fk1 by A22, FINSEQ_1:def 3;
(Line B,1) . j = B * 1,j by A22, MATRIX_1:def 8;
then A24: Fk1 . j = (A * i,1) * (B * 1,j) by A10, A18, A19, A20, A23, FVSUM_1:62;
set C = Col B,j;
set L = Line A,i;
reconsider LC1 = (mlt (Line A,i),(Col B,j)) | (Seg (k + 1)), mLC = mlt (Line A,i),(Col B,j) as FinSequence of the carrier of K by FINSEQ_1:23;
A25: the multF of K .: (Line A,i),(Col B,j) is Element of m -tuples_on the carrier of K by A1, FINSEQ_2:140;
then len mLC = m by FINSEQ_1:def 18;
then A26: dom mLC = Seg m by FINSEQ_1:def 3;
Seg 1 = (Seg m) /\ (Seg 1) by A2, FINSEQ_1:9, NAT_1:14;
then A27: dom LC1 = Seg 1 by A19, A26, RELAT_1:90;
then A28: len LC1 = 1 by FINSEQ_1:def 3;
1 in Seg 1 ;
then LC1 . 1 = mLC . 1 by A27, FUNCT_1:70;
then A29: LC1 = <*(mLC . 1)*> by A28, FINSEQ_1:57;
take LC1 ; :: thesis:
A30: 1 in Seg m by A9;
len mLC = m by A25, FINSEQ_1:def 18;
then A31: 1 in dom mLC by A30, FINSEQ_1:def 3;
Seg m = dom B by FINSEQ_1:def 3;
then A32: (Col B,j) . 1 = B * 1,j by A30, MATRIX_1:def 9;
(Line A,i) . 1 = A * i,1 by A1, A30, MATRIX_1:def 8;
then mLC . 1 = (A * i,1) * (B * 1,j) by A32, A31, FVSUM_1:73;
hence ( LC1 = (mlt (Line A,i),(Col B,j)) | (Seg (k + 1)) & the addF of K "**" LC1 = Fk1 . j ) by A24, A29, FINSOP_1:12; :: thesis:

end;

suppose A33: k > 0 ; :: thesis:

dom P = Seg m by A4, FINSEQ_1:def 3;
then A34: P . (k + 1) in rng P by A17, FUNCT_1:def 5;
rng P c= the carrier of K * by FINSEQ_1:def 4;
then reconsider Pk1 = P . (k + 1), Fk = F . k as FinSequence of the carrier of K by A34, FINSEQ_1:def 11;
A35: Pk1 is Element of the carrier of K * by FINSEQ_1:def 11;
then A36: (addFinS K) . Fk,Pk1 = Fk + Pk1 by Def5;
A37: k + 0 < k + 1 by XREAL_1:10;
then k < m by A16, XXREAL_0:2;
then A38: Fk1 = Fk + Pk1 by A4, A11, A18, A33, A36;
A39: len (Line B,(k + 1)) = w by MATRIX_1:def 8;
Pk1 = H₁(k + 1) by A5, A6, A17;
then len Pk1 = w by A39, Lm5;
then A40: dom Pk1 = Seg w by FINSEQ_1:def 3;
A41: len Fk = w by A14, A16, A33, A37, NAT_1:14, XXREAL_0:2;
then dom Fk = Seg w by FINSEQ_1:def 3;
then A42: dom (Fk + Pk1) = (Seg w) /\ (Seg w) by A40, A35, Lm9;
hence len Fk1 = w by A38, FINSEQ_1:def 3; :: thesis:
A43: rng Fk c= the carrier of K by FINSEQ_1:def 4;
set L = Line A,i;
A44: Pk1 = H₁(k + 1) by A5, A6, A17;
let j be Element of NAT ; :: thesis:
assume A45: j in Seg w ; :: thesis:
A46: (Line B,(k + 1)) . j = B * (k + 1),j by A45, MATRIX_1:def 8;
then Pk1 . j = (A * i,(k + 1)) * (B * (k + 1),j) by A40, A45, A44, FVSUM_1:62;
then reconsider Pk1j = Pk1 . j as Element of the carrier of K ;
set C = Col B,j;
consider LC being FinSequence of the carrier of K such that
A47: LC = (mlt (Line A,i),(Col B,j)) | (Seg k) and
A48: the addF of K "**" LC = Fk . j by A14, A16, A33, A37, A45, NAT_1:14, XXREAL_0:2;
reconsider LC1 = (mlt (Line A,i),(Col B,j)) | (Seg (k + 1)), mLC = mlt (Line A,i),(Col B,j) as FinSequence of the carrier of K by FINSEQ_1:23;
take LC1 ; :: thesis:
the multF of K .: (Line A,i),(Col B,j) is Element of m -tuples_on the carrier of K by A1, FINSEQ_2:140;
then len mLC = m by FINSEQ_1:def 18;
then A49: k + 1 in dom mLC by A17, FINSEQ_1:def 3;
A50: k + 1 in Seg m by A15, A16;
then A51: (Line A,i) . (k + 1) = A * i,(k + 1) by A1, MATRIX_1:def 8;
Seg m = dom B by FINSEQ_1:def 3;
then (Col B,j) . (k + 1) = B * (k + 1),j by A50, MATRIX_1:def 9;
then A52: mLC . (k + 1) = (A * i,(k + 1)) * (B * (k + 1),j) by A51, A49, FVSUM_1:73;
LC1 = LC ^ <*(mLC . (k + 1))*> by A47, A49, FINSEQ_5:11;
then A53: the addF of K "**" LC1 = the addF of K . (Fk . j),((A * i,(k + 1)) * (B * (k + 1),j)) by A48, A52, FINSOP_1:5, FVSUM_1:10;
j in dom Fk by A41, A45, FINSEQ_1:def 3;
then Fk . j in rng Fk by FUNCT_1:def 5;
then reconsider Fkj = Fk . j as Element of the carrier of K by A43;
Fk1 . j = Fkj + Pk1j by A42, A38, A45, FVSUM_1:21;
hence ( LC1 = (mlt (Line A,i),(Col B,j)) | (Seg (k + 1)) & the addF of K "**" LC1 = Fk1 . j ) by A40, A45, A46, A44, A53, FVSUM_1:62; :: thesis:

end;

set L = Line (A * B),i;
width (A * B) = w by A1, MATRIX_3:def 4;
then A54: len (Line (A * B),i) = w by MATRIX_1:def 8;
(addFinS K) "**" P is Element of the carrier of K * ;
then reconsider Fm = F . m as FinSequence of the carrier of K by A4, A12;
A55: S₁[ 0 ] ;
A56: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A55, A13);
A57: for j being Nat st 1 <= j & j <= len (Line (A * B),i) holds
(Line (A * B),i) . j = Fm . j

proof

set AB = A * B;
set LA = Line A,i;
let j be Nat; :: thesis:
assume that
A58: 1 <= j and
A59: j <= len (Line (A * B),i) ; :: thesis:
set CB = Col B,j;
the multF of K .: (Line A,i),(Col B,j) is Element of m -tuples_on the carrier of K by A1, FINSEQ_2:140;
then len (mlt (Line A,i),(Col B,j)) = m by FINSEQ_1:def 18;
then A60: dom (mlt (Line A,i),(Col B,j)) = Seg m by FINSEQ_1:def 3;
j in NAT by ORDINAL1:def 13;
then A61: j in Seg w by A54, A58, A59;
then ex LC being FinSequence of the carrier of K st
( LC = (mlt (Line A,i),(Col B,j)) | (Seg m) & the addF of K "**" LC = Fm . j ) by A9, A56;
then A62: Fm . j = (Line A,i) "*" (Col B,j) by A60, RELAT_1:98;
A63: len (A * B) = len A by A1, MATRIX_3:def 4;
A64: width (A * B) = w by A1, MATRIX_3:def 4;
len A <> 0 by A3;
then A * B is Matrix of len A,w,K by A63, A64, MATRIX_1:20;
then Indices (A * B) = [:(Seg (len A)),(Seg w):] by A64, MATRIX_1:26;
then [i,j] in Indices (A * B) by A3, A61, ZFMISC_1:106;
then (A * B) * i,j = (Line A,i) "*" (Col B,j) by A1, MATRIX_3:def 4;
hence (Line (A * B),i) . j = Fm . j by A61, A62, A64, MATRIX_1:def 8; :: thesis:

end;

take P ; :: thesis:
thus len P = len B by A4; :: thesis:
len Fm = w by A9, A56;
hence Line (A * B),i = (addFinS K) "**" P by A4, A12, A54, A57, FINSEQ_1:18; :: thesis:
let j be Nat; :: thesis:
assume j in Seg (len B) ; :: thesis:
hence P . j = (A * i,j) * (Line B,j) by A5, A6; :: thesis: