let n be Nat; :: thesis:
let K be Ring; :: thesis:
let A, B be Matrix of n,n,K; :: thesis:
let i be Nat; :: thesis:
assume that
A1: i <= n and
A2: 0 < n ; :: thesis:
set KK = the carrier of K;
set I = idseq n;
set Sn = Seg n;
set Si = Seg i;
set mm = the multF of K;
set FF = Funcs ((Seg i),(Seg n));
reconsider Sn = Seg n as non empty set by A2;
set AB = A * B;
reconsider AB = A * B as Matrix of n,K ;
defpred S₁[ object , object ] means for F being Function of (Seg i),(Seg n) st F = $1 holds
for M being Matrix of n,n,K st M = (A * B) +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = (A * B) . j ) ) ) holds
ex Path being FinSequence of K st
( len Path = i & ( for Fj, j being Nat st j in Seg i & Fj = F . j holds
Path . j = A * (j,Fj) ) & $2 = ( the multF of K $$ Path) * (Det M) );
ex f being Function st
( dom f = Seg i & rng f c= Sn ) by FUNCT_1:8;
then reconsider FF = Funcs ((Seg i),(Seg n)) as non empty set ;
A3: for x being Element of FF ex y being Element of the carrier of K st S₁[x,y]

let x be Element of FF; :: thesis:
reconsider F = x as Function of (Seg i),Sn by FUNCT_2:66;
defpred S₂[ object , object ] means for Fj, j being Nat st j = $1 & Fj = F . j holds
$2 = A * (j,Fj);
A4: i is Element of NAT by ORDINAL1:def 12;
A5: for x9 being object st x9 in Seg i holds
ex y being object st
( y in the carrier of K & S₂[x9,y] )

let x9 be object ; :: thesis:
assume A6: x9 in Seg i ; :: thesis:
reconsider i = x9 as Nat by A6;
A7: rng F c= Seg n by RELAT_1:def 19;
Seg i = dom F by FUNCT_2:def 1;
then F . i in rng F by A6, FUNCT_1:def 3;
then F . i in Sn by A7;
then reconsider Fi = F . i as Nat ;
take A * (i,Fi) ; :: thesis:
thus ( A * (i,Fi) in the carrier of K & S₂[x9,A * (i,Fi)] ) ; :: thesis:

end;

consider path being Function of (Seg i), the carrier of K such that
A8: for x being object st x in Seg i holds
S₂[x,path . x] from FUNCT_2:sch 1(A5);
dom path = Seg i by FUNCT_2:def 1;
then reconsider p = path as FinSequence by FINSEQ_1:def 2;
rng path c= the carrier of K by RELAT_1:def 19;
then reconsider p = p as FinSequence of K by FINSEQ_1:def 4;
consider M being Matrix of n,K such that
M = AB +* ((B * ((idseq n) +* F)) | (Seg i)) and
A9: for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = AB . j ) ) by A1, A2, Th59;
take ( the multF of K $$ p) * (Det M) ; :: thesis:
let F9 be Function of (Seg i),(Seg n); :: thesis:
assume A10: F9 = x ; :: thesis:
let M9 be Matrix of n,n,K; :: thesis:
assume that
M9 = (A * B) +* ((B * ((idseq n) +* F9)) | (Seg i)) and
A11: for j being Nat holds
( ( j in Seg i implies M9 . j = B . (F9 . j) ) & ( not j in Seg i implies M9 . j = (A * B) . j ) ) ; :: thesis:
take p ; :: thesis:
dom path = Seg i by FUNCT_2:def 1;
hence ( len p = i & ( for Fj, j being Nat st j in Seg i & Fj = F9 . j holds
p . j = A * (j,Fj) ) ) by A8, A10, A4, FINSEQ_1:def 3; :: thesis:
A12: len M9 = n by MATRIX_0:24;

let k be Nat; :: thesis:
assume that
1 <= k and
k <= len M ; :: thesis:

then M . k = B . (F . k) by A9;
hence M . k = M9 . k by A10, A11, A14; :: thesis:

end;

then M . k = AB . k by A9;
hence M . k = M9 . k by A11, A15; :: thesis:

end;

end;

consider P being Function of FF, the carrier of K such that
A16: for x being Element of FF holds S₁[x,P . x] from FUNCT_2:sch 3(A3);
reconsider P = P as Function of (Funcs ((Seg i),(Seg n))), the carrier of K ;
take P ; :: thesis:
let F be Function of (Seg i),(Seg n); :: thesis:
reconsider F9 = F as Function of (Seg i),Sn ;
let M be Matrix of n,K; :: thesis:
assume that
A17: M = (A * B) +* ((B * ((idseq n) +* F)) | (Seg i)) and
A18: for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = (A * B) . j ) ) ; :: thesis:
F9 in FF by FUNCT_2:8;
hence ex Path being FinSequence of K st
( len Path = i & ( for Fj, j being Nat st j in Seg i & Fj = F . j holds
Path . j = A * (j,Fj) ) & P . F = ( the multF of K $$ Path) * (Det M) ) by A16, A17, A18; :: thesis: