let n be Nat; :: thesis: for K being commutative Ring
for A, B being Matrix of n,K st 0 < n holds
ex P being Function of (Permutations n), the carrier of K st
( Det (A * B) = the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),P) & ( for perm being Element of Permutations n holds P . perm = ( the multF of K $$ (Path_matrix (perm,A))) * (- ((Det B),perm)) ) )
let K be commutative Ring; :: thesis: for A, B being Matrix of n,K st 0 < n holds
ex P being Function of (Permutations n), the carrier of K st
( Det (A * B) = the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),P) & ( for perm being Element of Permutations n holds P . perm = ( the multF of K $$ (Path_matrix (perm,A))) * (- ((Det B),perm)) ) )
let A, B be Matrix of n,K; :: thesis: ( 0 < n implies ex P being Function of (Permutations n), the carrier of K st
( Det (A * B) = the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),P) & ( for perm being Element of Permutations n holds P . perm = ( the multF of K $$ (Path_matrix (perm,A))) * (- ((Det B),perm)) ) ) )
assume A1: 0 < n ; :: thesis: ex P being Function of (Permutations n), the carrier of K st
( Det (A * B) = the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),P) & ( for perm being Element of Permutations n holds P . perm = ( the multF of K $$ (Path_matrix (perm,A))) * (- ((Det B),perm)) ) )
set P = Permutations n;
A2: dom (id (Permutations n)) = Permutations n ;
set KK = the carrier of K;
set mm = the multF of K;
set aa = the addF of K;
set AB = A * B;
set X = Seg n;
set F = Funcs ((Seg n),(Seg n));
consider SUM1 being Function of (Funcs ((Seg n),(Seg n))), the carrier of K such that
A3: 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) ) & SUM1 . F = ( the multF of K $$ Path) * (Det (B * F)) ) and
A4: Det (A * B) = the addF of K $$ ((In ((Funcs ((Seg n),(Seg n))),(Fin (Funcs ((Seg n),(Seg n)))))),SUM1) by A1, Th60;
reconsider FP = (Funcs ((Seg n),(Seg n))) \ (Permutations n) as Element of Fin (Funcs ((Seg n),(Seg n))) by FINSUB_1:def 5;
A6: Permutations n c= Funcs ((Seg n),(Seg n))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Permutations n or x in Funcs ((Seg n),(Seg n)) )
assume x in Permutations n ; :: thesis: x in Funcs ((Seg n),(Seg n))
then reconsider p = x as Permutation of (Seg n) by MATRIX_1:def 12;
p is Element of Funcs ((Seg n),(Seg n)) by FUNCT_2:9;
hence x in Funcs ((Seg n),(Seg n)) ; :: thesis: verum

end;

then reconsider P9 = Permutations n as Element of Fin (Funcs ((Seg n),(Seg n))) by FINSUB_1:def 5;
Permutations n in Fin (Permutations n) by FINSUB_1:def 5;
then A7: Permutations n = In ((Permutations n),(Fin (Permutations n))) by SUBSET_1:def 8;
Funcs ((Seg n),(Seg n)) in Fin (Funcs ((Seg n),(Seg n))) by FINSUB_1:def 5;
then A8: In ((Funcs ((Seg n),(Seg n))),(Fin (Funcs ((Seg n),(Seg n))))) = Funcs ((Seg n),(Seg n)) by SUBSET_1:def 8;

A9: now :: thesis: Det (A * B) = the addF of K $$ (P9,SUM1)

per cases ( FP = {} or FP <> {} ) ;

suppose FP = {} ; :: thesis: Det (A * B) = the addF of K $$ (P9,SUM1)

then Funcs ((Seg n),(Seg n)) c= Permutations n by XBOOLE_1:37;
hence Det (A * B) = the addF of K $$ (P9,SUM1) by A4, A8, A6, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A10: FP <> {} ; :: thesis: Det (A * B) = the addF of K $$ (P9,SUM1)

A11: 0. K = the_unity_wrt the addF of K by FVSUM_1:7;
A12: SUM1 .: FP c= {(0. K)}

proof

let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in SUM1 .: FP or s in {(0. K)} )
assume s in SUM1 .: FP ; :: thesis: s in {(0. K)}
then consider x being object such that
x in dom SUM1 and
A13: x in FP and
A14: s = SUM1 . x by FUNCT_1:def 6;
reconsider f = x as Function of (Seg n),(Seg n) by A13, FUNCT_2:66;
not f in Permutations n by A13, XBOOLE_0:def 5;
then A15: Det (B * f) = 0. K by Th54;
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) ) & SUM1 . f = ( the multF of K $$ Path) * (Det (B * f)) ) by A3;
then SUM1 . f = 0. K by A15;
hence s in {(0. K)} by A14, TARSKI:def 1; :: thesis: verum

end;

dom SUM1 = Funcs ((Seg n),(Seg n)) by FUNCT_2:def 1;
then SUM1 .: FP = {(0. K)} by A10, A12, ZFMISC_1:33;
then A16: the addF of K $$ (FP,SUM1) = 0. K by A11, FVSUM_1:8, SETWOP_2:8;
A17: FP misses Permutations n by XBOOLE_1:79;
A18: FP \/ (Permutations n) = (Funcs ((Seg n),(Seg n))) \/ (Permutations n) by XBOOLE_1:39;
(Funcs ((Seg n),(Seg n))) \/ (Permutations n) = Funcs ((Seg n),(Seg n)) by A6, XBOOLE_1:12;
hence Det (A * B) = ( the addF of K $$ (P9,SUM1)) + (0. K) by A4, A8, A16, A17, A18, FVSUM_1:8, SETWOP_2:4
.= the addF of K $$ (P9,SUM1) by RLVECT_1:4 ;
:: thesis: verum

end;

end;

end;

dom SUM1 = Funcs ((Seg n),(Seg n)) by FUNCT_2:def 1;
then A19: dom (SUM1 | (Permutations n)) = Permutations n by A6, RELAT_1:62;
rng (SUM1 | (Permutations n)) c= the carrier of K by RELAT_1:def 19;
then reconsider SP = SUM1 | (Permutations n) as Function of (Permutations n), the carrier of K by A19, FUNCT_2:2;
take SP ; :: thesis: ( Det (A * B) = the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),SP) & ( for perm being Element of Permutations n holds SP . perm = ( the multF of K $$ (Path_matrix (perm,A))) * (- ((Det B),perm)) ) )
A20: rng (id (Permutations n)) = Permutations n ;
SP * (id (Permutations n)) = SP by A19, RELAT_1:52;
hence Det (A * B) = the addF of K $$ ((In ((Permutations n),(Fin (Permutations n)))),SP) by A9, A2, A20, A7, SETWOP_2:5; :: thesis: for perm being Element of Permutations n holds SP . perm = ( the multF of K $$ (Path_matrix (perm,A))) * (- ((Det B),perm))
let perm be Element of Permutations n; :: thesis: SP . perm = ( the multF of K $$ (Path_matrix (perm,A))) * (- ((Det B),perm))
reconsider Perm = perm as Permutation of (Seg n) by MATRIX_1:def 12;
SUM1 . Perm = SP . Perm by A19, FUNCT_1:47;
then consider Path being FinSequence of K such that
A21: len Path = n and
A22: for Fj, j being Nat st j in Seg n & Fj = Perm . j holds
Path . j = A * (j,Fj) and
A23: SP . Perm = ( the multF of K $$ Path) * (Det (B * Perm)) by A3;
set PM = Path_matrix (perm,A);
A24: len (Path_matrix (perm,A)) = n by MATRIX_3:def 7;

now :: thesis: for i being Nat st 1 <= i & i <= len Path holds
Path . i = (Path_matrix (perm,A)) . i

A25: Seg n = dom Perm by FUNCT_2:52;
let i be Nat; :: thesis: ( 1 <= i & i <= len Path implies Path . i = (Path_matrix (perm,A)) . i )
assume that
A26: 1 <= i and
A27: i <= len Path ; :: thesis: Path . i = (Path_matrix (perm,A)) . i
A28: i in Seg n by A21, A26, A27;
i in Seg n by A21, A26, A27;
then A29: Perm . i in rng Perm by A25, FUNCT_1:def 3;
rng Perm c= Seg n by RELAT_1:def 19;
then Perm . i in Seg n by A29;
then reconsider Pi = Perm . i as Element of NAT ;
dom (Path_matrix (perm,A)) = Seg n by A24, FINSEQ_1:def 3;
then (Path_matrix (perm,A)) . i = A * (i,Pi) by A28, MATRIX_3:def 7;
hence Path . i = (Path_matrix (perm,A)) . i by A22, A28; :: thesis: verum

end;

then Path = Path_matrix (perm,A) by A21, A24;
hence SP . perm = ( the multF of K $$ (Path_matrix (perm,A))) * (- ((Det B),perm)) by A23, Th46; :: thesis: verum