let K be Ring; :: 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:29
.= Seg (len B) by FINSEQ_1:def 3 ;
rng P c= the carrier of K *

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng P ; :: thesis:
then consider x being object such that
A7: x in dom P and
A8: y = P . x by FUNCT_1:def 3;
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 sequence of ( the carrier of K *) such that
A10: F . 1 = P . 1 and
A11: for n being 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 Nat st S₁[k] holds
S₁[k + 1]

proof

let k be 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_0:def 7;
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_0:def 7;
then A24: Fk1 . j = (A * (i,1)) * (B * (1,j)) by A10, A18, A19, A20, A23, FVSUM_1:50;
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:18;
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:120;
then len mLC = m by CARD_1:def 7;
then A26: dom mLC = Seg m by FINSEQ_1:def 3;
Seg 1 = (Seg m) /\ (Seg 1) by A2, FINSEQ_1:7, NAT_1:14;
then A27: dom LC1 = Seg 1 by A19, A26, RELAT_1:61;
then A28: len LC1 = 1 by FINSEQ_1:def 3;
1 in Seg 1 ;
then LC1 . 1 = mLC . 1 by A27, FUNCT_1:47;
then A29: LC1 = <*(mLC . 1)*> by A28, FINSEQ_1:40;
take LC1 ; :: thesis:
A30: 1 in Seg m by A9;
len mLC = m by A25, CARD_1:def 7;
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_0:def 8;
(Line (A,i)) . 1 = A * (i,1) by A1, A30, MATRIX_0:def 7;
then mLC . 1 = (A * (i,1)) * (B * (1,j)) by A32, A31, FVSUM_1:60;
hence ( LC1 = (mlt ((Line (A,i)),(Col (B,j)))) | (Seg (k + 1)) & the addF of K "**" LC1 = Fk1 . j ) by A24, A29, FINSOP_1:11; :: 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 3;
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;
reconsider Pk1 = Pk1, Fk = Fk as Element of the carrier of K * by FINSEQ_1:def 11;
A35: (addFinS K) . (Fk,Pk1) = Fk + Pk1 by Def5;
A36: k + 0 < k + 1 by XREAL_1:8;
then k < m by A16, XXREAL_0:2;
then A37: Fk1 = Fk + Pk1 by A4, A11, A18, A33, A35;
A38: len (Line (B,(k + 1))) = w by MATRIX_0:def 7;
Pk1 = H₁(k + 1) by A5, A6, A17;
then len Pk1 = w by A38, Lm5;
then A39: dom Pk1 = Seg w by FINSEQ_1:def 3;
A40: w in NAT by ORDINAL1:def 12;
A41: len Fk = w by A14, A16, A33, A36, 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 A39, Lm9;
hence len Fk1 = w by A37, FINSEQ_1:def 3, A40; :: 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_0:def 7;
then Pk1 . j = (A * (i,(k + 1))) * (B * ((k + 1),j)) by A39, A45, A44, FVSUM_1:50;
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, A36, 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:18;
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:120;
then len mLC = m by CARD_1:def 7;
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_0:def 7;
Seg m = dom B by FINSEQ_1:def 3;
then (Col (B,j)) . (k + 1) = B * ((k + 1),j) by A50, MATRIX_0:def 8;
then A52: mLC . (k + 1) = (A * (i,(k + 1))) * (B * ((k + 1),j)) by A51, A49, FVSUM_1:60;
LC1 = LC ^ <*(mLC . (k + 1))*> by A47, A49, FINSEQ_5:10;
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:4, FVSUM_1:8;
j in dom Fk by A41, A45, FINSEQ_1:def 3;
then Fk . j in rng Fk by FUNCT_1:def 3;
then reconsider Fkj = Fk . j as Element of the carrier of K by A43;
Fk1 . j = Fkj + Pk1j by A42, A37, A45, FVSUM_1:17;
hence ( LC1 = (mlt ((Line (A,i)),(Col (B,j)))) | (Seg (k + 1)) & the addF of K "**" LC1 = Fk1 . j ) by A39, A45, A46, A44, A53, FVSUM_1:50; :: 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_0:def 7;
reconsider Fm = F . m as FinSequence of the carrier of K ;
A55: S₁[ 0 ] ;
A56: for k being Nat holds S₁[k] from NAT_1:sch 2(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:120;
then len (mlt ((Line (A,i)),(Col (B,j)))) = m by CARD_1:def 7;
then A60: dom (mlt ((Line (A,i)),(Col (B,j)))) = Seg m by FINSEQ_1:def 3;
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;
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_0:20;
then Indices (A * B) = [:(Seg (len A)),(Seg w):] by A64, MATRIX_0:25;
then [i,j] in Indices (A * B) by A3, A61, ZFMISC_1:87;
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_0:def 7; :: 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; :: 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: