let n be Nat; :: thesis:
let K be Field; :: thesis:
let A, B be Matrix of n,K; :: thesis:
assume A1: 0 < n ; :: thesis:
set AB = A * B;
set aa = the addF of K;
set I = idseq n;
set mm = the multF of K;
set KK = the carrier of K;
defpred S₁[ Function, Nat] means for F being Function of (Seg $2),(Seg n)
for M being Matrix of n,n,K st M = (A * B) +* ((B * ((idseq n) +* F)) | (Seg $2)) & ( for j being Nat holds
( ( j in Seg $2 implies M . j = B . (F . j) ) & ( not j in Seg $2 implies M . j = (A * B) . j ) ) ) holds
ex Path being FinSequence of K st
( len Path = $2 & ( for Fj, j being Nat st j in Seg $2 & Fj = F . j holds
Path . j = A * j,Fj ) & $1 . F = (the multF of K $$ Path) * (Det M) );
defpred S₂[ Nat] means ( $1 <= n implies for FUNC being non empty set st FUNC = Funcs (Seg $1),(Seg n) holds
ex P being Function of FUNC,the carrier of K st
( S₁[P,$1] & Det (A * B) = the addF of K $$ (FinOmega FUNC),P ) );
A2: for k being Element of NAT st S₂[k] holds
S₂[k + 1]

set Y = Seg n;
let k be Element of NAT ; :: thesis:
assume A3: S₂[k] ; :: thesis:
set X = Seg k;
reconsider FUNC = Funcs (Seg k),(Seg n) as non empty set by A1;
set k1 = k + 1;
assume A4: k + 1 <= n ; :: thesis:
set Xx = (Seg k) \/ {(k + 1)};
let FUNC1 be non empty set ; :: thesis:
assume A5: FUNC1 = Funcs (Seg (k + 1)),(Seg n) ; :: thesis:
consider P1 being Function of FUNC1,the carrier of K such that
A6: S₁[P1,k + 1] by A4, A5, Lm10;
reconsider FUNC19 = Funcs ((Seg k) \/ {(k + 1)}),(Seg n) as non empty set by A5, FINSEQ_1:11;
A7: FUNC1 = Funcs ((Seg k) \/ {(k + 1)}),(Seg n) by A5, FINSEQ_1:11;
then reconsider P19 = P1 as Function of FUNC19,the carrier of K ;
A8: k + 0 <= k + 1 by XREAL_1:10;
then consider P being Function of FUNC,the carrier of K such that
A9: S₁[P,k] and
A10: Det (A * B) = the addF of K $$ (FinOmega FUNC),P by A3, A4, XXREAL_0:2;
A11: not k + 1 in Seg k by FINSEQ_3:9;
A12: for H being Function of (Seg k),(Seg n)
for SF being Element of Fin FUNC19 st SF = { h where h is Function of ((Seg k) \/ {(k + 1)}),(Seg n) : h | (Seg k) = H } holds
the addF of K $$ SF,P19 = P . H

reconsider YY = Seg n as non empty set by A1;
let H be Function of (Seg k),(Seg n); :: thesis:
let SF be Element of Fin FUNC19; :: thesis:
assume A13: SF = { h where h is Function of ((Seg k) \/ {(k + 1)}),(Seg n) : h | (Seg k) = H } ; :: thesis:
defpred S₃[ set , set ] means for h being Function of ((Seg k) \/ {(k + 1)}),(Seg n) st h | (Seg k) = H & h . (k + 1) = $1 holds
h = $2;
A14: for y being set st y in YY holds
ex f9 being set st
( f9 in SF & S₃[y,f9] )

proof

let y be set ; :: thesis:
assume y in YY ; :: thesis:
then (Seg n) \/ {y} = Seg n by ZFMISC_1:46;
then consider q being Function of ((Seg k) \/ {(k + 1)}),(Seg n) such that
A15: q | (Seg k) = H and
A16: q . (k + 1) = y by A11, STIRL2_1:67;
take q ; :: thesis:
thus q in SF by A13, A15; :: thesis:
let h be Function of ((Seg k) \/ {(k + 1)}),(Seg n); :: thesis:
assume that
A17: h | (Seg k) = H and
A18: h . (k + 1) = y ; :: thesis:

now

let x be set ; :: thesis:
assume x in (Seg k) \/ {(k + 1)} ; :: thesis:
then A19: ( x in Seg k or x in {(k + 1)} ) by XBOOLE_0:def 3;
dom H = Seg k by A1, FUNCT_2:def 1;
then ( ( q . x = H . x & h . x = H . x ) or x = k + 1 ) by A15, A17, A19, FUNCT_1:70, TARSKI:def 1;
hence h . x = q . x by A16, A18; :: thesis:

