let K be Field; :: thesis:
let A, B be Matrix of K; :: thesis:
assume A1: ( width A = len B & len B > 0 ) ; :: thesis:
let i be Nat; :: thesis:
assume A2: i in Seg (len A) ; :: thesis:
set KK = the carrier of K;
set a = addFinS K;
set mm = the multF of K;
set aa = the addF of K;
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
A3: len P = len B and
A4: for k being Nat st k in dom P holds
P . k = H₁(k) from FINSEQ_1:sch 2();
A5: dom P = dom B by A3, FINSEQ_3:31
.= Seg (len B) by FINSEQ_1:def 3 ;
reconsider m = len B, w = width B as Nat ;
rng P c= the carrier of K *

proof

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

end;

then reconsider P = P as FinSequence of the carrier of K * by FINSEQ_1:def 4;
take P ; :: thesis:
thus len P = len B by A3; :: thesis:
A9: m >= 1 by A1, 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 A3, 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: S₁[ 0 ] ;
A14: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A15: S₁[k] ; :: thesis:
set k1 = k + 1;
assume A16: ( 1 <= k + 1 & k + 1 <= m ) ; :: thesis:
then A17: k + 1 in Seg m ;
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: ( Fk1 = P . 1 & P . 1 = (A * i,1) * (Line B,1) & len (Line B,1) = w ) by A4, A10, A17, A18, A5, MATRIX_1:def 8;
hence len Fk1 = w by Lm5; :: thesis:
let j be Element of NAT ; :: thesis:
assume A21: j in Seg w ; :: thesis:
set L = Line A,i;
set C = Col B,j;
A22: 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;
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:
( 1 in Seg m & Seg m = dom B & len mLC = m ) by A9, A22, FINSEQ_1:def 3, FINSEQ_1:def 18;
then A23: ( (Line A,i) . 1 = A * i,1 & (Col B,j) . 1 = B * 1,j & (Line B,1) . j = B * 1,j & 1 in dom mLC ) by A1, A21, FINSEQ_1:def 3, MATRIX_1:def 8, MATRIX_1:def 9;
then A24: mLC . 1 = (A * i,1) * (B * 1,j) by FVSUM_1:73;
len Fk1 = w by A20, Lm5;
then j in dom Fk1 by A21, FINSEQ_1:def 3;
then A25: Fk1 . j = (A * i,1) * (B * 1,j) by A20, A23, FVSUM_1:62;
len mLC = m by A22, FINSEQ_1:def 18;
then ( dom mLC = Seg m & Seg 1 = (Seg m) /\ (Seg 1) ) by A9, FINSEQ_1:9, FINSEQ_1:def 3;
then ( dom LC1 = Seg 1 & 1 in Seg 1 ) by A19, RELAT_1:90;
then ( len LC1 = 1 & LC1 . 1 = mLC . 1 ) by FINSEQ_1:def 3, FUNCT_1:70;
then LC1 = <*(mLC . 1)*> by FINSEQ_1:57;
hence ( LC1 = (mlt (Line A,i),(Col B,j)) | (Seg (k + 1)) & the addF of K "**" LC1 = Fk1 . j ) by A24, A25, FINSOP_1:12; :: thesis:

end;

suppose A26: k > 0 ; :: thesis:

dom P = Seg m by A3, FINSEQ_1:def 3;
then ( P . (k + 1) in rng P & rng P c= the carrier of K * ) by A17, FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider Pk1 = P . (k + 1), Fk = F . k as FinSequence of the carrier of K by FINSEQ_1:def 11;
( Pk1 = H₁(k + 1) & len (Line B,(k + 1)) = w ) by A4, A17, A5, MATRIX_1:def 8;
then len Pk1 = w by Lm5;
then A27: dom Pk1 = Seg w by FINSEQ_1:def 3;
A28: k + 0 < k + 1 by XREAL_1:10;
then A29: len Fk = w by A15, A16, A26, NAT_1:14, XXREAL_0:2;
then ( dom Fk = Seg w & Fk is Element of the carrier of K * & Pk1 is Element of the carrier of K * ) by FINSEQ_1:def 3, FINSEQ_1:def 11;
then A30: ( dom (Fk + Pk1) = (Seg w) /\ (Seg w) & (addFinS K) . Fk,Pk1 = Fk + Pk1 & k < m ) by A16, A27, A28, Def5, Lm9, XXREAL_0:2;
then A31: ( len (Fk + Pk1) = w & Fk1 = Fk + Pk1 ) by A3, A11, A18, A26, FINSEQ_1:def 3;
hence len Fk1 = w ; :: thesis:
let j be Element of NAT ; :: thesis:
assume A32: j in Seg w ; :: thesis:
set L = Line A,i;
set C = Col B,j;
consider LC being FinSequence of the carrier of K such that
A33: ( LC = (mlt (Line A,i),(Col B,j)) | (Seg k) & the addF of K "**" LC = Fk . j ) by A15, A16, A26, A28, A32, NAT_1:14, XXREAL_0:2;
A34: 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;
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:
( k + 1 in Seg m & Seg m = dom B ) by A16, FINSEQ_1:def 3;
then A35: ( (Line A,i) . (k + 1) = A * i,(k + 1) & (Col B,j) . (k + 1) = B * (k + 1),j & (Line B,(k + 1)) . j = B * (k + 1),j ) by A1, A32, MATRIX_1:def 8, MATRIX_1:def 9;
j in dom Fk by A29, A32, FINSEQ_1:def 3;
then ( Fk . j in rng Fk & rng Fk c= the carrier of K ) by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider Fkj = Fk . j as Element of the carrier of K ;
A36: Pk1 = H₁(k + 1) by A4, A17, A5;
then Pk1 . j = (A * i,(k + 1)) * (B * (k + 1),j) by A27, A32, A35, FVSUM_1:62;
then reconsider Pk1j = Pk1 . j as Element of the carrier of K ;
len mLC = m by A34, FINSEQ_1:def 18;
then k + 1 in dom mLC by A17, FINSEQ_1:def 3;
then ( LC1 = LC ^ <*(mLC . (k + 1))*> & mLC . (k + 1) = (A * i,(k + 1)) * (B * (k + 1),j) & the addF of K is having_a_unity ) by A33, A35, FINSEQ_5:11, FVSUM_1:10, FVSUM_1:73;
then ( the addF of K "**" LC1 = the addF of K . (Fk . j),((A * i,(k + 1)) * (B * (k + 1),j)) & j in dom Fk1 ) by A3, A11, A18, A26, A30, A32, A33, FINSOP_1:5;
then ( the addF of K "**" LC1 = Fkj + Pk1j & Fk1 . j = Fkj + Pk1j ) by A27, A31, A32, A35, A36, FVSUM_1:21, FVSUM_1:62;
hence ( LC1 = (mlt (Line A,i),(Col B,j)) | (Seg (k + 1)) & the addF of K "**" LC1 = Fk1 . j ) ; :: thesis:

end;

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

proof

let j be Nat; :: thesis:
assume A40: ( 1 <= j & j <= len (Line (A * B),i) ) ; :: thesis:
set LA = Line A,i;
set CB = Col B,j;
set AB = A * B;
j in NAT by ORDINAL1:def 13;
then A41: j in Seg w by A39, A40;
then consider LC being FinSequence of the carrier of K such that
A42: ( LC = (mlt (Line A,i),(Col B,j)) | (Seg m) & the addF of K "**" LC = Fm . j ) by A9, A37;
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 dom (mlt (Line A,i),(Col B,j)) = Seg m by FINSEQ_1:def 3;
then A43: Fm . j = (Line A,i) "*" (Col B,j) by A42, RELAT_1:98;
len A <> 0 by A2;
then A44: ( len A > 0 & len (A * B) = len A & width (A * B) = w ) by A1, MATRIX_3:def 4;
then A * B is Matrix of len A,w,K by MATRIX_1:20;
then Indices (A * B) = [:(Seg (len A)),(Seg w):] by A44, MATRIX_1:26;
then [i,j] in Indices (A * B) by A2, A41, 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 A41, A43, A44, MATRIX_1:def 8; :: thesis:

end;

hence Line (A * B),i = (addFinS K) "**" P by A3, A12, A38, A39, FINSEQ_1:18; :: thesis:
let j be Nat; :: thesis:
assume A45: j in Seg (len B) ; :: thesis:
thus P . j = (A * i,j) * (Line B,j) by A4, A45, A5; :: thesis: