let n be Nat; :: thesis:
let K be commutative Ring; :: 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 $$ ((In (FUNC,(Fin FUNC))),P) ) );
A2: for k being Nat st S₂[k] holds
S₂[k + 1]

set Y = Seg n;
let k be 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:9;
A7: FUNC1 = Funcs (((Seg k) \/ {(k + 1)}),(Seg n)) by A5, FINSEQ_1:9;
then reconsider P19 = P1 as Function of FUNC19, the carrier of K ;
A8: k + 0 <= k + 1 by XREAL_1:8;
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 $$ ((In (FUNC,(Fin FUNC))),P) by A3, A4, XXREAL_0:2;
A11: not k + 1 in Seg k by FINSEQ_3:8;
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₃[ object , object ] 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 object st y in YY holds
ex f9 being object st
( f9 in SF & S₃[y,f9] )

proof

let y be object ; :: thesis:
assume y in YY ; :: thesis:
then (Seg n) \/ {y} = Seg n by ZFMISC_1:40;
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:57;
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 :: thesis:

let x be object ; :: 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:47, TARSKI:def 1;
hence h . x = q . x by A16, A18; :: thesis:

end;

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

end;

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

proof

let y be object ; :: 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 3;
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 3;
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;
(Seg n) \/ {n} = Seg n by A1, FINSEQ_1:3, ZFMISC_1:40;
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:57;
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:6;
A37: dom (P19 * QQ) = Seg n by FUNCT_2:def 1;
A38: QQ .: (dom QQ) = SF by A28, RELAT_1:113;
1 + 0 <= k + 1 by XREAL_1:7;
then A39: k + 1 in Seg n by A4;
then A40: (A * B) . (k + 1) = Line ((A * B),(k + 1)) by MATRIX_0:52;
Mh . (k + 1) = Line (Mh,(k + 1)) by A39, MATRIX_0:52;
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 ;
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_0:24;
A48: len Mh = n by MATRIX_0:24;
A49: dom (P19 * QQ) = Seg n by FUNCT_2:def 1;
A50: width Mh = n by MATRIX_0:24;
let j be Nat; :: thesis:
assume A51: j in Seg n ; :: thesis:
(Seg n) \/ {j} = Seg n by A51, ZFMISC_1:40;
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:57;
set L = Line (B,j);
set R = RLine (Mh,(k + 1),(Line (B,j)));
(Seg k) \/ {(k + 1)} = Seg (k + 1) by FINSEQ_1:9;
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_0:24;
A57: len (Line (B,j)) = width B by MATRIX_0:def 7;

A58: now :: thesis:

A59: k + 0 < k + 1 by XREAL_1:8;
let i be Nat; :: thesis:
assume that
A60: 1 <= i and
A61: i <= len Mhj ; :: thesis:
A62: i in Seg n by A56, A60, A61;

per cases ;

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

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

end;

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

A71: k + 1 in Seg (k + 1) by FINSEQ_1:4;
A72: Line (B,j) = B . j by A51, MATRIX_0:52;
A73: (RLine (Mh,(k + 1),(Line (B,j)))) . i = Line ((RLine (Mh,(k + 1),(Line (B,j)))),i) by A62, MATRIX_0:52;
A74: i = k + 1 by A70, NAT_1:9;
then Line (B,j) = Line ((RLine (Mh,(k + 1),(Line (B,j)))),i) by A57, A47, A50, A62, Th28;
hence Mhj . i = (RLine (Mh,(k + 1),(Line (B,j)))) . i by A53, A55, A74, A71, A73, A72; :: thesis:

end;

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

then not i in Seg (k + 1) by FINSEQ_1:1;
then A76: Mhj . i = (A * B) . i by A55;
A77: Line ((RLine (Mh,(k + 1),(Line (B,j)))),i) = (RLine (Mh,(k + 1),(Line (B,j)))) . i by A62, MATRIX_0:52;
A78: not i in Seg k by A75, FINSEQ_1:1;
A79: Line (Mh,i) = Mh . i by A62, MATRIX_0:52;
Line ((RLine (Mh,(k + 1),(Line (B,j)))),i) = Line (Mh,i) by A62, A75, Th28;
hence Mhj . i = (RLine (Mh,(k + 1),(Line (B,j)))) . i by A32, A77, A79, A78, A76; :: 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;
then consider Pathj being FinSequence of K such that
A80: len Pathj = k + 1 and
A81: for m, j being Nat st j in Seg (k + 1) & m = hj . j holds
Pathj . j = A * (j,m) and
A82: P1 . hj = ( the multF of K "**" Pathj) * (Det (RLine (Mh,(k + 1),(Line (B,j))))) by A6, A54, A55;
A83: Pathj . (k + 1) = A * ((k + 1),j) by A53, A81, FINSEQ_1:4;

A84: now :: thesis:

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

end;

len (Pathj | k) = k by A8, A80, FINSEQ_1:59;
then Pathj = Path ^ <*(Pathj . (k + 1))*> by A33, A80, A84, FINSEQ_1:14, FINSEQ_3:55;
then A93: the multF of K "**" Pathj = ( the multF of K "**" Path) * (A * ((k + 1),j)) by A83, FINSOP_1:4;
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, A82, A49, A93, FUNCT_1:12; :: thesis:

end;

now :: thesis:

let y be object ; :: thesis:
assume A94: y in dom (( the multF of K "**" Path) * SUM1) ; :: thesis:
reconsider j = y as Nat by A94;
SUM1 . j = (A * ((k + 1),j)) * (Det (RLine (Mh,(k + 1),(Line (B,j))))) by A43, A45, A94;
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 A94, FVSUM_1:50
.= (( the multF of K "**" Path) * (A * ((k + 1),j))) * (Det (RLine (Mh,(k + 1),(Line (B,j))))) by GROUP_1:def 3
.= (P19 * QQ) . y by A46, A45, A94 ;
:: thesis:

end;

then ( the multF of K "**" Path) * SUM1 = P19 * QQ by A37, A45, FUNCT_1:2;
then A95: ([#] ((( 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:21;

now :: thesis:

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

end;

then A102: QQ is one-to-one by FUNCT_2:19;
reconsider Y9 = Seg n as Element of Fin YY by FINSUB_1:def 5;
A103: dom QQ = Y9 by FUNCT_2:def 1;
A104: rng (id (Seg n)) = Seg n ;
(P19 * QQ) * (id (Seg n)) = P19 * QQ by A37, RELAT_1:52;
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, A104, A95, SETWOP_2:5
.= Sum (( the multF of K "**" Path) * SUM1) by FVSUM_1:8, SETWOP_2:def 2
.= ( the multF of K "**" Path) * (Sum SUM1) by FVSUM_1:73
.= P . H by A35, A42 ;
hence the addF of K $$ (SF,P19) = P . H by A102, A38, A103, SETWOP_2:6; :: thesis:

end;

the addF of K is having_a_unity by FVSUM_1:8;
then Det (A * B) = the addF of K $$ ((In (FUNC19,(Fin 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 $$ ((In (FUNC1,(Fin FUNC1))),P) ) by A6, A7; :: thesis:

end;

set FUN = Funcs ((Seg n),(Seg n));
A105: S₂[ 0 ]

proof

reconsider E = {} as Function of (Seg 0),(Seg n) by XBOOLE_1:2;
assume 0 <= n ; :: thesis:
A106: the_unity_wrt the multF of K = 1_ K by GROUP_1:22;
let FUNC be non empty set ; :: thesis:
assume A107: FUNC = Funcs ((Seg 0),(Seg n)) ; :: thesis:
consider P being Function of FUNC, the carrier of K such that
A108: S₁[P, 0 ] by A1, A107, Lm10;
A109: FUNC = {E} by A107, FUNCT_5:57;
then A110: E in FUNC by TARSKI:def 1;
FUNC is finite by A109;
then FUNC in Fin FUNC by FINSUB_1:def 5;
then In (FUNC,(Fin FUNC)) = {E} by SUBSET_1:def 8, A109;
then A111: the addF of K $$ ((In (FUNC,(Fin FUNC))),P) = P . E by A110, SETWISEO:17;
consider M being Matrix of n,K such that
A112: M = (A * B) +* ((B * ((idseq n) +* E)) | (Seg 0)) and
A113: 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;
A114: M = (A * B) +* {} by A112;
consider Path being FinSequence of K such that
A115: len Path = 0 and
for Fj, j being Nat st j in Seg 0 & Fj = E . j holds
Path . j = A * (j,Fj) and
A116: P . E = ( the multF of K $$ Path) * (Det M) by A108, A112, A113;
Path = <*> the carrier of K by A115;
then the multF of K "**" Path = 1_ K by A106, FINSOP_1:10;
then P . E = Det (A * B) by A116, A114;
hence ex P being Function of FUNC, the carrier of K st
( S₁[P, 0 ] & Det (A * B) = the addF of K $$ ((In (FUNC,(Fin FUNC))),P) ) by A108, A111; :: thesis:

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(A105, A2);
then consider P being Function of (Funcs ((Seg n),(Seg n))), the carrier of K such that
A117: S₁[P,n] and
A118: Det (A * B) = the addF of K $$ ((In ((Funcs ((Seg n),(Seg n))),(Fin (Funcs ((Seg n),(Seg n)))))),P) ;
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_0:24;
then A119: dom (A * B) = Seg n by FINSEQ_1:def 3;
let F be Function of (Seg n),(Seg n); :: thesis:
A120: dom (idseq n) = Seg n ;
dom F = Seg n by FUNCT_2:52;
then A121: (idseq n) +* F = F by A120, FUNCT_4:19;
A122: len B = n by MATRIX_0:24;
len (B * F) = len B by Def4;
then A123: dom (B * F) = Seg n by A122, FINSEQ_1:def 3;
consider M being Matrix of n,K such that
A124: M = (A * B) +* ((B * ((idseq n) +* F)) | (Seg n)) and
A125: 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;
M = B * F by A124, A121, A123, A119, FUNCT_4:19;
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 A117, A124, A125; :: thesis:

end;

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