let n be Nat; :: thesis: for K being Field
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 $$ (FinOmega (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 Field; :: 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 $$ (FinOmega (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 $$ (FinOmega (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 $$ (FinOmega (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 by RELAT_1:71;
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 $$ (FinOmega (Funcs (Seg n),(Seg n))),SUM1 by A1, Th60;
A5: Funcs (Seg n),(Seg n) is finite by FRAENKEL:16;
then 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 set ; :: 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_2:def 11;
p is Element of Funcs (Seg n),(Seg n) by FUNCT_2:12;
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 A5, FINSUB_1:def 5;
A7: Permutations n = FinOmega (Permutations n) by MATRIX_2:30, MATRIX_2:def 17;
A8: FinOmega (Funcs (Seg n),(Seg n)) = Funcs (Seg n),(Seg n) by FRAENKEL:16, MATRIX_2:def 17;

A9: now

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:9;
A12: SUM1 .: FP c= {(0. K)}

proof

let s be set ; :: 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 set such that
x in dom SUM1 and
A13: x in FP and
A14: s = SUM1 . x by FUNCT_1:def 12;
reconsider f = x as Function of (Seg n),(Seg n) by A13, FUNCT_2:121;
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, VECTSP_1:36;
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:39;
then A16: the addF of K $$ FP,SUM1 = 0. K by A11, FVSUM_1:10, SETWOP_2:10;
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:10, SETWOP_2:6
.= the addF of K $$ P9,SUM1 by RLVECT_1:10 ;
:: 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:91;
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:4;
take SP ; :: thesis: ( Det (A * B) = the addF of K $$ (FinOmega (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 by RELAT_1:71;
SP * (id (Permutations n)) = SP by A19, RELAT_1:78;
hence Det (A * B) = the addF of K $$ (FinOmega (Permutations n)),SP by A9, A2, A20, A7, SETWOP_2:7; :: 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_2:def 11;
SUM1 . Perm = SP . Perm by A19, FUNCT_1:70;
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

A25: Seg n = dom Perm by FUNCT_2:67;
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 NAT by ORDINAL1:def 13;
then A29: i in Seg n by A21, A26, A27;
i in Seg n by A21, A26, A27, A28;
then A30: Perm . i in rng Perm by A25, FUNCT_1:def 5;
rng Perm c= Seg n by RELAT_1:def 19;
then Perm . i in Seg n by A30;
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 A29, MATRIX_3:def 7;
hence Path . i = (Path_matrix perm,A) . i by A22, A29; :: thesis: verum

end;

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