let n be Nat; :: thesis: for K being Field
for A, B being Matrix of n,n,K
for i being Nat st i <= n & 0 < n holds
ex P being Function of (Funcs (Seg i),(Seg n)),the carrier of K st
for F being Function of (Seg i),(Seg n)
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 ) & P . F = (the multF of K $$ Path) * (Det M) )
let K be Field; :: thesis: for A, B being Matrix of n,n,K
for i being Nat st i <= n & 0 < n holds
ex P being Function of (Funcs (Seg i),(Seg n)),the carrier of K st
for F being Function of (Seg i),(Seg n)
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 ) & P . F = (the multF of K $$ Path) * (Det M) )
let A, B be Matrix of n,n,K; :: thesis: for i being Nat st i <= n & 0 < n holds
ex P being Function of (Funcs (Seg i),(Seg n)),the carrier of K st
for F being Function of (Seg i),(Seg n)
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 ) & P . F = (the multF of K $$ Path) * (Det M) )
let i be Nat; :: thesis: ( i <= n & 0 < n implies ex P being Function of (Funcs (Seg i),(Seg n)),the carrier of K st
for F being Function of (Seg i),(Seg n)
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 ) & P . F = (the multF of K $$ Path) * (Det M) ) )
assume A1: ( i <= n & 0 < n ) ; :: thesis: ex P being Function of (Funcs (Seg i),(Seg n)),the carrier of K st
for F being Function of (Seg i),(Seg n)
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 ) & P . F = (the multF of K $$ Path) * (Det M) )
set mm = the multF of K;
set Si = Seg i;
set Sn = Seg n;
set I = idseq n;
set AB = A * B;
set FF = Funcs (Seg i),(Seg n);
set KK = the carrier of K;
reconsider Sn = Seg n as non empty set by A1;
ex f being Function st
( dom f = Seg i & rng f c= Sn ) by FUNCT_1:18;
then reconsider FF = Funcs (Seg i),(Seg n) as non empty set ;
reconsider AB = A * B as Matrix of n,K ;
defpred S1[ set , set ] 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) );
A2: for x being Element of FF ex y being Element of the carrier of K st S1[x,y]
proof
let x be Element of FF; :: thesis: ex y being Element of the carrier of K st S1[x,y]
reconsider F = x as Function of (Seg i),Sn by FUNCT_2:121;
consider M being Matrix of n,K such that
M = AB +* ((B * ((idseq n) +* F)) | (Seg i)) and
A3: 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, Th59;
defpred S2[ set , set ] means for Fj, j being Nat st j = $1 & Fj = F . j holds
$2 = A * j,Fj;
A4: for x' being set st x' in Seg i holds
ex y being set st
( y in the carrier of K & S2[x',y] )
proof
let x' be set ; :: thesis: ( x' in Seg i implies ex y being set st
( y in the carrier of K & S2[x',y] ) )
assume A5: x' in Seg i ; :: thesis: ex y being set st
( y in the carrier of K & S2[x',y] )
reconsider i = x' as Nat by A5;
Seg i = dom F by FUNCT_2:def 1;
then ( F . i in rng F & rng F c= Seg n ) by A5, FUNCT_1:def 5, RELAT_1:def 19;
then F . i in Sn ;
then reconsider Fi = F . i as Nat ;
take Y = A * i,Fi; :: thesis: ( Y in the carrier of K & S2[x',Y] )
thus ( Y in the carrier of K & S2[x',Y] ) ; :: thesis: verum
end;
consider path being Function of (Seg i),the carrier of K such that
A6: for x being set st x in Seg i holds
S2[x,path . x] from FUNCT_2:sch 1(A4);
 ( dom path = Seg i & i is Element of NAT ) by FUNCT_2:def 1, ORDINAL1:def 13;
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;
take MM = (the multF of K $$ p) * (Det M); :: thesis: S1[x,MM]
let F' be Function of (Seg i),(Seg n); :: thesis: ( F' = x implies 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 ) & MM = (the multF of K $$ Path) * (Det M) ) )
assume A7: F' = x ; :: thesis: 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 ) & MM = (the multF of K $$ Path) * (Det M) )
let M' be Matrix of n,n,K; :: thesis: ( 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 ) ) ) implies 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 ) & MM = (the multF of K $$ Path) * (Det M') ) )
assume that
M' = (A * B) +* ((B * ((idseq n) +* F')) | (Seg i)) and
A8: 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: 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 ) & MM = (the multF of K $$ Path) * (Det M') )
take p ; :: thesis: ( len p = i & ( for Fj, j being Nat st j in Seg i & Fj = F' . j holds
p . j = A * j,Fj ) & MM = (the multF of K $$ p) * (Det M') )
( dom path = Seg i & i is Element of NAT ) by FUNCT_2:def 1, ORDINAL1:def 13;
hence ( len p = i & ( for Fj, j being Nat st j in Seg i & Fj = F' . j holds
p . j = A * j,Fj ) ) by A6, A7, FINSEQ_1:def 3; :: thesis: MM = (the multF of K $$ p) * (Det M')
A9: ( len M = n & len M' = n ) by MATRIX_1:25;
now
let k be Nat; :: thesis: ( 1 <= k & k <= len M implies M . b1 = M' . b1 )
assume ( 1 <= k & k <= len M ) ; :: thesis: M . b1 = M' . b1
per cases ( k in Seg i or not k in Seg i ) ;
suppose k in Seg i ; :: thesis: M . b1 = M' . b1
then ( M . k = B . (F . k) & M' . k = B . (F' . k) ) by A3, A8;
hence M . k = M' . k by A7; :: thesis: verum
end;
suppose not k in Seg i ; :: thesis: M . b1 = M' . b1
then ( M . k = AB . k & M' . k = AB . k ) by A3, A8;
hence M . k = M' . k ; :: thesis: verum
end;
end;
end;
hence MM = (the multF of K $$ p) * (Det M') by A9, FINSEQ_1:18; :: thesis: verum
end;
consider P being Function of FF,the carrier of K such that
A10: for x being Element of FF holds S1[x,P . x] from FUNCT_2:sch 3(A2);
 reconsider P = P as Function of (Funcs (Seg i),(Seg n)),the carrier of K ;
take P ; :: thesis: for F being Function of (Seg i),(Seg n)
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 ) & P . F = (the multF of K $$ Path) * (Det M) )
let F be Function of (Seg i),(Seg n); :: thesis: 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 ) & P . F = (the multF of K $$ Path) * (Det M) )
reconsider F' = F as Function of (Seg i),Sn ;
let M be Matrix of n,K; :: thesis: ( 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 ) ) ) implies 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) ) )
assume that
A11: M = (A * B) +* ((B * ((idseq n) +* F)) | (Seg i)) and
A12: 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: 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) )
F' in FF by FUNCT_2:11;
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 A10, A11, A12; :: thesis: verum