end;

hence h = q by FUNCT_2:18; :: thesis:

end;

consider QQ being Function of YY,SF such that
A20: for y being set st y in YY holds
S₃[y,QQ . y] from FUNCT_2:sch 1(A14);
A21: SF c= rng QQ

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
k + 1 in {(k + 1)} by TARSKI:def 1;
then A22: k + 1 in (Seg k) \/ {(k + 1)} by XBOOLE_0:def 3;
assume A23: y in SF ; :: thesis:
then consider h being Function of ((Seg k) \/ {(k + 1)}),(Seg n) such that
A24: y = h and
A25: h | (Seg k) = H by A13;
dom h = (Seg k) \/ {(k + 1)} by A1, FUNCT_2:def 1;
then A26: h . (k + 1) in rng h by A22, FUNCT_1:def 5;
A27: rng h c= Seg n by RELAT_1:def 19;
dom QQ = YY by A23, FUNCT_2:def 1;
then QQ . (h . (k + 1)) in rng QQ by A26, A27, FUNCT_1:def 5;
hence y in rng QQ by A20, A24, A25, A26, A27; :: thesis:

end;

rng QQ c= SF by RELAT_1:def 19;
then A28: rng QQ = SF by A21, XBOOLE_0:def 10;
(Seg n) \/ {n} = Seg n by A1, FINSEQ_1:5, ZFMISC_1:46;
then consider h being Function of ((Seg k) \/ {(k + 1)}),(Seg n) such that
A29: h | (Seg k) = H and
h . (k + 1) = n by A11, STIRL2_1:67;
A30: SF c= FUNC19 by FINSUB_1:def 5;
k <= n by A4, A8, XXREAL_0:2;
then consider Mh being Matrix of n,K such that
A31: Mh = (A * B) +* ((B * ((idseq n) +* H)) | (Seg k)) and
A32: for j being Nat holds
( ( j in Seg k implies Mh . j = B . (H . j) ) & ( not j in Seg k implies Mh . j = (A * B) . j ) ) by A1, Th59;
consider Path being FinSequence of K such that
A33: len Path = k and
A34: for Hj, j being Nat st j in Seg k & Hj = H . j holds
Path . j = A * j,Hj and
A35: P . H = (the multF of K $$ Path) * (Det Mh) by A9, A31, A32;
A36: Mh . (k + 1) = (A * B) . (k + 1) by A11, A32;
h in SF by A13, A29;
then reconsider QQ = QQ as Function of YY,FUNC19 by A28, A30, FUNCT_2:8;
A37: dom (P19 * QQ) = Seg n by FUNCT_2:def 1;
A38: QQ .: (dom QQ) = SF by A28, RELAT_1:146;
1 + 0 <= k + 1 by XREAL_1:9;
then A39: k + 1 in Seg n by A4;
then A40: (A * B) . (k + 1) = Line (A * B),(k + 1) by MATRIX_2:10;
Mh . (k + 1) = Line Mh,(k + 1) by A39, MATRIX_2:10;
then Mh = RLine Mh,(k + 1),(Line (A * B),(k + 1)) by A36, A40, Th30;
then consider SUM1 being FinSequence of the carrier of K such that
A41: len SUM1 = n and
A42: Det Mh = the addF of K "**" SUM1 and
A43: for j being Nat st j in Seg n holds
SUM1 . j = (A * (k + 1),j) * (Det (RLine Mh,(k + 1),(Line B,j))) by A39, Th56;
A44: dom (id (Seg n)) = Seg n by RELAT_1:71;
set PA = the multF of K "**" Path;
set PS = (the multF of K "**" Path) * SUM1;
len ((the multF of K "**" Path) * SUM1) = n by A41, Lm5;
then A45: dom ((the multF of K "**" Path) * SUM1) = Seg n by FINSEQ_1:def 3;
set PSaa = [#] ((the multF of K "**" Path) * SUM1),(the_unity_wrt the addF of K);
A46: for j being Nat st j in Seg n holds
(P19 * QQ) . j = ((the multF of K "**" Path) * (A * (k + 1),j)) * (Det (RLine Mh,(k + 1),(Line B,j)))

proof

A47: width B = n by MATRIX_1:25;
A48: len Mh = n by MATRIX_1:25;
A49: dom (P19 * QQ) = Seg n by FUNCT_2:def 1;
A50: width Mh = n by MATRIX_1:25;
let j be Nat; :: thesis:
assume A51: j in Seg n ; :: thesis:
(Seg n) \/ {j} = Seg n by A51, ZFMISC_1:46;
then consider hj being Function of ((Seg k) \/ {(k + 1)}),(Seg n) such that
A52: hj | (Seg k) = H and
A53: hj . (k + 1) = j by A11, STIRL2_1:67;
set L = Line B,j;
set R = RLine Mh,(k + 1),(Line B,j);
(Seg k) \/ {(k + 1)} = Seg (k + 1) by FINSEQ_1:11;
then reconsider hj9 = hj as Function of (Seg (k + 1)),(Seg n) ;
consider Mhj being Matrix of n,K such that
A54: Mhj = (A * B) +* ((B * ((idseq n) +* hj9)) | (Seg (k + 1))) and
A55: for i being Nat holds
( ( i in Seg (k + 1) implies Mhj . i = B . (hj9 . i) ) & ( not i in Seg (k + 1) implies Mhj . i = (A * B) . i ) ) by A4, Th59;
A56: len Mhj = n by MATRIX_1:25;
A57: len (Line B,j) = width B by MATRIX_1:def 8;

A58: now

A59: k + 0 < k + 1 by XREAL_1:10;
let i be Nat; :: thesis:
assume that
A60: 1 <= i and
A61: i <= len Mhj ; :: thesis:
A62: i in NAT by ORDINAL1:def 13;
then A63: i in Seg n by A56, A60, A61;

per cases ;

suppose A64: i <= k ; :: thesis:

then i <= k + 1 by A59, XXREAL_0:2;
then A65: i in Seg (k + 1) by A60, A62;
A66: Line (RLine Mh,(k + 1),(Line B,j)),i = (RLine Mh,(k + 1),(Line B,j)) . i by A63, MATRIX_2:10;
A67: i in Seg k by A60, A62, A64;
then A68: Mh . i = B . (H . i) by A32;
dom H = Seg k by A56, A60, A61, FUNCT_2:def 1;
then A69: H . i = hj . i by A52, A67, FUNCT_1:70;
A70: Line Mh,i = Mh . i by A63, MATRIX_2:10;
Line (RLine Mh,(k + 1),(Line B,j)),i = Line Mh,i by A63, A59, A64, Th28;
hence Mhj . i = (RLine Mh,(k + 1),(Line B,j)) . i by A55, A66, A70, A68, A69, A65; :: thesis:

end;

suppose A71: ( i > k & i <= k + 1 ) ; :: thesis:

A72: k + 1 in Seg (k + 1) by FINSEQ_1:6;
A73: Line B,j = B . j by A51, MATRIX_2:10;
A74: (RLine Mh,(k + 1),(Line B,j)) . i = Line (RLine Mh,(k + 1),(Line B,j)),i by A63, MATRIX_2:10;
A75: i = k + 1 by A71, NAT_1:9;
then Line B,j = Line (RLine Mh,(k + 1),(Line B,j)),i by A57, A47, A50, A63, Th28;
hence Mhj . i = (RLine Mh,(k + 1),(Line B,j)) . i by A53, A55, A75, A72, A74, A73; :: thesis:

end;

suppose A76: ( i > k & i > k + 1 ) ; :: thesis:

then not i in Seg (k + 1) by FINSEQ_1:3;
then A77: Mhj . i = (A * B) . i by A55;
A78: Line (RLine Mh,(k + 1),(Line B,j)),i = (RLine Mh,(k + 1),(Line B,j)) . i by A63, MATRIX_2:10;
A79: not i in Seg k by A76, FINSEQ_1:3;
A80: Line Mh,i = Mh . i by A63, MATRIX_2:10;
Line (RLine Mh,(k + 1),(Line B,j)),i = Line Mh,i by A63, A76, Th28;
hence Mhj . i = (RLine Mh,(k + 1),(Line B,j)) . i by A32, A78, A80, A79, A77; :: thesis:

end;

len (RLine Mh,(k + 1),(Line B,j)) = len Mh by Lm4;
then RLine Mh,(k + 1),(Line B,j) = Mhj by A48, A56, A58, FINSEQ_1:18;
then consider Pathj being FinSequence of K such that
A81: len Pathj = k + 1 and
A82: for m, j being Nat st j in Seg (k + 1) & m = hj . j holds
Pathj . j = A * j,m and
A83: P1 . hj = (the multF of K "**" Pathj) * (Det (RLine Mh,(k + 1),(Line B,j))) by A6, A54, A55;
A84: Pathj . (k + 1) = A * (k + 1),j by A53, A82, FINSEQ_1:6;

A85: now

A86: rng H c= Seg n by RELAT_1:def 19;
A87: Seg k = dom H by A51, FUNCT_2:def 1;
let i be Nat; :: thesis:
assume that
A88: 1 <= i and
A89: i <= len Path ; :: thesis:
A90: (Pathj | k) . i = Pathj . i by A33, A89, FINSEQ_3:121;
A91: i in NAT by ORDINAL1:def 13;
then A92: i in Seg k by A33, A88, A89;
then H . i in rng H by A87, FUNCT_1:def 5;
then H . i in Seg n by A86;
then reconsider Hi = H . i as Nat ;
i <= k + 1 by A8, A33, A89, XXREAL_0:2;
then A93: i in Seg (k + 1) by A88, A91;
i in Seg k by A33, A88, A89, A91;
then A94: Path . i = A * i,Hi by A34;
H . i = hj . i by A52, A92, A87, FUNCT_1:70;
hence Path . i = (Pathj | (Seg k)) . i by A82, A93, A94, A90; :: thesis:

end;

len (Pathj | k) = k by A8, A81, FINSEQ_1:80;
then Pathj = Path ^ <*(Pathj . (k + 1))*> by A33, A81, A85, FINSEQ_1:18, FINSEQ_3:61;
then A95: the multF of K "**" Pathj = (the multF of K "**" Path) * (A * (k + 1),j) by A84, FINSOP_1:5;
QQ . j = hj by A20, A51, A52, A53;
hence (P19 * QQ) . j = ((the multF of K "**" Path) * (A * (k + 1),j)) * (Det (RLine Mh,(k + 1),(Line B,j))) by A51, A83, A49, A95, FUNCT_1:22; :: thesis:

end;

now

let y be set ; :: thesis:
assume A96: y in dom ((the multF of K "**" Path) * SUM1) ; :: thesis:
reconsider j = y as Nat by A96;
SUM1 . j = (A * (k + 1),j) * (Det (RLine Mh,(k + 1),(Line B,j))) by A43, A45, A96;
hence ((the multF of K "**" Path) * SUM1) . y = (the multF of K "**" Path) * ((A * (k + 1),j) * (Det (RLine Mh,(k + 1),(Line B,j)))) by A96, FVSUM_1:62
.= ((the multF of K "**" Path) * (A * (k + 1),j)) * (Det (RLine Mh,(k + 1),(Line B,j))) by GROUP_1:def 4
.= (P19 * QQ) . y by A46, A45, A96 ;
:: thesis:

end;

then (the multF of K "**" Path) * SUM1 = P19 * QQ by A37, A45, FUNCT_1:9;
then A97: ([#] ((the multF of K "**" Path) * SUM1),(the_unity_wrt the addF of K)) | (dom ((the multF of K "**" Path) * SUM1)) = P19 * QQ by SETWOP_2:23;

now

let x1, x2 be set ; :: thesis:
assume that
A98: x1 in Seg n and
A99: x2 in Seg n and
A100: QQ . x1 = QQ . x2 ; :: thesis:
(Seg n) \/ {x2} = Seg n by A99, ZFMISC_1:46;
then A101: ex h2 being Function of ((Seg k) \/ {(k + 1)}),(Seg n) st
( h2 | (Seg k) = H & h2 . (k + 1) = x2 ) by A11, STIRL2_1:67;
(Seg n) \/ {x1} = Seg n by A98, ZFMISC_1:46;
then consider h1 being Function of ((Seg k) \/ {(k + 1)}),(Seg n) such that
A102: h1 | (Seg k) = H and
A103: h1 . (k + 1) = x1 by A11, STIRL2_1:67;
QQ . x1 = h1 by A20, A98, A102, A103;
hence x1 = x2 by A20, A99, A100, A103, A101; :: thesis:

end;

then A104: QQ is one-to-one by FUNCT_2:25;
reconsider Y9 = Seg n as Element of Fin YY by FINSUB_1:def 5;
A105: dom QQ = Y9 by FUNCT_2:def 1;
A106: rng (id (Seg n)) = Seg n by RELAT_1:71;
(P19 * QQ) * (id (Seg n)) = P19 * QQ by A37, RELAT_1:78;
then the addF of K $$ Y9,(P19 * QQ) = the addF of K $$ (findom ((the multF of K "**" Path) * SUM1)),([#] ((the multF of K "**" Path) * SUM1),(the_unity_wrt the addF of K)) by A45, A44, A106, A97, SETWOP_2:7
.= Sum ((the multF of K "**" Path) * SUM1) by FVSUM_1:10, SETWOP_2:def 2
.= (the multF of K "**" Path) * (Sum SUM1) by FVSUM_1:92
.= P . H by A35, A42 ;
hence the addF of K $$ SF,P19 = P . H by A104, A38, A105, SETWOP_2:8; :: thesis:

end;

the addF of K is having_a_unity by FVSUM_1:10;
then Det (A * B) = the addF of K $$ (FinOmega FUNC19),P19 by A1, A10, A11, A12, Th58;
hence ex P being Function of FUNC1,the carrier of K st
( S₁[P,k + 1] & Det (A * B) = the addF of K $$ (FinOmega FUNC1),P ) by A6, A7; :: thesis:

end;

set FUN = Funcs (Seg n),(Seg n);
A107: n is Element of NAT by ORDINAL1:def 13;
A108: S₂[ 0 ]

proof

reconsider E = {} as Function of (Seg 0 ),(Seg n) by XBOOLE_1:2;
assume 0 <= n ; :: thesis:
A109: the_unity_wrt the multF of K = 1_ K by GROUP_1:33;
let FUNC be non empty set ; :: thesis:
assume A110: FUNC = Funcs (Seg 0 ),(Seg n) ; :: thesis:
consider P being Function of FUNC,the carrier of K such that
A111: S₁[P, 0 ] by A1, A110, Lm10;
A112: FUNC = {E} by A110, FUNCT_5:64;
then A113: E in FUNC by TARSKI:def 1;
FinOmega FUNC = {E} by A112, MATRIX_2:def 17;
then A114: the addF of K $$ (FinOmega FUNC),P = P . E by A113, SETWISEO:26;
consider M being Matrix of n,K such that
A115: M = (A * B) +* ((B * ((idseq n) +* E)) | (Seg 0 )) and
A116: for j being Nat holds
( ( j in Seg 0 implies M . j = B . (E . j) ) & ( not j in Seg 0 implies M . j = (A * B) . j ) ) by A1, Th59;
A117: M = A * B by A115, FUNCT_4:22;
consider Path being FinSequence of K such that
A118: len Path = 0 and
for Fj, j being Nat st j in Seg 0 & Fj = E . j holds
Path . j = A * j,Fj and
A119: P . E = (the multF of K $$ Path) * (Det M) by A111, A115, A116;
Path = <*> the carrier of K by A118;
then the multF of K "**" Path = 1_ K by A109, FINSOP_1:11;
then P . E = Det (A * B) by A119, A117, VECTSP_1:def 13;
hence ex P being Function of FUNC,the carrier of K st
( S₁[P, 0 ] & Det (A * B) = the addF of K $$ (FinOmega FUNC),P ) by A111, A114; :: thesis:

end;

for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A108, A2);
then consider P being Function of (Funcs (Seg n),(Seg n)),the carrier of K such that
A120: S₁[P,n] and
A121: Det (A * B) = the addF of K $$ (FinOmega (Funcs (Seg n),(Seg n))),P by A107;
take P ; :: thesis:
thus for F being Function of (Seg n),(Seg n) ex Path being FinSequence of K st
( len Path = n & ( for Fj, j being Nat st j in Seg n & Fj = F . j holds
Path . j = A * j,Fj ) & P . F = (the multF of K $$ Path) * (Det (B * F)) ) :: thesis:

proof

len (A * B) = n by MATRIX_1:25;
then A122: dom (A * B) = Seg n by FINSEQ_1:def 3;
let F be Function of (Seg n),(Seg n); :: thesis:
A123: dom (idseq n) = Seg n by FUNCT_2:67;
dom F = Seg n by FUNCT_2:67;
then A124: (idseq n) +* F = F by A123, FUNCT_4:20;
A125: len B = n by MATRIX_1:25;
A126: len (B * F) = len B by Def4;
then A127: dom (B * F) = Seg n by A125, FINSEQ_1:def 3;
consider M being Matrix of n,K such that
A128: M = (A * B) +* ((B * ((idseq n) +* F)) | (Seg n)) and
A129: for j being Nat holds
( ( j in Seg n implies M . j = B . (F . j) ) & ( not j in Seg n implies M . j = (A * B) . j ) ) by A1, Th59;
(B * F) | n = B * F by A126, A125, FINSEQ_1:79;
then M = B * F by A128, A124, A127, A122, FUNCT_4:20;
hence ex Path being FinSequence of K st
( len Path = n & ( for Fj, j being Nat st j in Seg n & Fj = F . j holds
Path . j = A * j,Fj ) & P . F = (the multF of K $$ Path) * (Det (B * F)) ) by A120, A128, A129; :: thesis:

end;

thus Det (A * B) = the addF of K $$ (FinOmega (Funcs (Seg n),(Seg n))),P by A121; :: thesis: