laplace.miz

begin

 reserve x,y for object,

N for Element of NAT ,

c,i,j,k,m,n for Nat,

D for non empty set,

s for Element of ( 2Set ( Seg (n + 2))),

p for Element of ( Permutations n),

p1,q1 for Element of ( Permutations (n + 1)),

p2 for Element of ( Permutations (n + 2)),

K for Field,

a for Element of K,

f for FinSequence of K,

A for Matrix of K,

AD for Matrix of n, m, D,

pD for FinSequence of D,

M for Matrix of n, K;

 theorem :: LAPLACE:1



 Th1: for f be FinSequence, i be Nat st i in ( dom f) holds ( len ( Del (f,i))) = (( len f) -' 1)

 proof

 let f be FinSequence, i be Nat;

 assume i in ( dom f);

 then ex m be Nat st ( len f) = (m + 1) & ( len ( Del (f,i))) = m by FINSEQ_3: 104;

 hence thesis by NAT_D: 34;

 end;

 theorem :: LAPLACE:2



 Th2: for i,j,n be Nat, M be Matrix of n, K st i in ( dom M) holds ( len ( Deleting (M,i,j))) = (n -' 1)

 proof

 let i,j,n be Nat, M be Matrix of n, K;

 assume

 A1: i in ( dom M);



 A2: ( len M) = n by MATRIX_0:def 2;



 thus ( len ( Deleting (M,i,j))) = ( len ( DelLine (M,i))) by MATRIX_0:def 13

 .= (n -' 1) by A1, A2, Th1;

 end;

 theorem :: LAPLACE:3



 Th3: j in ( Seg ( width A)) implies ( width ( DelCol (A,j))) = (( width A) -' 1)

 proof

 set DC = ( DelCol (A,j));



 A1: ( len DC) = ( len A) by MATRIX_0:def 13;

 assume

 A2: j in ( Seg ( width A));

 then ( Seg ( width A)) <> {} ;

 then ( width A) <> 0 ;

 then ( len A) > 0 by MATRIX_0:def 3;

 then

 consider t be FinSequence such that

 A3: t in ( rng DC) and

 A4: ( len t) = ( width DC) by A1, MATRIX_0:def 3;

 consider k9 be object such that

 A5: k9 in ( dom ( DelCol (A,j))) and

 A6: (DC . k9) = t by A3, FUNCT_1:def 3;

 k9 in ( Seg ( len DC)) by A5, FINSEQ_1:def 3;

 then

 consider k be Nat such that

 A7: k9 = k and 1 <= k and k <= ( len DC);

 k in ( dom A) by A1, A5, A7, FINSEQ_3: 29;

 then

 A8: t = ( Del (( Line (A,k)),j)) by A6, A7, MATRIX_0:def 13;



 A9: ( len ( Line (A,k))) = ( width A) by MATRIX_0:def 7;

 then ( dom ( Line (A,k))) = ( Seg ( width A)) by FINSEQ_1:def 3;

 hence thesis by A2, A4, A9, A8, Th1;

 end;

 theorem :: LAPLACE:4



 Th4: for i be Nat st ( len A) > 1 holds ( width A) = ( width ( DelLine (A,i)))

 proof

 let i be Nat;

 assume

 A1: ( len A) > 1;

 per cases ;

 suppose i in ( dom A);

 then

 consider m be Nat such that

 A2: ( len A) = (m + 1) and

 A3: ( len ( Del (A,i))) = m by FINSEQ_3: 104;



 A4: m >= 1 by A1, A2, NAT_1: 13;

 then

 A5: m in ( dom ( Del (A,i))) by A3, FINSEQ_3: 25;

 then

 A6: (( DelLine (A,i)) . m) in ( rng ( Del (A,i))) by FUNCT_1:def 3;



 A7: ( rng ( Del (A,i))) c= ( rng A) by FINSEQ_3: 106;



 A8: (( DelLine (A,i)) . m) = ( Line (( DelLine (A,i)),m)) by A5, MATRIX_0: 60;

 A is Matrix of ( len A), ( width A), K by A1, MATRIX_0: 20;

 then ( len ( Line (( DelLine (A,i)),m))) = ( width A) by A6, A8, A7, MATRIX_0:def 2;

 hence thesis by A3, A4, A6, A8, MATRIX_0:def 3;

 end;

 suppose not i in ( dom A);

 hence thesis by FINSEQ_3: 104;

 end;

 end;

 theorem :: LAPLACE:5



 Th5: for i be Nat st j in ( Seg ( width M)) holds ( width ( Deleting (M,i,j))) = (n -' 1)

 proof

 let i be Nat;

 assume

 A1: j in ( Seg ( width M));

 per cases ;

 suppose

 A2: ( len M) <= 1 & i in ( dom M);

 ( Seg ( width M)) <> {} by A1;

 then ( width M) <> {} ;

 then ( len M) > 0 by MATRIX_0:def 3;

 then

 A3: ( len M) = 1 by A2, NAT_1: 25;



 A4: ( len ( Deleting (M,i,j))) = (n -' 1) by A2, Th2;

 ( len M) = n by MATRIX_0: 24;

 then ( len ( Deleting (M,i,j))) = 0 by A3, A4, XREAL_1: 232;

 hence thesis by A4, MATRIX_0:def 3;

 end;

 suppose

 A5: ( len M) > 1;



 A6: ( width M) = n by MATRIX_0: 24;

 ( width M) = ( width ( DelLine (M,i))) by A5, Th4;

 hence thesis by A1, A6, Th3;

 end;

 suppose

 A7: not i in ( dom M);



 A8: ( width M) = n by MATRIX_0: 24;

 ( DelLine (M,i)) = M by A7, FINSEQ_3: 104;

 hence thesis by A1, A8, Th3;

 end;

 end;

 definition

 let G be non empty multMagma;

 let B be Function of [:the carrier of G, NAT :], the carrier of G;

 let g be Element of G, i be Nat;

 :: original: .

 redefine

 func B . (g,i) -> Element of G ;

 coherence

 proof

 reconsider i as Element of NAT by ORDINAL1:def 12;

 (B . (g,i)) is Element of G;

 hence thesis;

 end;

 end

 theorem :: LAPLACE:6



 Th6: ( card ( Permutations n)) = (n ! )

 proof

 set P = ( Permutations n);

 reconsider N = n as Element of NAT by ORDINAL1:def 12;

 set X = ( finSeg N);

 set PER = { F where F be Function of X, X : F is Permutation of X };



 A1: P c= PER

 proof

 let x be object;

 assume x in P;

 then x is Permutation of X by MATRIX_1:def 12;

 hence thesis;

 end;

 PER c= P

 proof

 let x be object;

 assume x in PER;

 then ex F be Function of X, X st x = F & F is Permutation of X;

 hence thesis by MATRIX_1:def 12;

 end;

 then P = PER by A1, XBOOLE_0:def 10;



 hence ( card P) = (( card X) ! ) by CARD_FIN: 8

 .= (n ! ) by FINSEQ_1: 57;

 end;

 theorem :: LAPLACE:7



 Th7: for i, j st i in ( Seg (n + 1)) & j in ( Seg (n + 1)) holds ( card { p1 : (p1 . i) = j }) = (n ! )

 proof

 let i, j such that

 A1: i in ( Seg (n + 1)) and

 A2: j in ( Seg (n + 1));

 reconsider N = n as Element of NAT by ORDINAL1:def 12;

 set n1 = (N + 1);

 set X = ( finSeg n1);

 set Y = (X \ {j});



 A3: (Y \/ {j}) = X by A2, ZFMISC_1: 116;

 set X9 = (X \ {i});

 set P1 = ( Permutations n1);

 set F = { p where p be Element of P1 : (p . i) = j };

 set F9 = { f where f be Function of (X9 \/ {i}), (Y \/ {j}) : f is one-to-one & (f . i) = j };



 A4: (X9 \/ {i}) = X by A1, ZFMISC_1: 116;



 A5: F9 c= F

 proof

 let x be object;

 assume x in F9;

 then

 consider f be Function of X, X such that

 A6: f = x and

 A7: f is one-to-one and

 A8: (f . i) = j by A4, A3;

 ( card X) = ( card X);

 then f is onto by A7, FINSEQ_4: 63;

 then f in P1 by A7, MATRIX_1:def 12;

 hence thesis by A6, A8;

 end;

 F c= F9

 proof

 let x be object;

 assume x in F;

 then

 consider p be Element of P1 such that

 A9: x = p and

 A10: (p . i) = j;

 reconsider p as Permutation of X by MATRIX_1:def 12;

 (p . i) = j by A10;

 hence thesis by A4, A3, A9;

 end;

 then

 A11: F = F9 by A5, XBOOLE_0:def 10;



 A12: ( card X) = n1 by FINSEQ_1: 57;



 A13: not j in Y by ZFMISC_1: 56;

 then

 A14: ( card X) = (( card Y) + 1) by A3, CARD_2: 41;



 A15: not i in X9 by ZFMISC_1: 56;

 then

 A16: ( card X) = (( card X9) + 1) by A4, CARD_2: 41;

 then Y is empty implies X9 is empty by A14;



 hence ( card { p1 : (p1 . i) = j }) = ( card { f where f be Function of X9, Y : f is one-to-one }) by A15, A13, A11, CARD_FIN: 5

 .= ((( card Y) ! ) / ((( card Y) -' ( card X9)) ! )) by A16, A14, CARD_FIN: 7

 .= ((( card Y) ! ) / 1) by A16, A14, NEWTON: 12, XREAL_1: 232

 .= (n ! ) by A14, A12;

 end;

 theorem :: LAPLACE:8



 Th8: for K be Fanoian Field holds for p2 holds for X,Y be Element of ( Fin ( 2Set ( Seg (n + 2)))) st Y = { s : s in X & (( Part_sgn (p2,K)) . s) = ( - ( 1_ K)) } holds (the multF of K $$ (X,( Part_sgn (p2,K)))) = (( power K) . (( - ( 1_ K)),( card Y)))

 proof

 let K be Fanoian Field;

 let p2;

 set n2 = (n + 2);

 let X,Y be Element of ( Fin ( 2Set ( Seg n2))) such that

 A1: Y = { s : s in X & (( Part_sgn (p2,K)) . s) = ( - ( 1_ K)) };

 reconsider ID = ( id ( Seg n2)) as Element of ( Permutations n2) by MATRIX_1:def 12;

 set Y9 = { s : s in X & (( Part_sgn (p2,K)) . s) <> (( Part_sgn (ID,K)) . s) };



 A2: for x st x in X holds (( Part_sgn (ID,K)) . x) = ( 1_ K)

 proof



 A3: X c= ( 2Set ( Seg n2)) by FINSUB_1:def 5;

 let x;

 assume x in X;

 then

 consider i,j be Nat such that

 A4: i in ( Seg n2) and

 A5: j in ( Seg n2) and

 A6: i < j and

 A7: x = {i, j} by A3, MATRIX11: 1;



 A8: (ID . j) = j by A5, FUNCT_1: 17;

 (ID . i) = i by A4, FUNCT_1: 17;

 hence thesis by A4, A5, A6, A7, A8, MATRIX11:def 1;

 end;



 A9: Y9 c= Y

 proof

 let y be object;

 assume y in Y9;

 then

 consider s such that

 A10: y = s and

 A11: s in X and

 A12: (( Part_sgn (p2,K)) . s) <> (( Part_sgn (ID,K)) . s);

 (( Part_sgn (ID,K)) . s) = ( 1_ K) by A2, A11;

 then (( Part_sgn (p2,K)) . s) = ( - ( 1_ K)) by A12, MATRIX11: 5;

 hence thesis by A1, A10, A11;

 end;

 Y c= Y9

 proof

 let y be object;



 A13: ( 1_ K) <> ( - ( 1_ K)) by MATRIX11: 22;

 assume y in Y;

 then

 consider s such that

 A14: s = y and

 A15: s in X and

 A16: (( Part_sgn (p2,K)) . s) = ( - ( 1_ K)) by A1;

 (( Part_sgn (ID,K)) . s) = ( 1_ K) by A2, A15;

 hence thesis by A14, A15, A16, A13;

 end;

 then

 A17: Y = Y9 by A9, XBOOLE_0:def 10;

 per cases by NAT_D: 12;

 suppose

 A18: (( card Y) mod 2) = 0 ;

 then

 consider t be Nat such that

 A19: ( card Y) = ((2 * t) + 0 ) and 0 < 2 by NAT_D:def 2;

 t is Element of NAT by ORDINAL1:def 12;



 hence (( power K) . (( - ( 1_ K)),( card Y))) = ( 1_ K) by A19, HURWITZ: 4

 .= (the multF of K $$ (X,( Part_sgn (ID,K)))) by A2, MATRIX11: 4

 .= (the multF of K $$ (X,( Part_sgn (p2,K)))) by A17, A18, MATRIX11: 7;

 end;

 suppose

 A20: (( card Y) mod 2) = 1;

 then

 consider t be Nat such that

 A21: ( card Y) = ((2 * t) + 1) and 1 < 2 by NAT_D:def 2;

 t is Element of NAT by ORDINAL1:def 12;



 hence (( power K) . (( - ( 1_ K)),( card Y))) = ( - ( 1_ K)) by A21, HURWITZ: 4

 .= ( - (the multF of K $$ (X,( Part_sgn (ID,K))))) by A2, MATRIX11: 4

 .= (the multF of K $$ (X,( Part_sgn (p2,K)))) by A17, A20, MATRIX11: 7;

 end;

 end;

 theorem :: LAPLACE:9



 Th9: for K be Fanoian Field holds for p2, i, j st i in ( Seg (n + 2)) & (p2 . i) = j holds ex X be Element of ( Fin ( 2Set ( Seg (n + 2)))) st X = { {N, i} where N be Nat : {N, i} in ( 2Set ( Seg (n + 2))) } & (the multF of K $$ (X,( Part_sgn (p2,K)))) = (( power K) . (( - ( 1_ K)),(i + j)))

 proof

 let K be Fanoian Field;

 let p2, i, j such that

 A1: i in ( Seg (n + 2)) and

 A2: (p2 . i) = j;

 reconsider N = n as Element of NAT by ORDINAL1:def 12;

 set n2 = (N + 2);

 reconsider p29 = p2 as Permutation of ( finSeg n2) by MATRIX_1:def 12;



 A3: ( rng p29) = ( Seg n2) by FUNCT_2:def 3;

 1 <= i by A1, FINSEQ_1: 1;

 then

 reconsider i1 = (i - 1) as Element of NAT by NAT_1: 21;

 deffunc F( object) = {$1, i};

 set Ui = (( finSeg n2) \ ( Seg i));

 set Li = ( finSeg i1);

 set SS = ( 2Set ( Seg (n + 2)));

 set X = { {k, i} where k be Nat : {k, i} in ( 2Set ( Seg (n + 2))) };



 A4: X c= SS

 proof

 let x be object;

 assume x in X;

 then ex k be Nat st x = {k, i} & {k, i} in ( 2Set ( Seg n2));

 hence thesis;

 end;

 then

 reconsider X as Element of ( Fin SS) by FINSUB_1:def 5;

 set Y = { s : s in X & (( Part_sgn (p2,K)) . s) = ( - ( 1_ K)) };



 A5: Y c= X

 proof

 let x be object;

 assume x in Y;

 then ex s st s = x & s in X & (( Part_sgn (p2,K)) . s) = ( - ( 1_ K));

 hence thesis;

 end;

 then

 A6: Y c= SS by A4;

 ( dom p29) = ( Seg n2) by FUNCT_2: 52;

 then

 A7: (p2 . i) in ( rng p2) by A1, FUNCT_1:def 3;

 then 1 <= j by A2, A3, FINSEQ_1: 1;

 then

 reconsider j1 = (j - 1) as Element of NAT by NAT_1: 21;

 reconsider Y as Element of ( Fin SS) by A6, FINSUB_1:def 5;

 consider f be Function such that

 A8: ( dom f) = (Li \/ Ui) & for x be object st x in (Li \/ Ui) holds (f . x) = F(x) from FUNCT_1:sch 3;



 A9: (f " Y) c= ( dom f) by RELAT_1: 132;

 then

 reconsider fY = (f " Y) as finite set by A8;



 A10: (Li \/ Ui) c= (( Seg n2) \ {i})

 proof

 let x be object such that

 A11: x in (Li \/ Ui);

 per cases by A11, XBOOLE_0:def 3;

 suppose

 A12: x in Li;



 A13: i <= n2 by A1, FINSEQ_1: 1;

 consider k be Nat such that

 A14: x = k and

 A15: 1 <= k and

 A16: k <= i1 by A12;



 A17: i1 < (i1 + 1) by NAT_1: 13;

 then k < i by A16, XXREAL_0: 2;

 then k <= n2 by A13, XXREAL_0: 2;

 then

 A18: k in ( Seg n2) by A15;

 not k in {i} by A16, A17, TARSKI:def 1;

 hence thesis by A14, A18, XBOOLE_0:def 5;

 end;

 suppose

 A19: x in Ui;



 A20: (i1 + 1) in ( Seg i) by FINSEQ_1: 4;

 not x in ( Seg i) by A19, XBOOLE_0:def 5;

 then not x in {i} by A20, TARSKI:def 1;

 hence thesis by A19, XBOOLE_0:def 5;

 end;

 end;

 for x1,x2 be object st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2

 proof

 let x1,x2 be object such that

 A21: x1 in ( dom f) and

 A22: x2 in ( dom f) and

 A23: (f . x1) = (f . x2);



 A24: (f . x2) = F(x2) by A8, A22;

 not x1 in {i} by A10, A8, A21, XBOOLE_0:def 5;

 then

 A25: x1 <> i by TARSKI:def 1;

 (f . x1) = F(x1) by A8, A21;

 then x1 in {i, x2} by A23, A24, TARSKI:def 2;

 hence thesis by A25, TARSKI:def 2;

 end;

 then f is one-to-one by FUNCT_1:def 4;

 then ((f .: fY),fY) are_equipotent by A9, CARD_1: 33;

 then

 A26: ( card (f .: fY)) = ( card fY) by CARD_1: 5;

 (( finSeg n2) \ {i}) c= (Li \/ Ui)

 proof

 let x be object such that

 A27: x in (( finSeg n2) \ {i});

 x in ( finSeg n2) by A27;

 then

 consider k be Nat such that

 A28: x = k and

 A29: 1 <= k and

 A30: k <= n2;

 not k in {i} by A27, A28, XBOOLE_0:def 5;

 then

 A31: k <> i by TARSKI:def 1;

 per cases by A31, XXREAL_0: 1;

 suppose k < (i1 + 1);

 then k <= i1 by NAT_1: 13;

 then x in Li by A28, A29;

 hence thesis by XBOOLE_0:def 3;

 end;

 suppose k > (i1 + 1);

 then

 A32: not x in ( Seg i) by A28, FINSEQ_1: 1;

 x in ( Seg n2) by A28, A29, A30;

 then x in Ui by A32, XBOOLE_0:def 5;

 hence thesis by XBOOLE_0:def 3;

 end;

 end;

 then

 A33: (( finSeg n2) \ {i}) = (Li \/ Ui) by A10, XBOOLE_0:def 10;



 A34: ( rng f) c= X

 proof

 let x be object;

 assume x in ( rng f);

 then

 consider y be object such that

 A35: y in ( dom f) and

 A36: (f . y) = x by FUNCT_1:def 3;

 y in ( finSeg n2) by A33, A8, A35;

 then

 consider k be Nat such that

 A37: k = y and

 A38: 1 <= k and

 A39: k <= n2;



 A40: (f . k) = {i, k} by A8, A35, A37;

 not y in {i} by A10, A8, A35, XBOOLE_0:def 5;

 then i <> k by A37, TARSKI:def 1;

 then

 A41: k < i or i < k by XXREAL_0: 1;

 k in ( Seg n2) by A38, A39;

 then {i, k} in SS by A1, A41, MATRIX11: 1;

 hence thesis by A36, A37, A40;

 end;



 A42: (p29 .: ((Li \ (f " Y)) \/ (Ui /\ (f " Y)))) c= ( Seg j1)

 proof

 let y be object;

 assume y in (p29 .: ((Li \ (f " Y)) \/ (Ui /\ (f " Y))));

 then

 consider x be object such that

 A43: x in ( dom p29) and

 A44: x in ((Li \ (f " Y)) \/ (Ui /\ (f " Y))) and

 A45: (p29 . x) = y by FUNCT_1:def 6;

 ( dom p29) = ( Seg n2) by FUNCT_2: 52;

 then

 consider k be Nat such that

 A46: x = k and

 A47: 1 <= k and

 A48: k <= n2 by A43;

 per cases by A44, A46, XBOOLE_0:def 3;

 suppose

 A49: k in (Li \ (f " Y));

 then k <= i1 by FINSEQ_1: 1;

 then

 A50: k < (i1 + 1) by NAT_1: 13;



 A51: Li c= ( dom f) by A8, XBOOLE_1: 7;



 A52: k in Li by A49;

 then

 A53: (f . k) in ( rng f) by A51, FUNCT_1:def 3;

 not k in (f " Y) by A49, XBOOLE_0:def 5;

 then

 A54: not (f . k) in Y by A52, A51, FUNCT_1:def 7;



 A55: k in ( Seg n2) by A47, A48;

 ( dom p29) = ( Seg n2) by FUNCT_2: 52;

 then

 A56: (p2 . i) <> (p2 . k) by A1, A50, A55, FUNCT_1:def 4;



 A57: (f . k) = F(k) by A8, A52, A51;

 then F(k) in X by A34, A53;

 then ex m be Nat st F(k) = {m, i} & {m, i} in SS;

 then (( Part_sgn (p2,K)) . {k, i}) <> ( - ( 1_ K)) by A34, A54, A53, A57;

 then (p2 . k) <= (p2 . i) by A1, A50, A55, MATRIX11:def 1;

 then (p2 . k) < (j1 + 1) by A2, A56, XXREAL_0: 1;

 then

 A58: (p2 . k) <= j1 by NAT_1: 13;



 A59: ( rng p29) = ( Seg n2) by FUNCT_2:def 3;

 (p2 . k) in ( rng p29) by A43, A46, FUNCT_1:def 3;

 then 1 <= (p2 . k) by A59, FINSEQ_1: 1;

 hence thesis by A45, A46, A58;

 end;

 suppose

 A60: k in (Ui /\ (f " Y));

 then k in Ui by XBOOLE_0:def 4;

 then

 A61: not k in ( Seg i) by XBOOLE_0:def 5;

 1 <= k by A60, FINSEQ_1: 1;

 then

 A62: i < k by A61;



 A63: k in (f " Y) by A60, XBOOLE_0:def 4;

 then (f . k) in Y by FUNCT_1:def 7;

 then

 consider s such that

 A64: s = (f . k) and s in X and

 A65: (( Part_sgn (p2,K)) . s) = ( - ( 1_ K));

 k in ( dom f) by A63, FUNCT_1:def 7;

 then

 A66: s = {i, k} by A8, A64;

 ( dom p29) = ( finSeg n2) by FUNCT_2: 52;

 then

 A67: (p29 . i) <> (p2 . k) by A1, A60, A62, FUNCT_1:def 4;

 reconsider i, k as Element of NAT by ORDINAL1:def 12;

 ( 1_ K) <> ( - ( 1_ K)) by MATRIX11: 22;

 then (p2 . i) >= (p2 . k) by A1, A60, A65, A66, A62, MATRIX11:def 1;

 then (p2 . k) < (j1 + 1) by A2, A67, XXREAL_0: 1;

 then

 A68: (p2 . k) <= j1 by NAT_1: 13;



 A69: ( rng p29) = ( Seg n2) by FUNCT_2:def 3;

 (p2 . k) in ( rng p29) by A43, A46, FUNCT_1:def 3;

 then 1 <= (p2 . k) by A69, FINSEQ_1: 1;

 hence thesis by A45, A46, A68;

 end;

 end;

 take X;

 reconsider I = i, J = j as Element of NAT by ORDINAL1:def 12;

 set P = ( power K);

 thus X = { {e, i} where e be Nat : {e, i} in ( 2Set ( Seg (n + 2))) };



 A70: (Li /\ (f " Y)) c= Li by XBOOLE_1: 17;

 ( Seg j1) c= (p29 .: ((Li \ (f " Y)) \/ (Ui /\ (f " Y))))

 proof

 let y be object such that

 A71: y in ( Seg j1);

 consider k be Nat such that

 A72: y = k and 1 <= k and

 A73: k <= j1 by A71;



 A74: j1 < (j1 + 1) by NAT_1: 13;

 then

 A75: k < j by A73, XXREAL_0: 2;

 j <= n2 by A2, A7, A3, FINSEQ_1: 1;

 then j1 <= n2 by A74, XXREAL_0: 2;

 then ( Seg j1) c= ( Seg n2) by FINSEQ_1: 5;

 then

 consider x be object such that

 A76: x in ( dom p29) and

 A77: y = (p29 . x) by A3, A71, FUNCT_1:def 3;



 A78: not x in {i} by A2, A72, A73, A74, A77, TARSKI:def 1;

 then

 A79: x in ( dom f) by A33, A8, A76, XBOOLE_0:def 5;

 then

 A80: (f . x) = F(x) by A8;



 A81: (f . x) in ( rng f) by A79, FUNCT_1:def 3;

 then F(x) in X by A34, A80;

 then

 consider m be Nat such that

 A82: F(x) = {m, i} and

 A83: {m, i} in ( 2Set ( Seg n2));



 A84: m <> i by A83, SGRAPH1: 10;



 A85: m in ( Seg n2) by A83, SGRAPH1: 10;

 m in {x, i} by A82, TARSKI:def 2;

 then

 A86: m = x by A84, TARSKI:def 2;

 reconsider m, i as Element of NAT by ORDINAL1:def 12;

 per cases by A83, SGRAPH1: 10, XXREAL_0: 1;

 suppose

 A87: m < i;



 A88: not m in (f " Y)

 proof

 assume m in (f " Y);

 then {m, i} in Y by A80, A86, FUNCT_1:def 7;

 then

 A89: ex s st s = {m, i} & s in X & (( Part_sgn (p2,K)) . s) = ( - ( 1_ K));

 (( Part_sgn (p2,K)) . {m, i}) = ( 1_ K) by A1, A2, A72, A75, A76, A77, A86, A87, MATRIX11:def 1;

 hence thesis by A89, MATRIX11: 22;

 end;

 m < (i1 + 1) by A87;

 then

 A90: m <= i1 by NAT_1: 13;

 1 <= m by A85, FINSEQ_1: 1;

 then m in Li by A90;

 then x in (Li \ (f " Y)) by A86, A88, XBOOLE_0:def 5;

 then x in ((Li \ (f " Y)) \/ (Ui /\ (f " Y))) by XBOOLE_0:def 3;

 hence thesis by A76, A77, FUNCT_1:def 6;

 end;

 suppose

 A91: m > i;

 then not m in ( Seg i) by FINSEQ_1: 1;

 then

 A92: x in Ui by A86, A85, XBOOLE_0:def 5;

 (( Part_sgn (p2,K)) . {m, i}) = ( - ( 1_ K)) by A1, A2, A72, A75, A76, A77, A86, A91, MATRIX11:def 1;

 then

 A93: (f . x) in Y by A34, A80, A81, A82, A83;

 x in ( dom f) by A33, A8, A76, A78, XBOOLE_0:def 5;

 then x in (f " Y) by A93, FUNCT_1:def 7;

 then x in (Ui /\ (f " Y)) by A92, XBOOLE_0:def 4;

 then x in ((Li \ (f " Y)) \/ (Ui /\ (f " Y))) by XBOOLE_0:def 3;

 hence thesis by A76, A77, FUNCT_1:def 6;

 end;

 end;

 then

 A94: ( Seg j1) = (p29 .: ((Li \ (f " Y)) \/ (Ui /\ (f " Y)))) by A42, XBOOLE_0:def 10;



 A95: ( Seg n2) = ( dom p29) by FUNCT_2: 52;



 A96: (Li \ (f " Y)) = (Li \ ((f " Y) /\ Li)) by XBOOLE_1: 47;

 i1 < (i1 + 1) by NAT_1: 13;

 then Li c= ( Seg i) by FINSEQ_1: 5;

 then

 A97: Li misses Ui by XBOOLE_1: 64, XBOOLE_1: 79;

 X c= ( rng f)

 proof

 let x be object;

 assume x in X;

 then

 consider k be Nat such that

 A98: x = {k, i} and

 A99: {k, i} in SS;

 k <> i by A99, SGRAPH1: 10;

 then

 A100: not k in {i} by TARSKI:def 1;

 k in ( Seg n2) by A99, SGRAPH1: 10;

 then

 A101: k in (Li \/ Ui) by A33, A100, XBOOLE_0:def 5;

 then (f . k) = F(k) by A8;

 hence thesis by A8, A98, A101, FUNCT_1:def 3;

 end;

 then X = ( rng f) by A34, XBOOLE_0:def 10;

 then

 A102: (f .: fY) = Y by A5, FUNCT_1: 77;

 ((Li /\ (f " Y)) \/ (Ui /\ (f " Y))) = (( dom f) /\ (f " Y)) by A8, XBOOLE_1: 23;

 then

 A103: ((Li /\ (f " Y)) \/ (Ui /\ (f " Y))) = (f " Y) by RELAT_1: 132, XBOOLE_1: 28;



 A104: (Ui /\ (f " Y)) c= Ui by XBOOLE_1: 17;

 then ((Li \ (f " Y)) \/ (Ui /\ (f " Y))) c= (( finSeg n2) \ {i}) by A33, XBOOLE_1: 13;

 then (( finSeg j1),((Li \ (f " Y)) \/ (Ui /\ (f " Y)))) are_equipotent by A95, A94, CARD_1: 33, XBOOLE_1: 1;



 then

 A105: ( card ( finSeg j1)) = ( card ((Li \ (f " Y)) \/ (Ui /\ (f " Y)))) by CARD_1: 5

 .= (( card (Li \ ((f " Y) /\ Li))) + ( card (Ui /\ (f " Y)))) by A97, A104, A96, CARD_2: 40, XBOOLE_1: 64

 .= ((( card Li) - ( card ((f " Y) /\ Li))) + ( card (Ui /\ (f " Y)))) by CARD_2: 44, XBOOLE_1: 17;

 per cases ;

 suppose j > i;

 then

 reconsider ji = (j - i) as Element of NAT by NAT_1: 21;

 ( card Y) = (((( card (Li /\ fY)) + ( card ( finSeg j1))) - ( card Li)) + ( card (fY /\ Li))) by A97, A70, A104, A103, A26, A102, A105, CARD_2: 40, XBOOLE_1: 64

 .= (((2 * ( card (Li /\ fY))) + ( card ( finSeg j1))) - ( card Li))

 .= (((2 * ( card (Li /\ fY))) + j1) - ( card Li)) by FINSEQ_1: 57

 .= (((2 * ( card (Li /\ fY))) + j1) - i1) by FINSEQ_1: 57

 .= ((2 * ( card (Li /\ fY))) + ji);



 hence (the multF of K $$ (X,( Part_sgn (p2,K)))) = (P . (( - ( 1_ K)),((2 * ( card (Li /\ fY))) + ji))) by Th8

 .= ((P . (( - ( 1_ K)),(2 * ( card (Li /\ fY))))) * (P . (( - ( 1_ K)),ji))) by HURWITZ: 3

 .= (( 1_ K) * (P . (( - ( 1_ K)),ji))) by HURWITZ: 4

 .= ((P . (( - ( 1_ K)),(2 * I))) * (P . (( - ( 1_ K)),ji))) by HURWITZ: 4

 .= (P . (( - ( 1_ K)),((2 * i) + ji))) by HURWITZ: 3

 .= (P . (( - ( 1_ K)),(i + j)));

 end;

 suppose j <= i;

 then

 reconsider ij = (i - j) as Element of NAT by NAT_1: 21;

 ( card Y) = (((( card Li) + ( card (Ui /\ fY))) - ( card ( finSeg j1))) + ( card (Ui /\ fY))) by A97, A70, A104, A103, A26, A102, A105, CARD_2: 40, XBOOLE_1: 64

 .= (((2 * ( card (Ui /\ fY))) - ( card ( finSeg j1))) + ( card Li))

 .= (((2 * ( card (Ui /\ fY))) - j1) + ( card Li)) by FINSEQ_1: 57

 .= (((2 * ( card (Ui /\ fY))) - j1) + i1) by FINSEQ_1: 57

 .= ((2 * ( card (Ui /\ fY))) + ij);



 hence (the multF of K $$ (X,( Part_sgn (p2,K)))) = (P . (( - ( 1_ K)),((2 * ( card (Ui /\ fY))) + ij))) by Th8

 .= ((P . (( - ( 1_ K)),(2 * ( card (Ui /\ fY))))) * (P . (( - ( 1_ K)),ij))) by HURWITZ: 3

 .= (( 1_ K) * (P . (( - ( 1_ K)),ij))) by HURWITZ: 4

 .= ((P . (( - ( 1_ K)),(2 * J))) * (P . (( - ( 1_ K)),ij))) by HURWITZ: 4

 .= (P . (( - ( 1_ K)),((2 * j) + ij))) by HURWITZ: 3

 .= (P . (( - ( 1_ K)),(i + j)));

 end;

 end;

 theorem :: LAPLACE:10



 Th10: for i, j st i in ( Seg (n + 1)) & n >= 2 holds ex Proj be Function of ( 2Set ( Seg n)), ( 2Set ( Seg (n + 1))) st ( rng Proj) = (( 2Set ( Seg (n + 1))) \ { {N, i} where N be Nat : {N, i} in ( 2Set ( Seg (n + 1))) }) & Proj is one-to-one & for k, m st k < m & {k, m} in ( 2Set ( Seg n)) holds (m = i & k = i & k >= i implies (Proj . {k, m}) = {(k + 1), (m + 1)})

 proof

 let i,j be Nat such that

 A1: i in ( Seg (n + 1)) and

 A2: n >= 2;

 defpred P[ object, object] means for k,m be Nat st {k, m} = $1 & k < m holds (m = i & k = i & k >= i implies $2 = {(k + 1), (m + 1)});

 set X = { {N, i} where N be Nat : {N, i} in ( 2Set ( Seg (n + 1))) };

 set SS = ( 2Set ( Seg n));

 set n1 = (n + 1);

 set SS1 = ( 2Set ( Seg n1));



 A3: for k,m be Nat st {k, m} in X holds k = i or m = i

 proof

 let k,m be Nat;

 assume {k, m} in X;

 then

 consider m1 be Nat such that

 A4: {k, m} = {m1, i} and {m1, i} in SS1;

 i in {i, m1} by TARSKI:def 2;

 hence thesis by A4, TARSKI:def 2;

 end;



 A5: for x be object st x in SS holds ex y be object st y in (SS1 \ X) & P[x, y]

 proof

 n <= (n + 1) by NAT_1: 11;

 then

 A6: ( Seg n) c= ( Seg n1) by FINSEQ_1: 5;

 reconsider N = n as Element of NAT by ORDINAL1:def 12;

 let x be object;

 assume x in SS;

 then

 consider k,m be Nat such that

 A7: k in ( Seg n) and

 A8: m in ( Seg n) and

 A9: k < m and

 A10: x = {k, m} by MATRIX11: 1;



 A11: (m + 1) in ( Seg (N + 1)) by A8, FINSEQ_1: 60;

 reconsider e = k as Element of NAT by ORDINAL1:def 12;



 A12: (e + 1) in ( Seg (N + 1)) by A7, FINSEQ_1: 60;

 per cases ;

 suppose

 A13: m < i & k < i;

 then

 A14: not {k, m} in X by A3;

 {k, m} in SS1 by A7, A8, A9, A6, MATRIX11: 1;

 then

 A15: {k, m} in (SS1 \ X) by A14, XBOOLE_0:def 5;

 P[ {k, m}, {k, m}] by A13, ZFMISC_1: 6;

 hence thesis by A10, A15;

 end;

 suppose

 A16: m >= i & k < i;



 A17: P[ {k, m}, {k, (m + 1)}]

 proof

 let k9,m9 be Nat such that

 A18: {k9, m9} = {k, m} and k9 < m9;

 k9 = k or k9 = m by A18, ZFMISC_1: 6;

 hence thesis by A16, A18, ZFMISC_1: 6;

 end;

 (m + 1) > i by A16, NAT_1: 13;

 then

 A19: not {k, (m + 1)} in X by A3, A16;

 (m + 1) > k by A9, NAT_1: 13;

 then {k, (m + 1)} in SS1 by A7, A6, A11, MATRIX11: 1;

 then {k, (m + 1)} in (SS1 \ X) by A19, XBOOLE_0:def 5;

 hence thesis by A10, A17;

 end;

 suppose m = i;

 hence thesis by A9, XXREAL_0: 2;

 end;

 suppose

 A20: m >= i & k >= i;



 A21: P[ {k, m}, {(k + 1), (m + 1)}]

 proof

 let k9,m9 be Nat such that

 A22: {k9, m9} = {k, m} and

 A23: k9 < m9;

 k9 = k or k9 = m by A22, ZFMISC_1: 6;

 hence thesis by A20, A22, A23, ZFMISC_1: 6;

 end;



 A24: (k + 1) > i by A20, NAT_1: 13;

 (m + 1) > (k + 1) by A9, XREAL_1: 8;

 then

 A25: {(k + 1), (m + 1)} in SS1 by A11, A12, MATRIX11: 1;

 (m + 1) > i by A20, NAT_1: 13;

 then not {(k + 1), (m + 1)} in X by A3, A24;

 then {(k + 1), (m + 1)} in (SS1 \ X) by A25, XBOOLE_0:def 5;

 hence thesis by A10, A21;

 end;

 end;

 consider f be Function of SS, (SS1 \ X) such that

 A26: for x be object st x in SS holds P[x, (f . x)] from FUNCT_2:sch 1( A5);

 ex y be object st y in (SS1 \ X) & P[ {1, 2}, y] by A2, A5, MATRIX11: 3;

 then

 reconsider SSX = (SS1 \ X) as non empty set;

 reconsider f as Function of SS, SSX;



 A27: SSX c= ( rng f)

 proof

 let x be object such that

 A28: x in SSX;

 consider k,m be Nat such that

 A29: k in ( Seg n1) and

 A30: m in ( Seg n1) and

 A31: k < m and

 A32: x = {k, m} by A28, MATRIX11: 1;



 A33: k <> i & m <> i

 proof

 assume k = i or m = i;

 then x in X by A28, A32;

 hence thesis by A28, XBOOLE_0:def 5;

 end;



 A34: 1 <= m by A30, FINSEQ_1: 1;

 1 <= k by A29, FINSEQ_1: 1;

 then

 reconsider k1 = (k - 1), m1 = (m - 1) as Element of NAT by A34, NAT_1: 21;

 reconsider m9 = m, k9 = k as Element of NAT by ORDINAL1:def 12;

 per cases by A33, XXREAL_0: 1;

 suppose

 A35: k < i & m < i;



 A36: i <= (n + 1) by A1, FINSEQ_1: 1;

 then k < (n + 1) by A35, XXREAL_0: 2;

 then

 A37: k <= n by NAT_1: 13;

 m < (n + 1) by A35, A36, XXREAL_0: 2;

 then

 A38: m <= n by NAT_1: 13;

 1 <= m by A30, FINSEQ_1: 1;

 then

 A39: m in ( Seg n) by A38;



 A40: ( dom f) = SS by FUNCT_2:def 1;

 1 <= k by A29, FINSEQ_1: 1;

 then k in ( Seg n) by A37;

 then

 A41: {k9, m9} in SS by A31, A39, MATRIX11: 1;

 then x = (f . x) by A26, A31, A32, A35;

 hence thesis by A32, A41, A40, FUNCT_1:def 3;

 end;

 suppose k > i & m < i;

 hence thesis by A31, XXREAL_0: 2;

 end;

 suppose

 A42: k i;

 1 <= i by A1, FINSEQ_1: 1;

 then

 A43: 1 < (m1 + 1) by A42, XXREAL_0: 2;

 then

 A44: i <= m1 by A42, NAT_1: 13;

 then

 A45: k < m1 by A42, XXREAL_0: 2;

 i <= (n + 1) by A1, FINSEQ_1: 1;

 then k < (n + 1) by A42, XXREAL_0: 2;

 then

 A46: k <= n by NAT_1: 13;



 A47: ( dom f) = SS by FUNCT_2:def 1;

 (m1 + 1) <= (n + 1) by A30, FINSEQ_1: 1;

 then m1 < (n + 1) by NAT_1: 13;

 then

 A48: m1 <= n by NAT_1: 13;

 1 <= m1 by A43, NAT_1: 13;

 then

 A49: m1 in ( Seg n) by A48;

 1 <= k by A29, FINSEQ_1: 1;

 then k in ( Seg n) by A46;

 then

 A50: {k9, m1} in SS by A49, A45, MATRIX11: 1;

 then (f . {k9, m1}) = {k9, (m1 + 1)} by A26, A42, A44, A45;

 hence thesis by A32, A50, A47, FUNCT_1:def 3;

 end;

 suppose

 A51: k > i & m > i;

 (k1 + 1) <= (n + 1) by A29, FINSEQ_1: 1;

 then k1 < (n + 1) by NAT_1: 13;

 then

 A52: k1 <= n by NAT_1: 13;



 A53: ( dom f) = SS by FUNCT_2:def 1;

 (m1 + 1) <= (n + 1) by A30, FINSEQ_1: 1;

 then m1 < (n + 1) by NAT_1: 13;

 then

 A54: m1 <= n by NAT_1: 13;



 A55: k1 < m1 by A31, XREAL_1: 9;



 A56: 1 <= i by A1, FINSEQ_1: 1;

 then

 A57: 1 < (m1 + 1) by A51, XXREAL_0: 2;



 A58: 1 < (k1 + 1) by A51, A56, XXREAL_0: 2;

 then

 A59: i <= k1 by A51, NAT_1: 13;

 1 <= k1 by A58, NAT_1: 13;

 then

 A60: k1 in ( Seg n) by A52;

 1 <= m1 by A57, NAT_1: 13;

 then m1 in ( Seg n) by A54;

 then

 A61: {k1, m1} in SS by A60, A55, MATRIX11: 1;

 i <= m1 by A51, A57, NAT_1: 13;

 then (f . {k1, m1}) = {(k1 + 1), (m1 + 1)} by A26, A59, A55, A61;

 hence thesis by A32, A61, A53, FUNCT_1:def 3;

 end;

 end;



 A62: ( rng f) c= SSX by RELAT_1:def 19;

 then

 A63: SSX = ( rng f) by A27, XBOOLE_0:def 10;

 ( dom f) = SS by FUNCT_2:def 1;

 then

 reconsider f as Function of SS, SS1 by A63, FUNCT_2: 2;

 take f;

 for x1,x2 be object st x1 in SS & x2 in SS & (f . x1) = (f . x2) holds x1 = x2

 proof

 let x1,x2 be object such that

 A64: x1 in SS and

 A65: x2 in SS and

 A66: (f . x1) = (f . x2);

 consider k2,m2 be Nat such that k2 in ( Seg n) and m2 in ( Seg n) and

 A67: k2 < m2 and

 A68: x2 = {k2, m2} by A65, MATRIX11: 1;

 consider k1,m1 be Nat such that k1 in ( Seg n) and m1 in ( Seg n) and

 A69: k1 < m1 and

 A70: x1 = {k1, m1} by A64, MATRIX11: 1;

 reconsider m1, m2, k1, k2 as Element of NAT by ORDINAL1:def 12;

 per cases ;

 suppose

 A71: k1 < i & m1 < i & k2 < i & m2 < i;

 then (f . x1) = x1 by A26, A64, A69, A70;

 hence thesis by A26, A65, A66, A67, A68, A71;

 end;

 suppose

 A72: k1 = i) & m2 >= i;

 then

 A73: (f . x2) = {k2, (m2 + 1)} or (f . x2) = {(k2 + 1), (m2 + 1)} by A26, A65, A67, A68;

 (f . x1) = {k1, m1} by A26, A64, A69, A70, A72;

 then (k1 = k2 or k1 = (m2 + 1)) & (m1 = k2 or m1 = (m2 + 1)) or (k1 = (k2 + 1) or k1 = (m2 + 1)) & (m1 = (k2 + 1) or m1 = (m2 + 1)) by A66, A73, ZFMISC_1: 6;

 hence thesis by A69, A72, NAT_1: 13;

 end;

 suppose

 A74: k1 = i & k2 = i;

 then

 A75: (f . x2) = {k2, (m2 + 1)} by A26, A65, A67, A68;



 A76: (f . x1) = {k1, (m1 + 1)} by A26, A64, A69, A70, A74;

 then

 A77: (m1 + 1) = k2 or (m1 + 1) = (m2 + 1) by A66, A75, ZFMISC_1: 6;

 k1 = k2 or k1 = (m2 + 1) by A66, A76, A75, ZFMISC_1: 6;

 hence thesis by A70, A68, A74, A77, NAT_1: 13;

 end;

 suppose

 A78: k1 = i & (k2 >= i & m2 >= i or k2 < i & m2 < i);

 then

 A79: (f . x2) = {(k2 + 1), (m2 + 1)} or (f . x2) = {k2, m2} by A26, A65, A67, A68;

 (f . x1) = {k1, (m1 + 1)} by A26, A64, A69, A70, A78;

 then (k1 = (k2 + 1) or k1 = (m2 + 1)) & ((m1 + 1) = (k2 + 1) or (m1 + 1) = (m2 + 1)) or (k1 = k2 or k1 = m2) & ((m1 + 1) = k2 or (m1 + 1) = m2) by A66, A79, ZFMISC_1: 6;

 hence thesis by A78, NAT_1: 13;

 end;

 suppose k1 >= i & m1 = i & m2 < i;

 hence thesis by A69, A67, XXREAL_0: 2;

 end;

 suppose

 A80: k1 >= i & m1 >= i & k2 >= i & m2 >= i;

 then

 A81: (f . x2) = {(k2 + 1), (m2 + 1)} by A26, A65, A67, A68;



 A82: (f . x1) = {(k1 + 1), (m1 + 1)} by A26, A64, A69, A70, A80;

 then

 A83: (m1 + 1) = (k2 + 1) or (m1 + 1) = (m2 + 1) by A66, A81, ZFMISC_1: 6;

 (k1 + 1) = (k2 + 1) or (k1 + 1) = (m2 + 1) by A66, A82, A81, ZFMISC_1: 6;

 hence thesis by A69, A70, A68, A83;

 end;

 suppose

 A84: k1 >= i & m1 >= i & (k2 = i);

 then

 A85: (f . x2) = {k2, m2} or (f . x2) = {k2, (m2 + 1)} by A26, A65, A67, A68;

 (f . x1) = {(k1 + 1), (m1 + 1)} by A26, A64, A69, A70, A84;

 then ((k1 + 1) = k2 or (k1 + 1) = m2) & ((m1 + 1) = k2 or (m1 + 1) = m2) or ((k1 + 1) = k2 or (k1 + 1) = (m2 + 1)) & ((m1 + 1) = k2 or (m1 + 1) = (m2 + 1)) by A66, A85, ZFMISC_1: 6;

 hence thesis by A69, A84, NAT_1: 13;

 end;

 end;

 hence thesis by A26, A27, A62, FUNCT_2: 19, XBOOLE_0:def 10;

 end;

 theorem :: LAPLACE:11



 Th11: n < 2 implies for p be Element of ( Permutations n) holds p is even & p = ( idseq n)

 proof

 assume

 A1: n < 2;

 let p be Element of ( Permutations n);

 reconsider P = p as Permutation of ( Seg n) by MATRIX_1:def 12;

 now

 per cases by A1, NAT_1: 23;

 suppose

 A2: n = 0 ;

 then

 A3: ( Seg n) = {} ;



 A4: ( len ( Permutations n)) = n by MATRIX_1: 9;

 P = {} by A2;

 hence thesis by A4, A3, MATRIX_1: 16, RELAT_1: 55;

 end;

 suppose

 A5: n = 1;



 A6: ( len ( Permutations n)) = n by MATRIX_1: 9;

 P = ( id ( Seg n)) by A5, MATRIX_1: 10, TARSKI:def 1;

 hence thesis by A6, MATRIX_1: 16;

 end;

 end;

 hence thesis;

 end;

 theorem :: LAPLACE:12



 Th12: for X,Y,D be non empty set holds for f be Function of X, ( Fin Y), g be Function of ( Fin Y), D, F be BinOp of D st (for A,B be Element of ( Fin Y) st A misses B holds (F . ((g . A),(g . B))) = (g . (A \/ B))) & F is commutative associative & F is having_a_unity & (g . {} ) = ( the_unity_wrt F) holds for I be Element of ( Fin X) st for x, y st x in I & y in I & (f . x) meets (f . y) holds x = y holds (F $$ (I,(g * f))) = (F $$ ((f .: I),g)) & (F $$ ((f .: I),g)) = (g . ( union (f .: I))) & ( union (f .: I)) is Element of ( Fin Y)

 proof

 let X,Y,D be non empty set;

 let f be Function of X, ( Fin Y), g be Function of ( Fin Y), D, F be BinOp of D such that

 A1: for A,B be Element of ( Fin Y) st A misses B holds (F . ((g . A),(g . B))) = (g . (A \/ B)) and

 A2: F is commutative associative and

 A3: F is having_a_unity and

 A4: (g . {} ) = ( the_unity_wrt F);

 defpred P[ set] means for I be Element of ( Fin X) st I = $1 & for x, y st x in I & y in I & (f . x) meets (f . y) holds x = y holds (F $$ (I,(g * f))) = (F $$ ((f .: I),g)) & (F $$ ((f .: I),g)) = (g . ( union (f .: I))) & ( union (f .: I)) is Element of ( Fin Y);



 A5: for I be Element of ( Fin X), i be Element of X holds P[I] & not i in I implies P[(I \/ {i})]

 proof

 let A be Element of ( Fin X), a be Element of X such that

 A6: P[A] and

 A7: not a in A;

 let I be Element of ( Fin X) such that

 A8: (A \/ {a}) = I and

 A9: for x, y st x in I & y in I & (f . x) meets (f . y) holds x = y;



 A10: for x, y st x in A & y in A & (f . x) meets (f . y) holds x = y

 proof

 let x, y such that

 A11: x in A and

 A12: y in A and

 A13: (f . x) meets (f . y);

 A c= I by A8, XBOOLE_1: 7;

 hence thesis by A9, A11, A12, A13;

 end;

 then

 A14: (F $$ (A,(g * f))) = (F $$ ((f .: A),g)) by A6;



 A15: ( union (f .: A)) is Element of ( Fin Y) by A6, A10;

 ( dom f) = X by FUNCT_2:def 1;

 then ( Im (f,a)) = {(f . a)} by FUNCT_1: 59;

 then

 A16: (f .: I) = ((f .: A) \/ {(f . a)}) by A8, RELAT_1: 120;



 A17: (F $$ ((f .: A),g)) = (g . ( union (f .: A))) by A6, A10;

 ( dom (g * f)) = X by FUNCT_2:def 1;

 then

 A18: (g . (f . a)) = ((g * f) . a) by FUNCT_1: 12;

 per cases ;

 suppose

 A19: (f . a) is non empty or not (f . a) in (f .: A);

 not (f . a) in (f .: A)

 proof



 A20: A c= I by A8, XBOOLE_1: 7;



 A21: {a} c= I by A8, XBOOLE_1: 7;



 A22: a in {a} by TARSKI:def 1;

 assume

 A23: (f . a) in (f .: A);

 then

 consider x be object such that x in ( dom f) and

 A24: x in A and

 A25: (f . x) = (f . a) by FUNCT_1:def 6;

 (f . x) meets (f . a) by A19, A23, A25, XBOOLE_1: 66;

 hence thesis by A7, A9, A24, A22, A21, A20;

 end;

 then

 A26: (F $$ ((f .: I),g)) = (F . ((F $$ ((f .: A),g)),((g * f) . a))) by A2, A3, A16, A18, SETWOP_2: 2;



 A27: (f . a) c= Y by FINSUB_1:def 5;

 ( union (f .: A)) c= Y by A15, FINSUB_1:def 5;

 then

 A28: (( union (f .: A)) \/ (f . a)) c= Y by A27, XBOOLE_1: 8;

 now

 let x be set;

 assume x in (f .: A);

 then

 A29: ex y be object st y in ( dom f) & y in A & (f . y) = x by FUNCT_1:def 6;



 A30: a in {a} by TARSKI:def 1;



 A31: A c= I by A8, XBOOLE_1: 7;



 A32: {a} c= I by A8, XBOOLE_1: 7;

 assume x meets (f . a);

 hence contradiction by A7, A9, A29, A30, A32, A31;

 end;

 then

 A33: ( union (f .: A)) misses (f . a) by ZFMISC_1: 80;

 ( union (f .: I)) = (( union (f .: A)) \/ ( union {(f . a)})) by A16, ZFMISC_1: 78

 .= (( union (f .: A)) \/ (f . a)) by ZFMISC_1: 25;

 hence thesis by A1, A2, A3, A7, A8, A14, A17, A15, A18, A26, A28, A33, FINSUB_1:def 5, SETWOP_2: 2;

 end;

 suppose

 A34: (f . a) is empty & (f . a) in (f .: A);

 then

 A35: ((f .: A) \/ {(f . a)}) = (f .: A) by ZFMISC_1: 40;

 (F $$ (I,(g * f))) = (F . ((F $$ ((f .: A),g)),( the_unity_wrt F))) by A2, A3, A4, A7, A8, A14, A18, A34, SETWOP_2: 2

 .= (F $$ ((f .: I),g)) by A3, A16, A35, SETWISEO: 15;

 hence thesis by A6, A10, A16, A35;

 end;

 end;



 A36: P[( {}. X)]

 proof



 A37: {} c= Y;

 let I be Element of ( Fin X) such that

 A38: ( {}. X) = I and for x, y st x in I & y in I & (f . x) meets (f . y) holds x = y;



 A39: (f .: I) = ( {}. ( Fin Y)) by A38;

 (F $$ (I,(g * f))) = (g . {} ) by A2, A3, A4, A38, SETWISEO: 31;

 hence thesis by A2, A3, A4, A39, A37, FINSUB_1:def 5, SETWISEO: 31, ZFMISC_1: 2;

 end;

 for I be Element of ( Fin X) holds P[I] from SETWISEO:sch 2( A36, A5);

 hence thesis;

 end;

 begin

 definition

 let i,j,n be Nat;

 let K;

 let M be Matrix of n, K;

 assume that

 A1: i in ( Seg n) and

 A2: j in ( Seg n);

 :: LAPLACE:def1

 func Delete (M,i,j) -> Matrix of (n -' 1), K equals

 : Def1: ( Deleting (M,i,j));

 coherence

 proof

 set D = ( Deleting (M,i,j));



 A3: ( width M) = n by MATRIX_0: 24;

 ( len M) = n by MATRIX_0: 24;

 then ( dom M) = ( Seg n) by FINSEQ_1:def 3;

 then

 A4: ( len D) = (n -' 1) by A1, Th2;

 per cases ;

 suppose (n -' 1) = 0 ;

 then ( dom D) = ( Seg 0 ) by A4, FINSEQ_1:def 3;

 then for f st f in ( rng D) holds ( len f) = (n -' 1) by RELAT_1: 42;

 hence thesis by A4, MATRIX_0:def 2;

 end;

 suppose

 A5: (n -' 1) > 0 ;

 ( width ( Deleting (M,i,j))) = (n -' 1) by A2, A3, Th5;

 hence thesis by A4, A5, MATRIX_0: 20;

 end;

 end;

 end

 theorem :: LAPLACE:13



 Th13: for i, j st i in ( Seg n) & j in ( Seg n) holds for k, m st k in ( Seg (n -' 1)) & m in ( Seg (n -' 1)) holds (k = j implies (( Delete (M,i,j)) * (k,m)) = (M * (k,(m + 1)))) & (k >= i & m < j implies (( Delete (M,i,j)) * (k,m)) = (M * ((k + 1),m))) & (k >= i & m >= j implies (( Delete (M,i,j)) * (k,m)) = (M * ((k + 1),(m + 1))))

 proof

 let i, j such that

 A1: i in ( Seg n) and

 A2: j in ( Seg n);

 set DM = ( Delete (M,i,j));



 A3: ( Deleting (M,i,j)) = DM by A1, A2, Def1;

 n > 0 by A1;

 then

 reconsider n9 = (n - 1) as Element of NAT by NAT_1: 20;

 set DL = ( DelLine (M,i));

 let k, m such that

 A4: k in ( Seg (n -' 1)) and

 A5: m in ( Seg (n -' 1));



 A6: (n -' 1) = n9 by XREAL_0:def 2;

 then

 A7: (k + 1) in ( Seg (n9 + 1)) by A4, FINSEQ_1: 60;

 reconsider I = i, J = j, K = k, U = m as Element of NAT by ORDINAL1:def 12;

 n9 <= (n9 + 1) by NAT_1: 11;

 then

 A8: ( Seg n9) c= ( Seg n) by FINSEQ_1: 5;



 A9: ( len M) = n by MATRIX_0: 24;

 then

 A10: ( dom M) = ( Seg n) by FINSEQ_1:def 3;

 then ( len DL) = n9 by A1, A6, A9, Th1;

 then

 A11: ( dom DL) = ( Seg n9) by FINSEQ_1:def 3;

 then

 A12: (( Deleting (M,i,j)) . k) = ( Del (( Line (DL,k)),j)) by A4, A6, MATRIX_0:def 13;

 ( len DM) = n9 by A6, MATRIX_0: 24;

 then ( dom DM) = ( Seg n9) by FINSEQ_1:def 3;

 then

 A13: (DM . k) = ( Line (DM,k)) by A4, A6, MATRIX_0: 60;

 ( width DM) = n9 by A6, MATRIX_0: 24;

 then

 A14: (( Line (DM,k)) . m) = (DM * (k,m)) by A5, A6, MATRIX_0:def 7;



 A15: ( Line (DL,k)) = (DL . k) by A4, A6, A11, MATRIX_0: 60;



 A16: (m + 1) in ( Seg (n9 + 1)) by A5, A6, FINSEQ_1: 60;



 A17: K >= I implies (U < J implies (DM * (K,U)) = (M * ((K + 1),U))) & (U >= J implies (DM * (K,U)) = (M * ((K + 1),(U + 1))))

 proof

 assume

 A18: K >= I;

 K <= n9 by A4, A6, FINSEQ_1: 1;

 then

 A19: (DL . K) = (M . (K + 1)) by A1, A9, A10, A7, A18, FINSEQ_3: 111;



 A20: (M . (K + 1)) = ( Line (M,(K + 1))) by A10, A7, MATRIX_0: 60;

 thus U < J implies (DM * (K,U)) = (M * ((K + 1),U))

 proof



 A21: ( width M) = n by MATRIX_0: 24;

 assume U < J;

 then (DM * (K,U)) = (( Line (M,(K + 1))) . U) by A12, A3, A13, A14, A15, A19, A20, FINSEQ_3: 110;

 hence thesis by A5, A6, A8, A21, MATRIX_0:def 7;

 end;

 assume

 A22: U >= J;



 A23: U <= n9 by A5, A6, FINSEQ_1: 1;



 A24: ( width M) = n by MATRIX_0: 24;



 A25: ( len ( Line (DL,K))) = ( width M) by A15, A19, A20, MATRIX_0:def 7;

 then J in ( dom ( Line (DL,K))) by A2, A24, FINSEQ_1:def 3;

 then (DM * (K,U)) = (( Line (M,(K + 1))) . (U + 1)) by A12, A3, A13, A14, A15, A7, A19, A20, A22, A25, A23, FINSEQ_3: 111, MATRIX_0: 24;

 hence thesis by A16, A24, MATRIX_0:def 7;

 end;

 K = J implies (DM * (K,U)) = (M * (K,(U + 1))))

 proof

 assume K < I;

 then

 A26: (DL . K) = (M . K) by FINSEQ_3: 110;



 A27: (M . K) = ( Line (M,K)) by A4, A6, A10, A8, MATRIX_0: 60;

 thus U < J implies (DM * (K,U)) = (M * (K,U))

 proof

 assume

 A28: U < J;



 A29: ( width M) = (n9 + 1) by MATRIX_0: 24;

 (DM * (K,U)) = (( Line (M,K)) . U) by A12, A3, A13, A14, A15, A26, A27, A28, FINSEQ_3: 110;

 hence thesis by A5, A6, A8, A29, MATRIX_0:def 7;

 end;

 assume

 A30: U >= J;



 A31: U <= n9 by A5, A6, FINSEQ_1: 1;



 A32: ( width M) = n by MATRIX_0: 24;



 A33: ( len ( Line (DL,K))) = ( width M) by A15, A26, A27, MATRIX_0:def 7;

 then J in ( dom ( Line (DL,K))) by A2, A32, FINSEQ_1:def 3;

 then (DM * (K,U)) = (( Line (M,K)) . (U + 1)) by A12, A3, A13, A14, A15, A7, A26, A27, A30, A33, A31, FINSEQ_3: 111, MATRIX_0: 24;

 hence thesis by A16, A32, MATRIX_0:def 7;

 end;

 hence thesis by A17;

 end;

 theorem :: LAPLACE:14



 Th14: for i, j st i in ( Seg n) & j in ( Seg n) holds (( Delete (M,i,j)) @ ) = ( Delete ((M @ ),j,i))

 proof

 let i, j such that

 A1: i in ( Seg n) and

 A2: j in ( Seg n);

 n > 0 by A1;

 then

 reconsider n1 = (n - 1) as Element of NAT by NAT_1: 20;

 set X1 = ( Seg n);

 reconsider MT = (M @ ) as Matrix of n, K;

 set D = ( Delete (M,i,j));

 set n9 = (n -' 1);

 reconsider I = i as Element of NAT by ORDINAL1:def 12;

 reconsider DT = (D @ ) as Matrix of n9, K;

 set D9 = ( Delete (MT,j,i));

 set X = ( Seg n9);



 A3: ((n1 + 1) -' 1) = n1 by NAT_D: 34;

 now

 n9 <= n by NAT_D: 35;

 then

 A4: X c= X1 by FINSEQ_1: 5;

 let k,m be Nat such that

 A5: [k, m] in ( Indices DT);

 [m, k] in ( Indices D) by A5, MATRIX_0:def 6;

 then

 A6: (DT * (k,m)) = (D * (m,k)) by MATRIX_0:def 6;

 reconsider k9 = k, m9 = m as Element of NAT by ORDINAL1:def 12;



 A7: ( Indices DT) = [:X, X:] by MATRIX_0: 24;

 then

 A8: k in X by A5, ZFMISC_1: 87;

 then

 A9: (k + 1) in X1 by A3, FINSEQ_1: 60;



 A10: ( Indices M) = [:X1, X1:] by MATRIX_0: 24;



 A11: m in X by A5, A7, ZFMISC_1: 87;

 then

 A12: (m + 1) in X1 by A3, FINSEQ_1: 60;

 per cases ;

 suppose

 A13: m9 < I & k9 < j;

 then

 A14: (D9 * (k,m)) = (MT * (k,m)) by A1, A2, A8, A11, Th13;



 A15: [m, k] in ( Indices M) by A8, A11, A4, A10, ZFMISC_1: 87;

 (D * (m,k)) = (M * (m,k)) by A1, A2, A8, A11, A13, Th13;

 hence (DT * (k,m)) = (D9 * (k,m)) by A6, A15, A14, MATRIX_0:def 6;

 end;

 suppose

 A16: m9 = j;

 then

 A17: (D9 * (k,m)) = (MT * ((k + 1),m)) by A1, A2, A8, A11, Th13;



 A18: [m, (k + 1)] in ( Indices M) by A11, A4, A9, A10, ZFMISC_1: 87;

 (D * (m,k)) = (M * (m,(k + 1))) by A1, A2, A8, A11, A16, Th13;

 hence (DT * (k,m)) = (D9 * (k,m)) by A6, A18, A17, MATRIX_0:def 6;

 end;

 suppose

 A19: m9 >= I & k9 < j;

 then

 A20: (D9 * (k,m)) = (MT * (k,(m + 1))) by A1, A2, A8, A11, Th13;



 A21: [(m + 1), k] in ( Indices M) by A8, A4, A12, A10, ZFMISC_1: 87;

 (D * (m,k)) = (M * ((m + 1),k)) by A1, A2, A8, A11, A19, Th13;

 hence (DT * (k,m)) = (D9 * (k,m)) by A6, A21, A20, MATRIX_0:def 6;

 end;

 suppose

 A22: m9 >= I & k9 >= j;

 then

 A23: (D9 * (k,m)) = (MT * ((k + 1),(m + 1))) by A1, A2, A8, A11, Th13;



 A24: [(m + 1), (k + 1)] in ( Indices M) by A9, A12, A10, ZFMISC_1: 87;

 (D * (m,k)) = (M * ((m + 1),(k + 1))) by A1, A2, A8, A11, A22, Th13;

 hence (DT * (k,m)) = (D9 * (k,m)) by A6, A24, A23, MATRIX_0:def 6;

 end;

 end;

 hence thesis by MATRIX_0: 27;

 end;

 theorem :: LAPLACE:15



 Th15: for f be FinSequence of K, i, j st i in ( Seg n) & j in ( Seg n) holds ( Delete (M,i,j)) = ( Delete (( RLine (M,i,f)),i,j))

 proof

 let f be FinSequence of K, i, j such that

 A1: i in ( Seg n) and

 A2: j in ( Seg n);



 A3: ( Delete (M,i,j)) = ( Deleting (M,i,j)) by A1, A2, Def1;



 A4: ( Delete (( RLine (M,i,f)),i,j)) = ( Deleting (( RLine (M,i,f)),i,j)) by A1, A2, Def1;

 reconsider f9 = f as Element of (the carrier of K * ) by FINSEQ_1:def 11;

 reconsider I = i as Element of NAT by ORDINAL1:def 12;

 per cases ;

 suppose ( len f) = ( width M);

 then ( RLine (M,I,f)) = ( Replace (M,i,f9)) by MATRIX11: 29;

 hence thesis by A3, A4, COMPUT_1: 3;

 end;

 suppose ( len f) <> ( width M);

 hence thesis by MATRIX11:def 3;

 end;

 end;

 definition

 let c, n, m, D;

 let M be Matrix of n, m, D;

 let pD be FinSequence of D;

 :: LAPLACE:def2

 func ReplaceCol (M,c,pD) -> Matrix of n, m, D means

 : Def2: ( len it ) = ( len M) & ( width it ) = ( width M) & for i, j st [i, j] in ( Indices M) holds (j <> c implies (it * (i,j)) = (M * (i,j))) & (j = c implies (it * (i,c)) = (pD . i)) if ( len pD) = ( len M)

 otherwise it = M;

 consistency ;

 existence

 proof

 thus ( len pD) = ( len M) implies ex M1 be Matrix of n, m, D st ( len M1) = ( len M) & ( width M1) = ( width M) & for i, j st [i, j] in ( Indices M) holds (j <> c implies (M1 * (i,j)) = (M * (i,j))) & (j = c implies (M1 * (i,c)) = (pD . i))

 proof

 reconsider M9 = M as Matrix of ( len M), ( width M), D by MATRIX_0: 51;

 reconsider V = n, U = m as Element of NAT by ORDINAL1:def 12;

 defpred P[ set, set, set] means for i, j st i = $1 & j = $2 holds (j <> c implies $3 = (M * (i,j))) & (j = c implies $3 = (pD . i));

 assume

 A1: ( len pD) = ( len M);



 A2: for i,j be Nat st [i, j] in [:( Seg V), ( Seg U):] holds ex x be Element of D st P[i, j, x]

 proof

 let i,j be Nat such that

 A3: [i, j] in [:( Seg V), ( Seg U):];

 now

 per cases ;

 case

 A4: j = c;



 A5: ( rng pD) c= D by FINSEQ_1:def 4;

 ( len M) = n by MATRIX_0:def 2;

 then i in ( Seg ( len pD)) by A1, A3, ZFMISC_1: 87;

 then i in ( dom pD) by FINSEQ_1:def 3;

 then

 A6: (pD . i) in ( rng pD) by FUNCT_1:def 3;

 P[i, j, (pD . i)] by A4;

 hence thesis by A6, A5;

 end;

 case j <> c;

 then P[i, j, (M * (i,j))];

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 consider M1 be Matrix of V, U, D such that

 A7: for i,j be Nat st [i, j] in ( Indices M1) holds P[i, j, (M1 * (i,j))] from MATRIX_0:sch 2( A2);

 reconsider M1 as Matrix of n, m, D;

 take M1;

 A8:

 now

 per cases ;

 suppose

 A9: n = 0 ;

 then ( len M1) = 0 by MATRIX_0:def 2;

 then

 A10: ( width M1) = 0 by MATRIX_0:def 3;

 ( len M) = 0 by A9, MATRIX_0:def 2;

 hence ( len M) = ( len M1) & ( width M1) = ( width M) by A9, A10, MATRIX_0:def 2, MATRIX_0:def 3;

 end;

 suppose

 A11: n > 0 ;

 then

 A12: ( width M) = m by MATRIX_0: 23;

 ( len M) = n by A11, MATRIX_0: 23;

 hence ( len M) = ( len M1) & ( width M) = ( width M1) by A11, A12, MATRIX_0: 23;

 end;

 end;

 ( Indices M9) = ( Indices M1) by MATRIX_0: 26;

 hence thesis by A7, A8;

 end;

 thus thesis;

 end;

 uniqueness

 proof

 let M1,M2 be Matrix of n, m, D;

 thus ( len pD) = ( len M) & (( len M1) = ( len M) & ( width M1) = ( width M) & for i, j st [i, j] in ( Indices M) holds (j <> c implies (M1 * (i,j)) = (M * (i,j))) & (j = c implies (M1 * (i,c)) = (pD . i))) & (( len M2) = ( len M) & ( width M2) = ( width M) & for i, j st [i, j] in ( Indices M) holds (j <> c implies (M2 * (i,j)) = (M * (i,j))) & (j = c implies (M2 * (i,c)) = (pD . i))) implies M1 = M2

 proof

 assume ( len pD) = ( len M);

 assume that

 A13: ( len M1) = ( len M) and

 A14: ( width M1) = ( width M) and

 A15: for i, j st [i, j] in ( Indices M) holds (j <> c implies (M1 * (i,j)) = (M * (i,j))) & (j = c implies (M1 * (i,c)) = (pD . i));

 assume that ( len M2) = ( len M) and ( width M2) = ( width M) and

 A16: for i, j st [i, j] in ( Indices M) holds (j <> c implies (M2 * (i,j)) = (M * (i,j))) & (j = c implies (M2 * (i,c)) = (pD . i));

 for i,j be Nat st [i, j] in ( Indices M1) holds (M1 * (i,j)) = (M2 * (i,j))

 proof

 let i,j be Nat;

 assume [i, j] in ( Indices M1);

 then

 A17: [i, j] in ( Indices M) by A13, A14, MATRIX_4: 55;

 reconsider I = i, J = j as Element of NAT by ORDINAL1:def 12;



 A18: J = c implies (M1 * (I,c)) = (pD . I) by A15, A17;



 A19: J <> c implies (M2 * (I,J)) = (M * (I,J)) by A16, A17;

 J <> c implies (M1 * (I,J)) = (M * (I,J)) by A15, A17;

 hence thesis by A16, A17, A18, A19;

 end;

 hence thesis by MATRIX_0: 27;

 end;

 thus thesis;

 end;

 end

 notation

 let c, n, m, D;

 let M be Matrix of n, m, D;

 let pD be FinSequence of D;

 synonym RCol (M,c,pD) for ReplaceCol (M,c,pD);

 end

 theorem :: LAPLACE:16

 for i st i in ( Seg ( width AD)) holds (i = c & ( len pD) = ( len AD) implies ( Col (( RCol (AD,c,pD)),i)) = pD) & (i <> c implies ( Col (( RCol (AD,c,pD)),i)) = ( Col (AD,i)))

 proof

 let i such that

 A1: i in ( Seg ( width AD));

 set R = ( RCol (AD,c,pD));

 set CR = ( Col (R,i));

 thus i = c & ( len pD) = ( len AD) implies CR = pD

 proof

 assume that

 A2: i = c and

 A3: ( len pD) = ( len AD);



 A4: ( len R) = ( len pD) by A3, Def2;

 A5:

 now

 let J be Nat such that

 A6: 1 <= J and

 A7: J <= ( len pD);

 J in ( Seg ( len pD)) by A6, A7;

 then

 A8: J in ( dom R) by A4, FINSEQ_1:def 3;

 i in ( Seg ( width R)) by A1, A3, Def2;

 then

 A9: [J, c] in ( Indices R) by A2, A8, ZFMISC_1: 87;



 A10: ( Indices R) = ( Indices AD) by MATRIX_0: 26;

 (CR . J) = (R * (J,c)) by A2, A8, MATRIX_0:def 8;

 hence (CR . J) = (pD . J) by A3, A9, A10, Def2;

 end;

 ( len CR) = ( len pD) by A4, MATRIX_0:def 8;

 hence thesis by A5;

 end;

 set CA = ( Col (AD,i));



 A11: ( len AD) = n by MATRIX_0:def 2;



 A12: ( len R) = n by MATRIX_0:def 2;



 A13: ( len AD) = ( len CA) by MATRIX_0:def 8;

 assume

 A14: i <> c;

 A15:

 now

 let j be Nat such that

 A16: 1 <= j and

 A17: j <= ( len CA);



 A18: j in ( Seg ( len AD)) by A13, A16, A17;

 then

 A19: j in ( dom AD) by FINSEQ_1:def 3;

 then

 A20: (CA . j) = (AD * (j,i)) by MATRIX_0:def 8;

 j in ( dom R) by A11, A12, A18, FINSEQ_1:def 3;

 then

 A21: (CR . j) = (R * (j,i)) by MATRIX_0:def 8;



 A22: [j, i] in ( Indices AD) by A1, A19, ZFMISC_1: 87;

 per cases ;

 suppose ( len pD) = ( len AD);

 hence (CA . j) = (CR . j) by A14, A20, A21, A22, Def2;

 end;

 suppose ( len pD) <> ( len AD);

 hence (CA . j) = (CR . j) by Def2;

 end;

 end;

 ( len CR) = ( len R) by MATRIX_0:def 8;

 hence thesis by A11, A12, A13, A15;

 end;

 theorem :: LAPLACE:17

 not c in ( Seg ( width AD)) implies ( RCol (AD,c,pD)) = AD

 proof

 assume

 A1: not c in ( Seg ( width AD));

 set R = ( RCol (AD,c,pD));

 per cases ;

 suppose

 A2: ( len pD) = ( len AD);

 now

 let i,j be Nat such that

 A3: [i, j] in ( Indices AD);

 j in ( Seg ( width AD)) by A3, ZFMISC_1: 87;

 hence (R * (i,j)) = (AD * (i,j)) by A1, A2, A3, Def2;

 end;

 hence thesis by MATRIX_0: 27;

 end;

 suppose ( len pD) <> ( len AD);

 hence thesis by Def2;

 end;

 end;

 theorem :: LAPLACE:18

 ( RCol (AD,c,( Col (AD,c)))) = AD

 proof

 set C = ( Col (AD,c));

 set R = ( RCol (AD,c,C));

 now

 reconsider c as Element of NAT by ORDINAL1:def 12;

 let i,j be Nat such that

 A1: [i, j] in ( Indices AD);



 A2: ( len C) = ( len AD) by MATRIX_0:def 8;

 reconsider I = i, J = j as Element of NAT by ORDINAL1:def 12;



 A3: i in ( dom AD) by A1, ZFMISC_1: 87;

 now

 per cases ;

 suppose

 A4: c = j;



 hence (R * (i,j)) = (C . I) by A1, A2, Def2

 .= (AD * (i,j)) by A3, A4, MATRIX_0:def 8;

 end;

 suppose c <> J;

 hence (R * (i,j)) = (AD * (i,j)) by A1, A2, Def2;

 end;

 end;

 hence (R * (i,j)) = (AD * (i,j));

 end;

 hence thesis by MATRIX_0: 27;

 end;

 theorem :: LAPLACE:19



 Th19: for A be Matrix of n, m, D, A9 be Matrix of m, n, D st A9 = (A @ ) & (m = 0 implies n = 0 ) holds ( ReplaceCol (A,c,pD)) = (( ReplaceLine (A9,c,pD)) @ )

 proof

 let A be Matrix of n, m, D, A9 be Matrix of m, n, D such that

 A1: A9 = (A @ ) and

 A2: m = 0 implies n = 0 ;

 set RC = ( ReplaceCol (A,c,pD));

 set RL = ( ReplaceLine (A9,c,pD));

 now

 per cases ;

 suppose

 A3: n = 0 ;

 then 0 = ( len A) by MATRIX_0:def 2;



 then 0 = ( width A) by MATRIX_0:def 3

 .= ( len A9) by A1, MATRIX_0:def 6;

 then m = 0 by MATRIX_0:def 2;

 then ( len RL) = 0 by MATRIX_0:def 2;

 then ( width RL) = 0 by MATRIX_0:def 3;

 then ( len (RL @ )) = 0 by MATRIX_0:def 6;

 then

 A4: (RL @ ) = {} ;

 ( len RC) = 0 by A3, MATRIX_0:def 2;

 hence thesis by A4;

 end;

 suppose

 A5: ( len pD) <> ( len A) & n > 0 ;

 then

 A6: ( width A) = m by MATRIX_0: 23;

 then

 A7: ( width A9) = ( len A) by A1, A2, A5, MATRIX_0: 54;



 A8: ( len A) = n by A5, MATRIX_0: 23;



 thus RC = A by A5, Def2

 .= ((A @ ) @ ) by A2, A5, A8, A6, MATRIX_0: 57

 .= (RL @ ) by A1, A5, A7, MATRIX11:def 3;

 end;

 suppose

 A9: ( len pD) = ( len A) & n > 0 ;

 then

 A10: ( width RL) = n by A2, MATRIX_0: 23;

 then

 A11: ( len (RL @ )) = n by A9, MATRIX_0: 54;

 ( len RL) = m by A2, A9, MATRIX_0: 23;

 then ( width (RL @ )) = m by A9, A10, MATRIX_0: 54;

 then

 reconsider RL9 = (RL @ ) as Matrix of n, m, D by A11, MATRIX_0: 51;



 A12: ( len A) = n by A9, MATRIX_0: 23;



 A13: ( width A9) = n by A2, A9, MATRIX_0: 23;

 now



 A14: ( Indices RC) = ( Indices A) by MATRIX_0: 26;



 A15: ( Indices RL) = ( Indices A9) by MATRIX_0: 26;

 let i,j be Nat such that

 A16: [i, j] in ( Indices RC);

 reconsider I = i, J = j as Element of NAT by ORDINAL1:def 12;

 ( Indices RC) = ( Indices RL9) by MATRIX_0: 26;

 then

 A17: [j, i] in ( Indices RL) by A16, MATRIX_0:def 6;

 per cases ;

 suppose

 A18: J = c;



 hence (RC * (i,j)) = (pD . I) by A9, A16, A14, Def2

 .= (RL * (J,I)) by A9, A12, A13, A17, A15, A18, MATRIX11:def 3

 .= (RL9 * (i,j)) by A17, MATRIX_0:def 6;

 end;

 suppose

 A19: J <> c;



 hence (RC * (i,j)) = (A * (I,J)) by A9, A16, A14, Def2

 .= (A9 * (j,i)) by A1, A16, A14, MATRIX_0:def 6

 .= (RL * (J,I)) by A9, A12, A13, A17, A15, A19, MATRIX11:def 3

 .= (RL9 * (i,j)) by A17, MATRIX_0:def 6;

 end;

 end;

 hence thesis by MATRIX_0: 27;

 end;

 end;

 hence thesis;

 end;

 begin

 definition

 let i, n;

 let perm be Element of ( Permutations (n + 1));

 assume

 A1: i in ( Seg (n + 1));

 :: LAPLACE:def3

 func Rem (perm,i) -> Element of ( Permutations n) means

 : Def3: for k st k in ( Seg n) holds (k = (perm . i) implies (it . k) = ((perm . k) - 1))) & (k >= i implies ((perm . (k + 1)) < (perm . i) implies (it . k) = (perm . (k + 1))) & ((perm . (k + 1)) >= (perm . i) implies (it . k) = ((perm . (k + 1)) - 1)));

 existence

 proof

 set j = (perm . i);

 set P = ( Permutations n);

 set p = perm;

 set n1 = (n + 1);

 reconsider N = n as Element of NAT by ORDINAL1:def 12;

 reconsider p9 = p as Permutation of ( Seg n1) by MATRIX_1:def 12;



 A2: ( dom p9) = ( Seg n1) by FUNCT_2: 52;

 defpred Q[ object, object] means for k st k in ( Seg n) & $1 = k holds (k = j implies $2 = ((p . k) - 1))) & (k >= i implies ((p . (k + 1)) < j implies $2 = (p . (k + 1))) & ((p . (k + 1)) >= j implies $2 = ((p . (k + 1)) - 1)));



 A3: ( rng p9) = ( Seg n1) by FUNCT_2:def 3;

 then

 A4: j in ( Seg n1) by A1, A2, FUNCT_1:def 3;



 A5: for k9 be object st k9 in ( Seg n) holds ex y be object st y in ( Seg n) & Q[k9, y]

 proof

 let k9 be object;

 assume k9 in ( Seg n);

 then

 consider k be Nat such that

 A6: k9 = k and

 A7: 1 <= k and

 A8: k <= n;



 A9: k < n1 by A8, NAT_1: 13;

 then

 A10: k in ( Seg n1) by A7;

 then

 A11: (p . k) in ( Seg n1) by A2, A3, FUNCT_1:def 3;

 set k1 = (k + 1);



 A12: (1 + 0 ) <= (k + 1) by NAT_1: 13;

 (k + 1) <= n1 by A9, NAT_1: 13;

 then

 A13: (k + 1) in ( Seg n1) by A12;

 then

 A14: (p . (k + 1)) in ( Seg n1) by A2, A3, FUNCT_1:def 3;

 per cases ;

 suppose

 A15: k < i & (p . k) < j;

 j <= n1 by A4, FINSEQ_1: 1;

 then (p . k) < n1 by A15, XXREAL_0: 2;

 then

 A16: (p . k) <= n by NAT_1: 13;



 A17: Q[k9, (p . k)] by A6, A15;

 1 <= (p . k) by A11, FINSEQ_1: 1;

 then (p . k) in ( Seg n) by A16;

 hence thesis by A17;

 end;

 suppose

 A18: k = j;

 then (p9 . k) <> (p9 . i) by A1, A10, FUNCT_2: 19;

 then

 A19: (p . k) > j by A18, XXREAL_0: 1;

 then

 reconsider pk1 = ((p . k) - 1) as Element of NAT by NAT_1: 20;



 A20: Q[k9, pk1] by A6, A18;



 A21: pk1 < (pk1 + 1) by NAT_1: 13;

 (p . k) <= n1 by A11, FINSEQ_1: 1;

 then pk1 < n1 by A21, XXREAL_0: 2;

 then

 A22: pk1 <= n by NAT_1: 13;

 j >= 1 by A4, FINSEQ_1: 1;

 then (pk1 + 1) > 1 by A19, XXREAL_0: 2;

 then pk1 >= 1 by NAT_1: 13;

 then pk1 in ( Seg n) by A22;

 hence thesis by A20;

 end;

 suppose

 A23: k >= i & (p . k1) < j;

 j <= n1 by A4, FINSEQ_1: 1;

 then (p . k1) < n1 by A23, XXREAL_0: 2;

 then

 A24: (p . k1) <= n by NAT_1: 13;



 A25: Q[k9, (p . k1)] by A6, A23;

 1 <= (p . k1) by A14, FINSEQ_1: 1;

 then (p . k1) in ( Seg n) by A24;

 hence thesis by A25;

 end;

 suppose

 A26: k >= i & (p . k1) >= j;

 then i < k1 by NAT_1: 13;

 then (p9 . k1) <> (p9 . i) by A1, A13, FUNCT_2: 19;

 then

 A27: (p . k1) > j by A26, XXREAL_0: 1;

 then

 reconsider pk1 = ((p . k1) - 1) as Element of NAT by NAT_1: 20;



 A28: Q[k9, pk1] by A6, A26;



 A29: pk1 < (pk1 + 1) by NAT_1: 13;

 (p . k1) <= n1 by A14, FINSEQ_1: 1;

 then pk1 < n1 by A29, XXREAL_0: 2;

 then

 A30: pk1 <= n by NAT_1: 13;

 j >= 1 by A4, FINSEQ_1: 1;

 then (pk1 + 1) > 1 by A27, XXREAL_0: 2;

 then pk1 >= 1 by NAT_1: 13;

 then pk1 in ( Seg n) by A30;

 hence thesis by A28;

 end;

 end;

 consider q be Function of ( Seg n), ( Seg n) such that

 A31: for x be object st x in ( Seg n) holds Q[x, (q . x)] from FUNCT_2:sch 1( A5);

 for x1,x2 be object st x1 in ( dom q) & x2 in ( dom q) & (q . x1) = (q . x2) holds x1 = x2

 proof

 let x1,x2 be object such that

 A32: x1 in ( dom q) and

 A33: x2 in ( dom q) and

 A34: (q . x1) = (q . x2);



 A35: ( dom q) = ( Seg n) by FUNCT_2: 52;

 then

 consider k1 be Nat such that

 A36: x1 = k1 and

 A37: 1 <= k1 and

 A38: k1 <= n by A32;



 A39: ( 0 + 1) <= (k1 + 1) by NAT_1: 13;



 A40: k1 < (n + 1) by A38, NAT_1: 13;

 then

 A41: k1 in ( Seg n1) by A37;

 (k1 + 1) <= (n + 1) by A40, NAT_1: 13;

 then

 A42: (k1 + 1) in ( Seg n1) by A39;

 consider k2 be Nat such that

 A43: x2 = k2 and

 A44: 1 <= k2 and

 A45: k2 <= n by A33, A35;



 A46: k2 < (n + 1) by A45, NAT_1: 13;

 then

 A47: k2 in ( Seg n1) by A44;



 A48: ( 0 + 1) <= (k2 + 1) by NAT_1: 13;

 (k2 + 1) <= (n + 1) by A46, NAT_1: 13;

 then

 A49: (k2 + 1) in ( Seg n1) by A48;

 per cases ;

 suppose

 A50: k1 < i & (p . k1) < j;

 then

 A51: (q . k1) = (p9 . k1) by A31, A32, A36;

 per cases ;

 suppose k2 < i & (p . k2) < j;

 then (p9 . k2) = (p9 . k1) by A31, A33, A34, A36, A43, A51;

 hence thesis by A2, A36, A43, A41, A47, FUNCT_1:def 4;

 end;

 suppose

 A52: k2 = j;

 then (q . k2) = ((p . k2) - 1) by A31, A33, A43;

 then ((p . k1) + 1) = (p . k2) by A34, A36, A43, A51;

 then (p . k2) <= j by A50, NAT_1: 13;

 then (p9 . k2) = (p9 . i) by A52, XXREAL_0: 1;

 hence thesis by A1, A2, A47, A52, FUNCT_1:def 4;

 end;

 suppose

 A53: k2 >= i & (p . (k2 + 1)) < j;

 then (p9 . k1) = (p9 . (k2 + 1)) by A31, A33, A34, A36, A43, A51;

 then k1 = (k2 + 1) by A2, A41, A49, FUNCT_1:def 4;

 hence thesis by A50, A53, NAT_1: 13;

 end;

 suppose

 A54: k2 >= i & (p . (k2 + 1)) >= j;

 then (p . k1) = ((p . (k2 + 1)) - 1) by A31, A33, A34, A36, A43, A51;

 then ((p . k1) + 1) = (p . (k2 + 1));

 then (p . (k2 + 1)) <= j by A50, NAT_1: 13;

 then (p9 . (k2 + 1)) = (p . i) by A54, XXREAL_0: 1;

 then (k2 + 1) = i by A1, A2, A49, FUNCT_1:def 4;

 hence thesis by A54, NAT_1: 13;

 end;

 end;

 suppose

 A55: k1 = j;

 then

 A56: (q . k1) = ((p . k1) - 1) by A31, A32, A36;

 per cases ;

 suppose

 A57: k2 < i & (p . k2) < j;

 then (q . k2) = (p9 . k2) by A31, A33, A43;

 then (p . k1) = ((p . k2) + 1) by A34, A36, A43, A56;

 then (p . k1) <= j by A57, NAT_1: 13;

 then (p . k1) = (p . i) by A55, XXREAL_0: 1;

 hence thesis by A1, A2, A41, A55, FUNCT_1:def 4;

 end;

 suppose k2 = j;

 then ((p . k1) - 1) = ((p . k2) - 1) by A31, A33, A34, A36, A43, A56;

 hence thesis by A2, A36, A43, A41, A47, FUNCT_1:def 4;

 end;

 suppose

 A58: k2 >= i & (p . (k2 + 1)) < j;

 then ((p . k1) - 1) = (p . (k2 + 1)) by A31, A33, A34, A36, A43, A56;

 then ((p . (k2 + 1)) + 1) = (p . k1);

 then (p . k1) <= j by A58, NAT_1: 13;

 then (p9 . k1) = (p9 . i) by A55, XXREAL_0: 1;

 hence thesis by A1, A2, A41, A55, FUNCT_1:def 4;

 end;

 suppose

 A59: k2 >= i & (p . (k2 + 1)) >= j;

 then ((p . k1) - 1) = ((p . (k2 + 1)) - 1) by A31, A33, A34, A36, A43, A56;

 then k1 = (k2 + 1) by A2, A41, A49, FUNCT_1:def 4;

 hence thesis by A55, A59, NAT_1: 13;

 end;

 end;

 suppose

 A60: k1 >= i & (p . (k1 + 1)) < j;

 then

 A61: (q . k1) = (p . (k1 + 1)) by A31, A32, A36;

 per cases ;

 suppose

 A62: k2 < i & (p . k2) < j;

 then (p9 . (k1 + 1)) = (p9 . k2) by A31, A33, A34, A36, A43, A61;

 then (k1 + 1) = k2 by A2, A47, A42, FUNCT_1:def 4;

 hence thesis by A60, A62, NAT_1: 13;

 end;

 suppose

 A63: k2 = j;

 then (p . (k1 + 1)) = ((p . k2) - 1) by A31, A33, A34, A36, A43, A61;

 then (p . k2) = ((p . (k1 + 1)) + 1);

 then (p . k2) <= j by A60, NAT_1: 13;

 then (p9 . k2) = (p9 . i) by A63, XXREAL_0: 1;

 hence thesis by A1, A2, A47, A63, FUNCT_1:def 4;

 end;

 suppose k2 >= i & (p . (k2 + 1)) < j;

 then (q . k2) = (p . (k2 + 1)) by A31, A33, A43;

 then (k1 + 1) = (k2 + 1) by A2, A34, A36, A43, A42, A49, A61, FUNCT_1:def 4;

 hence thesis by A36, A43;

 end;

 suppose

 A64: k2 >= i & (p . (k2 + 1)) >= j;

 then (p . (k1 + 1)) = ((p . (k2 + 1)) - 1) by A31, A33, A34, A36, A43, A61;

 then (p . (k2 + 1)) = ((p . (k1 + 1)) + 1);

 then (p . (k2 + 1)) <= j by A60, NAT_1: 13;

 then (p9 . (k2 + 1)) = (p9 . i) by A64, XXREAL_0: 1;

 then (k2 + 1) = i by A1, A2, A49, FUNCT_1:def 4;

 hence thesis by A64, NAT_1: 13;

 end;

 end;

 suppose

 A65: k1 >= i & (p . (k1 + 1)) >= j;

 then

 A66: (q . k1) = ((p . (k1 + 1)) - 1) by A31, A32, A36;

 per cases ;

 suppose

 A67: k2 < i & (p . k2) < j;

 then ((p . (k1 + 1)) - 1) = (p . k2) by A31, A33, A34, A36, A43, A66;

 then (p . (k1 + 1)) = ((p . k2) + 1);

 then (p . (k1 + 1)) <= j by A67, NAT_1: 13;

 then (p9 . (k1 + 1)) = (p9 . i) by A65, XXREAL_0: 1;

 then (k1 + 1) = i by A1, A2, A42, FUNCT_1:def 4;

 hence thesis by A65, NAT_1: 13;

 end;

 suppose

 A68: k2 = j;

 then ((p . (k1 + 1)) - 1) = ((p . k2) - 1) by A31, A33, A34, A36, A43, A66;

 then (k1 + 1) = k2 by A2, A47, A42, FUNCT_1:def 4;

 hence thesis by A65, A68, NAT_1: 13;

 end;

 suppose

 A69: k2 >= i & (p . (k2 + 1)) < j;

 then ((p . (k1 + 1)) - 1) = (p . (k2 + 1)) by A31, A33, A34, A36, A43, A66;

 then (p . (k1 + 1)) = ((p . (k2 + 1)) + 1);

 then (p . (k1 + 1)) <= j by A69, NAT_1: 13;

 then (p9 . (k1 + 1)) = (p9 . i) by A65, XXREAL_0: 1;

 then (k1 + 1) = i by A1, A2, A42, FUNCT_1:def 4;

 hence thesis by A65, NAT_1: 13;

 end;

 suppose k2 >= i & (p . (k2 + 1)) >= j;

 then ((p . (k1 + 1)) - 1) = ((p . (k2 + 1)) - 1) by A31, A33, A34, A36, A43, A66;

 then (k1 + 1) = (k2 + 1) by A2, A42, A49, FUNCT_1:def 4;

 hence thesis by A36, A43;

 end;

 end;

 end;

 then

 A70: q is one-to-one by FUNCT_1:def 4;

 ( card ( finSeg N)) = ( card ( finSeg N));

 then q is one-to-one onto by A70, FINSEQ_4: 63;

 then

 reconsider q as Element of P by MATRIX_1:def 12;

 take q;

 thus thesis by A31;

 end;

 uniqueness

 proof

 set p = perm;

 let q1,q2 be Element of ( Permutations n) such that

 A71: for k st k in ( Seg n) holds (k = (p . i) implies (q1 . k) = ((p . k) - 1))) & (k >= i implies ((p . (k + 1)) < (p . i) implies (q1 . k) = (p . (k + 1))) & ((p . (k + 1)) >= (p . i) implies (q1 . k) = ((p . (k + 1)) - 1))) and

 A72: for k st k in ( Seg n) holds (k = (p . i) implies (q2 . k) = ((p . k) - 1))) & (k >= i implies ((p . (k + 1)) < (p . i) implies (q2 . k) = (p . (k + 1))) & ((p . (k + 1)) >= (p . i) implies (q2 . k) = ((p . (k + 1)) - 1)));



 A73: q1 is Permutation of ( Seg n) by MATRIX_1:def 12;

 then

 A74: ( dom q1) = ( Seg n) by FUNCT_2: 52;

 A75:

 now

 let x be object such that

 A76: x in ( dom q1);

 consider k be Nat such that

 A77: x = k and 1 <= k and k <= n by A74, A76;

 set k1 = (k + 1);



 A78: (p . k) < (p . i) or (p . k) >= (p . i);



 A79: (p . k1) < (p . i) or (p . k1) >= (p . i);

 k = i;

 then (p . k) < (p . i) & (q1 . k) = (p . k) & (q2 . k) = (p . k) or (p . k) >= (p . i) & (q1 . k) = ((p . k) - 1) & (q2 . k) = ((p . k) - 1) or (p . k1) < (p . i) & (q1 . k) = (p . k1) & (q2 . k) = (p . k1) or (p . k1) >= (p . i) & (q1 . k) = ((p . k1) - 1) & (q2 . k) = ((p . k1) - 1) by A71, A72, A74, A76, A77, A78, A79;

 hence (q1 . x) = (q2 . x) by A77;

 end;

 q2 is Permutation of ( Seg n) by MATRIX_1:def 12;

 then ( dom q2) = ( Seg n) by FUNCT_2: 52;

 hence thesis by A73, A75, FUNCT_1: 2, FUNCT_2: 52;

 end;

 end

 theorem :: LAPLACE:20



 Th20: for i, j st i in ( Seg (n + 1)) & j in ( Seg (n + 1)) holds for P be set st P = { p1 : (p1 . i) = j } holds ex Proj be Function of P, ( Permutations n) st Proj is bijective & for q1 st (q1 . i) = j holds (Proj . q1) = ( Rem (q1,i))

 proof

 let i, j such that

 A1: i in ( Seg (n + 1)) and

 A2: j in ( Seg (n + 1));

 set n1 = (n + 1);

 reconsider N = n as Element of NAT by ORDINAL1:def 12;

 set P1 = ( Permutations (N + 1));

 defpred F[ object, object] means for p be Element of P1 st $1 = p & (p . i) = j holds $2 = ( Rem (p,i));

 let X be set such that

 A3: X = { p1 : (p1 . i) = j };



 A4: for x be object st x in X holds ex y be object st y in ( Permutations n) & F[x, y]

 proof

 let x be object;

 assume x in X;

 then

 consider p be Element of P1 such that

 A5: p = x and (p . i) = j by A3;

 take ( Rem (p,i));

 thus thesis by A5;

 end;

 consider f be Function of X, ( Permutations n) such that

 A6: for x be object st x in X holds F[x, (f . x)] from FUNCT_2:sch 1( A4);

 for x1,x2 be object st x1 in X & x2 in X & (f . x1) = (f . x2) holds x1 = x2

 proof

 let x1,x2 be object such that

 A7: x1 in X and

 A8: x2 in X and

 A9: (f . x1) = (f . x2);

 consider p1 be Element of P1 such that

 A10: p1 = x1 and

 A11: (p1 . i) = j by A3, A7;

 set R1 = ( Rem (p1,i));



 A12: (f . x1) = R1 by A6, A7, A10, A11;

 consider p2 be Element of P1 such that

 A13: p2 = x2 and

 A14: (p2 . i) = j by A3, A8;

 set R2 = ( Rem (p2,i));



 A15: (f . x2) = R2 by A6, A8, A13, A14;

 reconsider p19 = p1, p29 = p2 as Permutation of ( Seg n1) by MATRIX_1:def 12;



 A16: ( dom p29) = ( Seg n1) by FUNCT_2: 52;



 A17: ( dom p19) = ( Seg n1) by FUNCT_2: 52;

 now

 let x be object such that

 A18: x in ( Seg n1);

 consider k be Nat such that

 A19: x = k and

 A20: 1 <= k and

 A21: k <= n1 by A18;

 per cases by XXREAL_0: 1;

 suppose

 A22: k < i;

 i <= n1 by A1, FINSEQ_1: 1;

 then k < n1 by A22, XXREAL_0: 2;

 then k <= n by NAT_1: 13;

 then

 A23: k in ( Seg n) by A20;

 per cases ;

 suppose (p1 . k) < j & (p2 . k) < j or (p1 . k) >= j & (p2 . k) >= j;

 then (R1 . k) = (p1 . k) & (R2 . k) = (p2 . k) or (R1 . k) = ((p1 . k) - 1) & (R2 . k) = ((p2 . k) - 1) by A1, A11, A14, A22, A23, Def3;

 hence (p1 . x) = (p2 . x) by A9, A12, A15, A19;

 end;

 suppose (p1 . k) < j & (p2 . k) >= j or (p1 . k) >= j & (p2 . k) < j;

 then (R1 . k) = (p1 . k) & (R2 . k) = ((p2 . k) - 1) & (p1 . k) < j & (p2 . k) >= j or (R1 . k) = ((p1 . k) - 1) & (R2 . k) = (p2 . k) & (p1 . k) >= j & (p2 . k) < j by A1, A11, A14, A22, A23, Def3;

 then ((p1 . k) + 1) = (p2 . k) & (p1 . k) < j & (p2 . k) >= j or (p1 . k) = ((p2 . k) + 1) & (p1 . k) >= j & (p2 . k) < j by A9, A12, A15;

 then (p2 . k) <= j & (p2 . k) >= j or (p1 . k) >= j & (p1 . k) <= j by NAT_1: 13;

 then (p29 . k) = (p29 . i) or (p19 . k) = (p19 . i) by A11, A14, XXREAL_0: 1;

 hence (p1 . x) = (p2 . x) by A1, A17, A16, A18, A19, A22, FUNCT_1:def 4;

 end;

 end;

 suppose k = i;

 hence (p1 . x) = (p2 . x) by A11, A14, A19;

 end;

 suppose

 A24: k > i;

 then

 reconsider k1 = (k - 1) as Element of NAT by NAT_1: 20;

 (k1 + 1) > i by A24;

 then

 A25: k1 >= i by NAT_1: 13;

 (k1 + 1) <= n1 by A21;

 then k1 < n1 by NAT_1: 13;

 then

 A26: k1 <= n by NAT_1: 13;

 1 <= i by A1, FINSEQ_1: 1;

 then 1 < (k1 + 1) by A24, XXREAL_0: 2;

 then 1 <= k1 by NAT_1: 13;

 then

 A27: k1 in ( Seg n) by A26;

 per cases ;

 suppose (p1 . (k1 + 1)) < j & (p2 . (k1 + 1)) < j or (p1 . (k1 + 1)) >= j & (p2 . (k1 + 1)) >= j;

 then (R1 . k1) = (p1 . k) & (R2 . k1) = (p2 . k) or (R1 . k1) = ((p1 . k) - 1) & (R2 . k1) = ((p2 . k) - 1) by A1, A11, A14, A27, A25, Def3;

 hence (p1 . x) = (p2 . x) by A9, A12, A15, A19;

 end;

 suppose (p1 . (k1 + 1)) < j & (p2 . (k1 + 1)) >= j or (p1 . (k1 + 1)) >= j & (p2 . (k1 + 1)) < j;

 then (R1 . k1) = (p1 . k) & (R2 . k1) = ((p2 . k) - 1) & (p1 . k) < j & (p2 . k) >= j or (R1 . k1) = ((p1 . k) - 1) & (R2 . k1) = (p2 . k) & (p1 . k) >= j & (p2 . k) < j by A1, A11, A14, A27, A25, Def3;

 then ((p1 . k) + 1) = (p2 . k) & (p1 . k) < j & (p2 . k) >= j or (p1 . k) = ((p2 . k) + 1) & (p1 . k) >= j & (p2 . k) < j by A9, A12, A15;

 then (p2 . k) <= j & (p2 . k) >= j or (p1 . k) >= j & (p1 . k) <= j by NAT_1: 13;

 then (p29 . k) = (p29 . i) or (p19 . k) = (p19 . i) by A11, A14, XXREAL_0: 1;

 hence (p1 . x) = (p2 . x) by A1, A17, A16, A18, A19, A24, FUNCT_1:def 4;

 end;

 end;

 end;

 hence thesis by A10, A13, A17, A16, FUNCT_1: 2;

 end;

 then

 A28: f is one-to-one by FUNCT_2: 19;

 set P = ( Permutations N);

 ( card X) = (N ! ) by A1, A2, A3, Th7;

 then

 reconsider P9 = P, X9 = X as finite set;

 take f;



 A30: ( card P9) = (n ! ) by Th6;

 ( card X9) = (n ! ) by A1, A2, A3, Th7;

 then f is onto one-to-one by A28, A30, FINSEQ_4: 63;

 hence f is bijective;

 let p be Element of ( Permutations (n + 1)) such that

 A31: (p . i) = j;

 p in X by A3, A31;

 hence thesis by A6, A31;

 end;

 theorem :: LAPLACE:21



 Th21: for i, j st i in ( Seg (n + 1)) & (p1 . i) = j holds ( - (a,p1)) = ((( power K) . (( - ( 1_ K)),(i + j))) * ( - (a,( Rem (p1,i)))))

 proof

 set n1 = (n + 1);

 let i, j such that

 A1: i in ( Seg n1) and

 A2: (p1 . i) = j;



 A3: p1 is Permutation of ( Seg n1) by MATRIX_1:def 12;

 then

 A4: ( rng p1) = ( Seg n1) by FUNCT_2:def 3;

 ( dom p1) = ( Seg n1) by A3, FUNCT_2: 52;

 then

 A5: j in ( Seg n1) by A1, A2, A4, FUNCT_1:def 3;

 set R = ( Rem (p1,i));

 per cases by NAT_1: 23;

 suppose

 A6: n = 0 ;

 then R is even by Th11;

 then

 A7: ( - (a,R)) = a by MATRIX_1:def 16;



 A8: (1 + 1) = (2 * 1);

 p1 is even by A6, Th11;

 then

 A9: ( - (a,p1)) = a by MATRIX_1:def 16;



 A10: j = 1 by A5, A6, FINSEQ_1: 2, TARSKI:def 1;

 i = 1 by A1, A6, FINSEQ_1: 2, TARSKI:def 1;

 then (( power K) . (( - ( 1_ K)),(i + j))) = ( 1_ K) by A10, A8, HURWITZ: 4;

 hence thesis by A9, A7;

 end;

 suppose

 A11: n = 1;

 then

 A12: p1 is Permutation of ( Seg 2) by MATRIX_1:def 12;

 per cases by A12, MATRIX_7: 1;

 suppose

 A13: p1 = <*1, 2*>;

 i = 1 or i = 2 by A1, A11, FINSEQ_1: 2, TARSKI:def 2;

 then i = 1 & (p1 . i) = 1 or i = 2 & (p1 . i) = 2 by A13, FINSEQ_1: 44;

 then (i + j) = (2 * 1) or (i + j) = (2 * 2) by A2;

 then

 A14: (( power K) . (( - ( 1_ K)),(i + j))) = ( 1_ K) by HURWITZ: 4;



 A15: ( len ( Permutations 2)) = 2 by MATRIX_1: 9;

 R is even by A11, Th11;

 then

 A16: ( - (a,R)) = a by MATRIX_1:def 16;

 ( id ( Seg 2)) is even by MATRIX_1: 16;

 then ( - (a,p1)) = a by A11, A13, A15, FINSEQ_2: 52, MATRIX_1:def 16;

 hence thesis by A14, A16;

 end;

 suppose

 A17: p1 = <*2, 1*>;

 ( len ( Permutations 2)) = 2 by MATRIX_1: 9;

 then ( - (a,p1)) = ( - a) by A11, A17, MATRIX_1:def 16, MATRIX_9: 12;

 then

 A18: ( - (a,p1)) = ( - (( 1_ K) * a));

 i = 1 or i = 2 by A1, A11, FINSEQ_1: 2, TARSKI:def 2;

 then (i + j) = ((2 * 1) + 1) by A2, A17, FINSEQ_1: 44;

 then

 A19: (( power K) . (( - ( 1_ K)),(i + j))) = ( - ( 1_ K)) by HURWITZ: 4;

 R is even by A11, Th11;

 then ( - (a,R)) = a by MATRIX_1:def 16;

 hence thesis by A19, A18, VECTSP_1: 8;

 end;

 end;

 suppose

 A20: n >= 2;

 then

 reconsider n2 = (n - 2) as Element of NAT by NAT_1: 21;

 per cases ;

 suppose

 A21: not K is Fanoian;

 A22:

 now

 per cases by NAT_D: 12;

 suppose ((i + j) mod 2) = 0 ;

 then

 consider t be Nat such that

 A23: (i + j) = ((2 * t) + 0 ) and 0 < 2 by NAT_D:def 2;

 t is Element of NAT by ORDINAL1:def 12;

 hence (( power K) . (( - ( 1_ K)),(i + j))) = ( 1_ K) by A23, HURWITZ: 4;

 end;

 suppose ((i + j) mod 2) = 1;

 then

 consider t be Nat such that

 A24: (i + j) = ((2 * t) + 1) and 1 < 2 by NAT_D:def 2;



 A25: ( 1_ K) = ( - ( 1_ K)) by A21, MATRIX11: 22;

 t is Element of NAT by ORDINAL1:def 12;

 hence (( power K) . (( - ( 1_ K)),(i + j))) = ( 1_ K) by A24, A25, HURWITZ: 4;

 end;

 end;



 A26: ( - (a,p1)) = a or ( - (a,p1)) = ( - a) by MATRIX_1:def 16;

 ( - ( 1_ K)) = ( 1_ K) by A21, MATRIX11: 22;

 then

 A27: ( - (a * ( 1_ K))) = (a * ( 1_ K)) by VECTSP_1: 9;

 ( - (a,R)) = a or ( - (a,R)) = ( - a) by MATRIX_1:def 16;

 then ( - (a,R)) = a by A27;

 hence thesis by A22, A26, A27;

 end;

 suppose

 A29: K is Fanoian;

 set mm = the multF of K;

 reconsider n1 = (n2 + 1) as Element of NAT ;

 set P1 = ( Permutations (n1 + 2));

 reconsider Q1 = p1 as Element of P1;

 set SS1 = ( 2Set ( Seg (n1 + 2)));

 consider X be Element of ( Fin SS1) such that

 A30: X = { {N, i} where N be Nat : {N, i} in SS1 } and

 A31: (mm $$ (X,( Part_sgn (Q1,K)))) = (( power K) . (( - ( 1_ K)),(i + j))) by A1, A2, A29, Th9;

 set PQ1 = ( Part_sgn (Q1,K));

 set SS2 = ( 2Set ( Seg (n2 + 2)));

 reconsider Q19 = Q1 as Permutation of ( Seg (n1 + 2)) by MATRIX_1:def 12;

 set P2 = ( Permutations (n2 + 2));

 reconsider Q = R as Element of P2;

 reconsider Q9 = Q as Permutation of ( Seg (n2 + 2)) by MATRIX_1:def 12;

 set PQ = ( Part_sgn (Q,K));

 SS1 in ( Fin SS1) by FINSUB_1:def 5;

 then

 A32: ( In (SS1,( Fin SS1))) = SS1 by SUBSET_1:def 8;

 reconsider SSX = (SS1 \ X) as Element of ( Fin SS1) by FINSUB_1:def 5;



 A33: (X \/ SSX) = (SS1 \/ X) by XBOOLE_1: 39;

 X c= SS1 by FINSUB_1:def 5;

 then

 A34: (X \/ SSX) = SS1 by A33, XBOOLE_1: 12;

 consider f be Function of SS2, SS1 such that

 A35: ( rng f) = (SS1 \ X) and

 A36: f is one-to-one and

 A37: for k, m st k < m & {k, m} in SS2 holds (m = i & k = i & k >= i implies (f . {k, m}) = {(k + 1), (m + 1)}) by A1, A20, A30, Th10;

 set Pf = (PQ1 * f);



 A38: ( dom Pf) = SS2 by FUNCT_2:def 1;



 A39: ( dom Q19) = ( Seg (n1 + 2)) by FUNCT_2: 52;

 A40:

 now

 n <= (n + 1) by NAT_1: 11;

 then

 A41: ( Seg (n2 + 2)) c= ( Seg (n1 + 2)) by FINSEQ_1: 5;

 let x be object such that

 A42: x in SS2;

 consider k,m be Nat such that

 A43: k in ( Seg (n2 + 2)) and

 A44: m in ( Seg (n2 + 2)) and

 A45: k < m and

 A46: x = {k, m} by A42, MATRIX11: 1;

 reconsider k, m as Element of NAT by ORDINAL1:def 12;

 ( dom Q9) = ( Seg (n2 + 2)) by FUNCT_2: 52;

 then (Q9 . k) <> (Q . m) by A43, A44, A45, FUNCT_1:def 4;

 then

 A47: (Q . k) > (Q . m) or (Q . k) < (Q . m) by XXREAL_0: 1;

 set m1 = (m + 1);

 set k1 = (k + 1);



 A48: ((n2 + 2) + 1) = (n1 + 2);

 then

 A49: k1 in ( Seg (n1 + 2)) by A43, FINSEQ_1: 60;



 A50: m1 in ( Seg (n1 + 2)) by A44, A48, FINSEQ_1: 60;

 per cases ;

 suppose

 A51: k < i & m < i;



 A52: (Pf . x) = (PQ1 . (f . x)) by A38, A42, FUNCT_1: 12;



 A53: (f . x) = x by A37, A42, A45, A46, A51;

 per cases ;

 suppose (Q1 . k) < j & (Q1 . m) < j or (Q1 . k) >= j & (Q1 . m) >= j;

 then (Q . k) = (Q1 . k) & (Q . m) = (Q1 . m) or (Q . k) = ((Q1 . k) - 1) & (Q . m) = ((Q1 . m) - 1) by A1, A2, A43, A44, A51, Def3;

 then (Q . k) < (Q . m) & (Q1 . k) < (Q1 . m) or (Q . k) > (Q . m) & (Q1 . k) > (Q1 . m) by A47, XREAL_1: 9;

 then (PQ1 . x) = ( 1_ K) & (PQ . x) = ( 1_ K) or (PQ1 . x) = ( - ( 1_ K)) & (PQ . x) = ( - ( 1_ K)) by A43, A44, A45, A46, A41, MATRIX11:def 1;

 hence (Pf . x) = (PQ . x) by A38, A42, A53, FUNCT_1: 12;

 end;

 suppose

 A54: (Q1 . k) < j & (Q1 . m) >= j;

 then (Q . m) = ((Q1 . m) - 1) by A1, A2, A44, A51, Def3;

 then

 A55: (Q1 . m) = ((Q . m) + 1);

 (Q19 . m) <> j by A1, A2, A39, A44, A41, A51, FUNCT_1:def 4;

 then (Q1 . m) > j by A54, XXREAL_0: 1;

 then

 A56: (Q . m) >= j by A55, NAT_1: 13;

 (Q1 . k) < (Q1 . m) by A54, XXREAL_0: 2;

 then

 A57: (PQ1 . x) = ( 1_ K) by A43, A44, A45, A46, A41, MATRIX11:def 1;

 (Q1 . k) = (Q . k) by A1, A2, A43, A51, A54, Def3;

 then (Q . k) < (Q . m) by A54, A56, XXREAL_0: 2;

 hence (Pf . x) = (PQ . x) by A43, A44, A45, A46, A53, A52, A57, MATRIX11:def 1;

 end;

 suppose

 A58: (Q1 . k) >= j & (Q1 . m) < j;

 then (Q . k) = ((Q1 . k) - 1) by A1, A2, A43, A51, Def3;

 then

 A59: (Q1 . k) = ((Q . k) + 1);

 (Q19 . k) <> j by A1, A2, A39, A43, A41, A51, FUNCT_1:def 4;

 then (Q1 . k) > j by A58, XXREAL_0: 1;

 then

 A60: (Q . k) >= j by A59, NAT_1: 13;

 (Q1 . k) > (Q1 . m) by A58, XXREAL_0: 2;

 then

 A61: (PQ1 . x) = ( - ( 1_ K)) by A43, A44, A45, A46, A41, MATRIX11:def 1;

 (Q1 . m) = (Q . m) by A1, A2, A44, A51, A58, Def3;

 then (Q . k) > (Q . m) by A58, A60, XXREAL_0: 2;

 hence (Pf . x) = (PQ . x) by A43, A44, A45, A46, A53, A52, A61, MATRIX11:def 1;

 end;

 end;

 suppose k >= i & m < i;

 hence (Pf . x) = (PQ . x) by A45, XXREAL_0: 2;

 end;

 suppose

 A62: k = i;



 A63: (Pf . x) = (PQ1 . (f . {k, m})) by A38, A42, A46, FUNCT_1: 12;



 A64: (f . {k, m}) = {k, m1} by A37, A42, A45, A46, A62;

 per cases ;

 suppose (Q1 . k) < j & (Q1 . m1) < j or (Q1 . k) >= j & (Q1 . m1) >= j;

 then (Q . k) = (Q1 . k) & (Q . m) = (Q1 . m1) or (Q . k) = ((Q1 . k) - 1) & (Q . m) = ((Q1 . m1) - 1) by A1, A2, A43, A44, A62, Def3;

 then

 A65: (Q . k) < (Q . m) & (Q1 . k) < (Q1 . m1) or (Q . k) > (Q . m) & (Q1 . k) > (Q1 . m1) by A47, XREAL_1: 9;

 k < m1 by A45, NAT_1: 13;

 then (PQ1 . {k, m1}) = ( 1_ K) & (PQ . x) = ( 1_ K) or (PQ1 . {k, m1}) = ( - ( 1_ K)) & (PQ . x) = ( - ( 1_ K)) by A43, A44, A45, A46, A41, A50, A65, MATRIX11:def 1;

 hence (Pf . x) = (PQ . x) by A38, A42, A46, A64, FUNCT_1: 12;

 end;

 suppose

 A66: (Q1 . k) < j & (Q1 . m1) >= j;

 m1 > i by A62, NAT_1: 13;

 then (Q19 . m1) <> j by A1, A2, A39, A50, FUNCT_1:def 4;

 then

 A67: (Q1 . m1) > j by A66, XXREAL_0: 1;

 (Q . m) = ((Q1 . m1) - 1) by A1, A2, A44, A62, A66, Def3;

 then (Q1 . m1) = ((Q . m) + 1);

 then

 A68: (Q . m) >= j by A67, NAT_1: 13;

 (Q1 . k) = (Q . k) by A1, A2, A43, A62, A66, Def3;

 then

 A69: (Q . k) < (Q . m) by A66, A68, XXREAL_0: 2;



 A70: k < m1 by A45, NAT_1: 13;

 (Q1 . k) < (Q1 . m1) by A66, XXREAL_0: 2;

 then (PQ1 . {k, m1}) = ( 1_ K) by A43, A41, A50, A70, MATRIX11:def 1;

 hence (Pf . x) = (PQ . x) by A43, A44, A45, A46, A64, A63, A69, MATRIX11:def 1;

 end;

 suppose

 A71: (Q1 . k) >= j & (Q1 . m1) < j;

 then (Q . k) = ((Q1 . k) - 1) by A1, A2, A43, A62, Def3;

 then

 A72: (Q1 . k) = ((Q . k) + 1);

 (Q19 . k) <> j by A1, A2, A39, A43, A41, A62, FUNCT_1:def 4;

 then (Q1 . k) > j by A71, XXREAL_0: 1;

 then

 A73: (Q . k) >= j by A72, NAT_1: 13;

 (Q1 . m1) = (Q . m) by A1, A2, A44, A62, A71, Def3;

 then

 A74: (Q . m) < (Q . k) by A71, A73, XXREAL_0: 2;



 A75: k < m1 by A45, NAT_1: 13;

 (Q1 . k) > (Q1 . m1) by A71, XXREAL_0: 2;

 then (PQ1 . {k, m1}) = ( - ( 1_ K)) by A43, A41, A50, A75, MATRIX11:def 1;

 hence (Pf . x) = (PQ . x) by A43, A44, A45, A46, A64, A63, A74, MATRIX11:def 1;

 end;

 end;

 suppose

 A76: k >= i & m >= i;



 A77: (Pf . x) = (PQ1 . (f . {k, m})) by A38, A42, A46, FUNCT_1: 12;



 A78: k1 < m1 by A45, XREAL_1: 6;



 A79: (f . {k, m}) = {(k + 1), (m + 1)} by A37, A42, A45, A46, A76;

 per cases ;

 suppose (Q1 . k1) < j & (Q1 . m1) < j or (Q1 . k1) >= j & (Q1 . m1) >= j;

 then (Q . k) = (Q1 . k1) & (Q . m) = (Q1 . m1) or (Q . k) = ((Q1 . k1) - 1) & (Q . m) = ((Q1 . m1) - 1) by A1, A2, A43, A44, A76, Def3;

 then (Q . k) < (Q . m) & (Q1 . k1) < (Q1 . m1) or (Q . k) > (Q . m) & (Q1 . k1) > (Q1 . m1) by A47, XREAL_1: 9;

 then (PQ1 . {k1, m1}) = ( 1_ K) & (PQ . x) = ( 1_ K) or (PQ1 . {m1, k1}) = ( - ( 1_ K)) & (PQ . x) = ( - ( 1_ K)) by A43, A44, A45, A46, A49, A50, A78, MATRIX11:def 1;

 hence (Pf . x) = (PQ . x) by A38, A42, A46, A79, FUNCT_1: 12;

 end;

 suppose

 A80: (Q1 . k1) < j & (Q1 . m1) >= j;

 m1 > i by A76, NAT_1: 13;

 then (Q19 . m1) <> j by A1, A2, A39, A50, FUNCT_1:def 4;

 then

 A81: (Q1 . m1) > j by A80, XXREAL_0: 1;

 (Q . m) = ((Q1 . m1) - 1) by A1, A2, A44, A76, A80, Def3;

 then (Q1 . m1) = ((Q . m) + 1);

 then

 A82: (Q . m) >= j by A81, NAT_1: 13;

 (Q1 . k1) < (Q1 . m1) by A80, XXREAL_0: 2;

 then

 A83: (PQ1 . {k1, m1}) = ( 1_ K) by A49, A50, A78, MATRIX11:def 1;

 (Q1 . k1) = (Q . k) by A1, A2, A43, A76, A80, Def3;

 then (Q . k) < (Q . m) by A80, A82, XXREAL_0: 2;

 hence (Pf . x) = (PQ . x) by A43, A44, A45, A46, A79, A77, A83, MATRIX11:def 1;

 end;

 suppose

 A84: (Q1 . k1) >= j & (Q1 . m1) < j;

 k1 > i by A76, NAT_1: 13;

 then (Q19 . k1) <> j by A1, A2, A39, A49, FUNCT_1:def 4;

 then

 A85: (Q1 . k1) > j by A84, XXREAL_0: 1;

 (Q . k) = ((Q1 . k1) - 1) by A1, A2, A43, A76, A84, Def3;

 then (Q1 . k1) = ((Q . k) + 1);

 then

 A86: (Q . k) >= j by A85, NAT_1: 13;

 (Q1 . k1) > (Q1 . m1) by A84, XXREAL_0: 2;

 then

 A87: (PQ1 . {k1, m1}) = ( - ( 1_ K)) by A49, A50, A78, MATRIX11:def 1;

 (Q1 . m1) = (Q . m) by A1, A2, A44, A76, A84, Def3;

 then (Q . k) > (Q . m) by A84, A86, XXREAL_0: 2;

 hence (Pf . x) = (PQ . x) by A43, A44, A45, A46, A79, A77, A87, MATRIX11:def 1;

 end;

 end;

 end;

 reconsider domf = ( dom f) as Element of ( Fin SS2) by FINSUB_1:def 5;



 A88: (f .: domf) = ( rng f) by RELAT_1: 113;

 ( dom f) = SS2 by FUNCT_2:def 1;

 then

 A89: domf = ( In (SS2,( Fin SS2))) by SUBSET_1:def 8;

 ( dom PQ) = SS2 by FUNCT_2:def 1;

 then PQ = Pf by A38, A40, FUNCT_1: 2;

 then

 A90: (mm $$ (SSX,PQ1)) = ( sgn (Q,K)) by A35, A36, A89, A88, SETWOP_2: 6;

 X misses SSX by XBOOLE_1: 79;

 then ( sgn (Q1,K)) = ((( power K) . (( - ( 1_ K)),(i + j))) * ( sgn (Q,K))) by A31, A90, A34, A32, SETWOP_2: 4;



 hence ( - (a,p1)) = (((( power K) . (( - ( 1_ K)),(i + j))) * ( sgn (Q,K))) * a) by MATRIX11: 26

 .= ((( power K) . (( - ( 1_ K)),(i + j))) * (( sgn (Q,K)) * a)) by GROUP_1:def 3

 .= ((( power K) . (( - ( 1_ K)),(i + j))) * ( - (a,R))) by MATRIX11: 26;

 end;

 end;

 end;

 theorem :: LAPLACE:22



 Th22: for i, j st i in ( Seg (n + 1)) & (p1 . i) = j holds for M be Matrix of (n + 1), K holds for DM be Matrix of n, K st DM = ( Delete (M,i,j)) holds (( Path_product M) . p1) = (((( power K) . (( - ( 1_ K)),(i + j))) * (M * (i,j))) * (( Path_product DM) . ( Rem (p1,i))))

 proof

 reconsider N = n as Element of NAT by ORDINAL1:def 12;

 set n1 = (N + 1);

 let i,j be Nat such that

 A1: i in ( Seg (n + 1)) and

 A2: (p1 . i) = j;

 set mm = the multF of K;

 set R = ( Rem (p1,i));

 let M be Matrix of (n + 1), K, DM be Matrix of n, K such that

 A3: DM = ( Delete (M,i,j));

 set PR = ( Path_matrix (R,DM));

 set Pp1 = ( Path_matrix (p1,M));

 ( len Pp1) = n1 by MATRIX_3:def 7;

 then ( dom Pp1) = ( Seg n1) by FINSEQ_1:def 3;

 then

 A4: (Pp1 . i) = (M * (i,j)) by A1, A2, MATRIX_3:def 7;

 A5:

 now

 per cases ;

 suppose

 A6: N = 0 ;

 then

 A7: ( len Pp1) = 1 by MATRIX_3:def 7;

 (Pp1 . 1) = (M * (i,j)) by A1, A4, A6, FINSEQ_1: 2, TARSKI:def 1;

 then Pp1 = <*(M * (i,j))*> by A7, FINSEQ_1: 40;

 then

 A8: (mm $$ Pp1) = (M * (i,j)) by FINSOP_1: 11;

 ( len PR) = 0 by A6, MATRIX_3:def 7;

 then PR = ( <*> the carrier of K);

 then

 A9: (mm $$ PR) = ( the_unity_wrt mm) by FINSOP_1: 10;

 ( the_unity_wrt mm) = ( 1_ K) by FVSUM_1: 5;

 hence (mm $$ Pp1) = ((M * (i,j)) * (mm $$ PR)) by A8, A9;

 end;

 suppose

 A10: N > 0 ;

 ( len PR) = n by MATRIX_3:def 7;

 then

 consider f be sequence of the carrier of K such that

 A11: (f . 1) = (PR . 1) and

 A12: for k be Nat st 0 <> k & k < n holds (f . (k + 1)) = (mm . ((f . k),(PR . (k + 1)))) and

 A13: (mm $$ PR) = (f . n) by A10, FINSOP_1:def 1;

 ( len Pp1) = n1 by MATRIX_3:def 7;

 then

 consider F be sequence of the carrier of K such that

 A14: (F . 1) = (Pp1 . 1) and

 A15: for k be Nat st 0 <> k & k < n1 holds (F . (k + 1)) = (mm . ((F . k),(Pp1 . (k + 1)))) and

 A16: (mm $$ Pp1) = (F . n1) by FINSOP_1:def 1;

 defpred P[ Nat] means 1 <= $1 & $1 = i implies (PR . k) = (Pp1 . (k + 1)))

 proof

 ( len Pp1) = n1 by MATRIX_3:def 7;

 then

 A18: ( dom Pp1) = ( Seg n1) by FINSEQ_1:def 3;

 ( len PR) = n by MATRIX_3:def 7;

 then

 A19: ( dom PR) = ( Seg n) by FINSEQ_1:def 3;

 reconsider p19 = p1 as Permutation of ( Seg n1) by MATRIX_1:def 12;

 reconsider R9 = R as Permutation of ( Seg n) by MATRIX_1:def 12;

 let k such that

 A20: k in ( Seg n);

 reconsider k1 = (k + 1) as Element of NAT ;



 A21: k1 in ( Seg n1) by A20, FINSEQ_1: 60;



 A22: ( rng p19) = ( Seg n1) by FUNCT_2:def 3;

 ( dom p19) = ( Seg n1) by FUNCT_2: 52;

 then

 A23: j in ( Seg n1) by A1, A2, A22, FUNCT_1:def 3;



 A24: ( rng R9) = ( Seg n) by FUNCT_2:def 3;

 ( dom R9) = ( Seg n) by FUNCT_2: 52;

 then

 A25: (R . k) in ( Seg n) by A20, A24, FUNCT_1:def 3;

 then

 consider Rk be Nat such that

 A26: Rk = (R . k) and 1 <= Rk and Rk <= n;



 A27: (n1 -' 1) = (n1 - 1) by XREAL_0:def 2;

 n <= n1 by NAT_1: 11;

 then

 A28: ( Seg n) c= ( Seg n1) by FINSEQ_1: 5;

 thus k (p19 . i) by A1, A20, A28, A29, FUNCT_1:def 4;

 then (p1 . k) < j or (p1 . k) > j by A2, XXREAL_0: 1;

 then Rk = (p1 . k) & (p1 . k) < j or (p1 . k) > j & Rk = ((p1 . k) - 1) by A1, A2, A20, A26, A29, Def3;

 then Rk = (p1 . k) & (p1 . k) < j or (p1 . k) > j & (p1 . k) = (Rk + 1);

 then Rk = (p1 . k) & (p1 . k) < j or (p1 . k) > j & Rk >= j & (p1 . k) = (Rk + 1) by NAT_1: 13;

 then (DM * (k,Rk)) = (M * (k,Rk)) & (PR . k) = (DM * (k,Rk)) & (Pp1 . k) = (M * (k,Rk)) or (PR . k) = (DM * (k,Rk)) & (DM * (k,Rk)) = (M * (k,(Rk + 1))) & (Pp1 . k) = (M * (k,(Rk + 1))) by A1, A3, A20, A25, A23, A26, A28, A27, A19, A18, A29, Th13, MATRIX_3:def 7;

 hence thesis;

 end;



 A30: ( dom p19) = ( Seg n1) by FUNCT_2: 52;

 assume

 A31: k >= i;

 then k1 > i by NAT_1: 13;

 then (p19 . k1) <> (p19 . i) by A1, A21, A30, FUNCT_1:def 4;

 then (p1 . k1) < j or (p1 . k1) > j by A2, XXREAL_0: 1;

 then Rk = (p1 . k1) & (p1 . k1) < j or (p1 . k1) > j & Rk = ((p1 . k1) - 1) by A1, A2, A20, A26, A31, Def3;

 then Rk = (p1 . k1) & (p1 . k1) < j or (p1 . k1) > j & (p1 . k1) = (Rk + 1);

 then Rk = (p1 . k1) & (p1 . k1) < j or (p1 . k1) > j & Rk >= j & (p1 . k1) = (Rk + 1) by NAT_1: 13;

 then (DM * (k,Rk)) = (M * ((k + 1),Rk)) & (PR . k) = (DM * (k,Rk)) & (Pp1 . k1) = (M * ((k + 1),Rk)) or (PR . k) = (DM * (k,Rk)) & (DM * (k,Rk)) = (M * ((k + 1),(Rk + 1))) & (Pp1 . k1) = (M * (k1,(Rk + 1))) by A1, A3, A20, A25, A23, A26, A27, A21, A19, A18, A31, Th13, MATRIX_3:def 7;

 hence thesis;

 end;



 A32: for k st P[k] holds P[(k + 1)]

 proof

 let k such that

 A33: P[k];

 reconsider e = k as Element of NAT by ORDINAL1:def 12;

 assume that

 A34: 1 <= (k + 1) and

 A35: (k + 1) < i;

 set k1 = (e + 1);

 i <= n1 by A1, FINSEQ_1: 1;

 then k1 < n1 by A35, XXREAL_0: 2;

 then k1 <= n by NAT_1: 13;

 then

 A36: k1 in ( Seg N) by A34;

 per cases by NAT_1: 14;

 suppose k = 0 ;

 hence thesis by A14, A11, A17, A35, A36;

 end;

 suppose

 A37: k >= 1;

 i <= n1 by A1, FINSEQ_1: 1;

 then

 A38: k1 < n1 by A35, XXREAL_0: 2;

 then k < n1 by NAT_1: 13;

 then

 A39: (F . k1) = (mm . ((F . k),(Pp1 . k1))) by A15, A37;

 k1 <= n by A38, NAT_1: 13;

 then

 A40: k1 in ( Seg N) by A34;

 k < n by A38, XREAL_1: 6;

 then (f . k1) = (mm . ((f . k),(PR . k1))) by A12, A37;

 hence thesis by A17, A33, A35, A37, A39, A40, NAT_1: 13;

 end;

 end;

 defpred Q[ Nat] means i <= $1 & $1 <= n1 implies ($1 = 1 implies (F . $1) = (M * (i,j))) & ($1 > 1 implies for a st a = (f . ($1 - 1)) holds (F . $1) = ((M * (i,j)) * a));



 A41: P[ 0 ];



 A42: for k holds P[k] from NAT_1:sch 2( A41, A32);



 A43: for k st Q[k] holds Q[(k + 1)]

 proof

 let k such that

 A44: Q[k];

 set k1 = (k + 1);

 assume that

 A45: i <= k1 and

 A46: k1 <= n1;

 per cases ;

 suppose

 A47: k = 0 ;

 1 <= i by A1, FINSEQ_1: 1;

 hence thesis by A4, A14, A45, A47, XXREAL_0: 1;

 end;

 suppose

 A48: k > 0 ;

 hence k1 = 1 implies (F . k1) = (M * (i,j));

 assume k1 > 1;

 let a such that

 A49: a = (f . (k1 - 1));



 A50: k <= n by A46, XREAL_1: 6;

 k >= 1 by A48, NAT_1: 14;

 then

 A51: k in ( Seg n) by A50;

 ( len PR) = n by MATRIX_3:def 7;

 then

 A52: ( dom PR) = ( Seg n) by FINSEQ_1:def 3;

 then

 A53: (PR . k) = (DM * (k,(R . k))) by A51, MATRIX_3:def 7;

 k < n1 by A46, NAT_1: 13;

 then

 A54: (F . k1) = (mm . ((F . k),(Pp1 . k1))) by A15, A48;

 per cases by A45, XXREAL_0: 1;

 suppose

 A55: k1 = i;

 then k < i by NAT_1: 13;

 then (F . k1) = (a * (M * (i,j))) by A4, A42, A48, A49, A54, A55, NAT_1: 14;

 hence thesis;

 end;

 suppose

 A56: k1 > i;



 A57: k < n1 by A46, NAT_1: 13;



 A58: k >= i by A56, NAT_1: 13;

 i >= 1 by A1, FINSEQ_1: 1;

 then

 A59: k >= 1 by A58, XXREAL_0: 2;

 per cases by A59, XXREAL_0: 1;

 suppose k = 1;

 hence thesis by A11, A17, A44, A46, A49, A51, A54, A58, NAT_1: 13;

 end;

 suppose

 A60: k > 1;

 reconsider k9 = (k - 1) as Element of NAT by A48, NAT_1: 20;

 reconsider fk9 = (f . k9) as Element of K;

 (k9 + 1) <= n by A57, NAT_1: 13;

 then

 A61: k9 < n by NAT_1: 13;

 (k9 + 1) > ( 0 + 1) by A60;

 then

 A62: a = (mm . (fk9,(PR . (k9 + 1)))) by A12, A49, A61;

 (F . k) = ((M * (i,j)) * fk9) by A44, A46, A56, A60, NAT_1: 13;



 hence (F . k1) = (((M * (i,j)) * fk9) * (DM * (k,(R . k)))) by A17, A51, A54, A53, A58

 .= ((M * (i,j)) * (fk9 * (DM * (k,(R . k))))) by GROUP_1:def 3

 .= ((M * (i,j)) * a) by A51, A52, A62, MATRIX_3:def 7;

 end;

 end;

 end;

 end;



 A63: Q[ 0 ];



 A64: for k holds Q[k] from NAT_1:sch 2( A63, A43);



 A65: i <= n1 by A1, FINSEQ_1: 1;



 A66: (n1 - 1) = n;

 n1 > ( 0 + 1) by A10, XREAL_1: 6;

 hence (mm $$ Pp1) = ((M * (i,j)) * (mm $$ PR)) by A16, A13, A64, A65, A66;

 end;

 end;

 per cases ;

 suppose

 A67: R is even;



 thus (( Path_product M) . p1) = ( - ((mm $$ Pp1),p1)) by MATRIX_3:def 8

 .= ((( power K) . (( - ( 1_ K)),(i + j))) * ( - ((mm $$ Pp1),R))) by A1, A2, Th21

 .= ((( power K) . (( - ( 1_ K)),(i + j))) * ((M * (i,j)) * (mm $$ PR))) by A5, A67, MATRIX_1:def 16

 .= (((( power K) . (( - ( 1_ K)),(i + j))) * (M * (i,j))) * (mm $$ PR)) by GROUP_1:def 3

 .= (((( power K) . (( - ( 1_ K)),(i + j))) * (M * (i,j))) * ( - ((mm $$ PR),R))) by A67, MATRIX_1:def 16

 .= (((( power K) . (( - ( 1_ K)),(i + j))) * (M * (i,j))) * (( Path_product DM) . R)) by MATRIX_3:def 8;

 end;

 suppose

 A68: R is odd;



 thus (( Path_product M) . p1) = ( - ((mm $$ Pp1),p1)) by MATRIX_3:def 8

 .= ((( power K) . (( - ( 1_ K)),(i + j))) * ( - ((mm $$ Pp1),R))) by A1, A2, Th21

 .= ((( power K) . (( - ( 1_ K)),(i + j))) * ( - ((M * (i,j)) * (mm $$ PR)))) by A5, A68, MATRIX_1:def 16

 .= ((( power K) . (( - ( 1_ K)),(i + j))) * ((M * (i,j)) * ( - (mm $$ PR)))) by VECTSP_1: 8

 .= (((( power K) . (( - ( 1_ K)),(i + j))) * (M * (i,j))) * ( - (mm $$ PR))) by GROUP_1:def 3

 .= (((( power K) . (( - ( 1_ K)),(i + j))) * (M * (i,j))) * ( - ((mm $$ PR),R))) by A68, MATRIX_1:def 16

 .= (((( power K) . (( - ( 1_ K)),(i + j))) * (M * (i,j))) * (( Path_product DM) . R)) by MATRIX_3:def 8;

 end;

 end;

 begin

 definition

 let i,j,n be Nat;

 let K;

 let M be Matrix of n, K;

 :: LAPLACE:def4

 func Minor (M,i,j) -> Element of K equals ( Det ( Delete (M,i,j)));

 coherence ;

 end

 definition

 let i,j,n be Nat;

 let K;

 let M be Matrix of n, K;

 :: LAPLACE:def5

 func Cofactor (M,i,j) -> Element of K equals ((( power K) . (( - ( 1_ K)),(i + j))) * ( Minor (M,i,j)));

 coherence ;

 end

 theorem :: LAPLACE:23



 Th23: for i, j st i in ( Seg n) & j in ( Seg n) holds for P be Element of ( Fin ( Permutations n)) st P = { p : (p . i) = j } holds for M be Matrix of n, K holds (the addF of K $$ (P,( Path_product M))) = ((M * (i,j)) * ( Cofactor (M,i,j)))

 proof

 let i,j be Nat such that

 A1: i in ( Seg n) and

 A2: j in ( Seg n);

 n > 0 by A1;

 then

 reconsider n9 = (n - 1) as Element of NAT by NAT_1: 20;

 set P = ( Permutations (n -' 1));

 set n91 = (n9 + 1);

 set P1 = ( Permutations n);



 A3: (n91 -' 1) = ((n9 + 1) - 1) by XREAL_0:def 2;

 set aa = the addF of K;

 P in ( Fin P) by FINSUB_1:def 5;

 then

 A4: ( In (P,( Fin P))) = P by SUBSET_1:def 8;

 let PP be Element of ( Fin P1) such that

 A5: PP = { p : (p . i) = j };

 consider Proj be Function of PP, P such that

 A6: Proj is bijective and

 A7: for q be Element of ( Permutations n91) st (q . i) = j holds (Proj . q) = ( Rem (q,i)) by A1, A2, A5, A3, Th20;

 let M be Matrix of n, K;

 set DM = ( Delete (M,i,j));

 set PathM = ( Path_product M);

 set PathDM = ( Path_product DM);

 set pm = ((( power K) . (( - ( 1_ K)),(i + j))) * (M * (i,j)));

 defpred P[ set] means for D be Element of ( Fin P1), ProjD be Element of ( Fin P) st D = $1 & ProjD = (Proj .: D) & D c= PP holds (aa $$ (D,PathM)) = (pm * (aa $$ (ProjD,PathDM)));



 A8: for B9 be Element of ( Fin P1), b be Element of P1 holds P[B9] & not b in B9 implies P[(B9 \/ {b})]

 proof

 let B9 be Element of ( Fin P1), b be Element of P1 such that

 A9: P[B9] and

 A10: not b in B9;



 A11: b in {b} by TARSKI:def 1;



 A12: ( rng Proj) = P by A6, FUNCT_2:def 3;

 then (Proj .: B9) c= P by RELAT_1: 111;

 then

 reconsider ProjB9 = (Proj .: B9) as Element of ( Fin P) by FINSUB_1:def 5;

 let D be Element of ( Fin P1), ProjD be Element of ( Fin P) such that

 A13: D = (B9 \/ {b}) and

 A14: ProjD = (Proj .: D) and

 A15: D c= PP;



 A16: B9 c= D by A13, XBOOLE_1: 7;

 B9 c= D by A13, XBOOLE_1: 7;

 then

 A17: B9 c= PP by A15;

 {b} c= D by A13, XBOOLE_1: 7;

 then

 A18: b in PP by A15, A11;

 then

 consider Q1 be Element of P1 such that

 A19: Q1 = b and

 A20: (Q1 . i) = j by A5;



 A21: ( dom Proj) = PP by FUNCT_2:def 1;

 then

 A22: ( Im (Proj,b)) = {(Proj . b)} by A18, FUNCT_1: 59;

 reconsider Q = (Proj . b) as Element of P by A18, A21, A12, FUNCT_1:def 3;



 A23: (Proj . b) in ( rng Proj) by A18, A21, FUNCT_1:def 3;

 reconsider Q19 = Q1 as Element of ( Permutations (n9 + 1));



 A24: ( Rem (Q19,i)) = Q by A7, A19, A20;

 then

 A25: (PathM . Q1) = (pm * (PathDM . Q)) by A1, A3, A20, Th22;



 A26: not Q in ProjB9

 proof

 assume Q in ProjB9;

 then ex x be object st x in ( dom Proj) & x in B9 & (Proj . x) = Q by FUNCT_1:def 6;

 hence thesis by A6, A10, A18, A21, FUNCT_1:def 4;

 end;

 per cases ;

 suppose

 A27: B9 = {} ;

 then

 A28: (aa $$ (D,PathM)) = (PathM . b) by A13, SETWISEO: 17;

 (aa $$ (ProjD,PathDM)) = (PathDM . (Proj . b)) by A13, A14, A22, A23, A12, A27, SETWISEO: 17;

 hence thesis by A1, A3, A19, A20, A24, A28, Th22;

 end;

 suppose

 A29: B9 <> {} ;

 ProjD = (ProjB9 \/ {Q}) by A13, A14, A22, RELAT_1: 120;



 hence (pm * (aa $$ (ProjD,PathDM))) = (pm * ((aa $$ (ProjB9,PathDM)) + (PathDM . Q))) by A18, A17, A21, A26, A29, SETWOP_2: 2

 .= ((pm * (aa $$ (ProjB9,PathDM))) + (pm * (PathDM . Q))) by VECTSP_1:def 2

 .= (aa . ((aa $$ (B9,PathM)),(PathM . b))) by A9, A15, A19, A16, A25, XBOOLE_1: 1

 .= (aa $$ (D,PathM)) by A10, A13, A29, SETWOP_2: 2;

 end;

 end;



 A30: P[( {}. P1)]

 proof

 let B be Element of ( Fin P1), ProjB be Element of ( Fin P) such that

 A31: B = ( {}. P1) and

 A32: ProjB = (Proj .: B) and B c= PP;

 ProjB = ( {}. P) by A31, A32;

 then

 A33: (aa $$ (ProjB,PathDM)) = ( the_unity_wrt aa) by FVSUM_1: 8, SETWISEO: 31;



 A34: ( the_unity_wrt aa) = ( 0. K) by FVSUM_1: 7;

 (aa $$ (B,PathM)) = ( the_unity_wrt aa) by A31, FVSUM_1: 8, SETWISEO: 31;

 hence thesis by A33, A34;

 end;



 A35: for B be Element of ( Fin P1) holds P[B] from SETWISEO:sch 2( A30, A8);



 A36: ( dom Proj) = PP by FUNCT_2:def 1;

 ( rng Proj) = P by A6, FUNCT_2:def 3;

 then (Proj .: PP) = ( In (P,( Fin P))) by A4, A36, RELAT_1: 113;



 hence (aa $$ (PP,PathM)) = (((M * (i,j)) * (( power K) . (( - ( 1_ K)),(i + j)))) * ( Det ( Delete (M,i,j)))) by A35

 .= ((M * (i,j)) * ( Cofactor (M,i,j))) by GROUP_1:def 3;

 end;

 theorem :: LAPLACE:24



 Th24: for i, j st i in ( Seg n) & j in ( Seg n) holds ( Minor (M,i,j)) = ( Minor ((M @ ),j,i))

 proof

 let i, j such that

 A1: i in ( Seg n) and

 A2: j in ( Seg n);



 thus ( Minor (M,i,j)) = ( Det (( Delete (M,i,j)) @ )) by MATRIXR2: 43

 .= ( Minor ((M @ ),j,i)) by A1, A2, Th14;

 end;

 definition

 let n, K;

 let M be Matrix of n, K;

 :: LAPLACE:def6

 func Matrix_of_Cofactor (M) -> Matrix of n, K means

 : Def6: for i,j be Nat st [i, j] in ( Indices it ) holds (it * (i,j)) = ( Cofactor (M,i,j));

 existence

 proof

 reconsider N = n as Element of NAT by ORDINAL1:def 12;

 deffunc C( Nat, Nat) = ( Cofactor (M,$1,$2));

 ex M be Matrix of N, N, K st for i,j be Nat st [i, j] in ( Indices M) holds (M * (i,j)) = C(i,j) from MATRIX_0:sch 1;

 hence thesis;

 end;

 uniqueness

 proof

 let C1,C2 be Matrix of n, K such that

 A1: for i,j be Nat st [i, j] in ( Indices C1) holds (C1 * (i,j)) = ( Cofactor (M,i,j)) and

 A2: for i,j be Nat st [i, j] in ( Indices C2) holds (C2 * (i,j)) = ( Cofactor (M,i,j));

 now



 A3: ( Indices C1) = ( Indices C2) by MATRIX_0: 26;

 let i,j be Nat such that

 A4: [i, j] in ( Indices C1);

 reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 12;

 (C1 * (i,j)) = ( Cofactor (M,i9,j9)) by A1, A4;

 hence (C1 * (i,j)) = (C2 * (i,j)) by A2, A4, A3;

 end;

 hence thesis by MATRIX_0: 27;

 end;

 end

 begin

 definition

 let n, i, K;

 let M be Matrix of n, K;

 ::$Notion-Name

 :: LAPLACE:def7

 func LaplaceExpL (M,i) -> FinSequence of K means

 : Def7: ( len it ) = n & for j st j in ( dom it ) holds (it . j) = ((M * (i,j)) * ( Cofactor (M,i,j)));

 existence

 proof

 reconsider N = n as Element of NAT by ORDINAL1:def 12;

 deffunc L( Nat) = ((M * (i,$1)) * ( Cofactor (M,i,$1)));

 consider LL be FinSequence such that

 A1: ( len LL) = N & for k be Nat st k in ( dom LL) holds (LL . k) = L(k) from FINSEQ_1:sch 2;

 ( rng LL) c= the carrier of K

 proof

 let x be object;

 assume x in ( rng LL);

 then

 consider y be object such that

 A2: y in ( dom LL) and

 A3: (LL . y) = x by FUNCT_1:def 3;

 ( dom LL) = ( Seg n) by A1, FINSEQ_1:def 3;

 then

 consider k be Nat such that

 A4: k = y and 1 <= k and k <= n by A2;

 L(k) is Element of K;

 then (LL . k) is Element of K by A1, A2, A4;

 hence thesis by A3, A4;

 end;

 then

 reconsider LL as FinSequence of K by FINSEQ_1:def 4;

 take LL;

 thus ( len LL) = n by A1;

 thus thesis by A1;

 end;

 uniqueness

 proof

 let L1,L2 be FinSequence of K such that

 A5: ( len L1) = n and

 A6: for j st j in ( dom L1) holds (L1 . j) = ((M * (i,j)) * ( Cofactor (M,i,j))) and

 A7: ( len L2) = n and

 A8: for j st j in ( dom L2) holds (L2 . j) = ((M * (i,j)) * ( Cofactor (M,i,j)));



 A9: ( dom L2) = ( Seg n) by A7, FINSEQ_1:def 3;



 A10: ( dom L1) = ( Seg n) by A5, FINSEQ_1:def 3;

 now

 let k be Nat such that

 A11: k in ( dom L1);

 (L1 . k) = ((M * (i,k)) * ( Cofactor (M,i,k))) by A6, A11;

 hence (L1 . k) = (L2 . k) by A8, A10, A9, A11;

 end;

 hence thesis by A10, A9, FINSEQ_1: 13;

 end;

 end

 definition

 let n;

 let j be Nat, K;

 let M be Matrix of n, K;

 :: LAPLACE:def8

 func LaplaceExpC (M,j) -> FinSequence of K means

 : Def8: ( len it ) = n & for i st i in ( dom it ) holds (it . i) = ((M * (i,j)) * ( Cofactor (M,i,j)));

 existence

 proof

 reconsider N = n as Element of NAT by ORDINAL1:def 12;

 deffunc L( Nat) = ((M * ($1,j)) * ( Cofactor (M,$1,j)));

 consider LL be FinSequence such that

 A1: ( len LL) = N & for k be Nat st k in ( dom LL) holds (LL . k) = L(k) from FINSEQ_1:sch 2;

 ( rng LL) c= the carrier of K

 proof

 let x be object;

 assume x in ( rng LL);

 then

 consider y be object such that

 A2: y in ( dom LL) and

 A3: (LL . y) = x by FUNCT_1:def 3;

 ( dom LL) = ( Seg n) by A1, FINSEQ_1:def 3;

 then

 consider k be Nat such that

 A4: k = y and 1 <= k and k <= n by A2;

 L(k) is Element of K;

 then (LL . k) is Element of K by A1, A2, A4;

 hence thesis by A3, A4;

 end;

 then

 reconsider LL as FinSequence of K by FINSEQ_1:def 4;

 take LL;

 thus ( len LL) = n by A1;

 let i;

 assume i in ( dom LL);

 hence thesis by A1;

 end;

 uniqueness

 proof

 let L1,L2 be FinSequence of K such that

 A5: ( len L1) = n and

 A6: for i st i in ( dom L1) holds (L1 . i) = ((M * (i,j)) * ( Cofactor (M,i,j))) and

 A7: ( len L2) = n and

 A8: for i st i in ( dom L2) holds (L2 . i) = ((M * (i,j)) * ( Cofactor (M,i,j)));



 A9: ( dom L2) = ( Seg n) by A7, FINSEQ_1:def 3;



 A10: ( dom L1) = ( Seg n) by A5, FINSEQ_1:def 3;

 now

 let k be Nat such that

 A11: k in ( dom L1);

 (L1 . k) = ((M * (k,j)) * ( Cofactor (M,k,j))) by A6, A11;

 hence (L1 . k) = (L2 . k) by A8, A10, A9, A11;

 end;

 hence thesis by A10, A9, FINSEQ_1: 13;

 end;

 end

 theorem :: LAPLACE:25



 Th25: for i be Nat, M be Matrix of n, K st i in ( Seg n) holds ( Det M) = ( Sum ( LaplaceExpL (M,i)))

 proof

 reconsider N = n as Element of NAT by ORDINAL1:def 12;

 set P = ( Permutations n);

 set KK = the carrier of K;

 set aa = the addF of K;



 A1: aa is having_a_unity by FVSUM_1: 8;

 let i be Nat, M be Matrix of n, K such that

 A2: i in ( Seg n);

 reconsider X = ( finSeg N) as non empty set by A2;

 set Path = ( Path_product M);

 deffunc G( Element of ( Fin P)) = (aa $$ ($1,Path));

 consider g be Function of ( Fin P), KK such that

 A3: for x be Element of ( Fin P) holds (g . x) = G(x) from FUNCT_2:sch 4;



 A4: for A,B be Element of ( Fin P) st A misses B holds (aa . ((g . A),(g . B))) = (g . (A \/ B))

 proof

 let A,B be Element of ( Fin P) such that

 A5: A misses B;



 A6: (g . A) = G(A) by A3;



 A7: (g . B) = G(B) by A3;

 (g . (A \/ B)) = G(\/) by A3;

 hence thesis by A5, A6, A7, FVSUM_1: 8, SETWOP_2: 4;

 end;

 deffunc F( object) = { p : (p . i) = $1 };

 consider f be Function such that

 A8: ( dom f) = X & for x be object st x in X holds (f . x) = F(x) from FUNCT_1:sch 3;

 ( rng f) c= ( Fin P)

 proof

 let x be object;

 assume x in ( rng f);

 then

 consider y be object such that

 A9: y in ( dom f) and

 A10: (f . y) = x by FUNCT_1:def 3;



 A11: F(y) c= P

 proof

 let z be object;

 assume z in F(y);

 then ex p st p = z & (p . i) = y;

 hence thesis;

 end;

 F(y) in ( Fin P) by A11, FINSUB_1:def 5;

 hence thesis by A8, A9, A10;

 end;

 then

 reconsider f as Function of X, ( Fin P) by A8, FUNCT_2: 2;



 A12: (g . ( In (P,( Fin P)))) = ( Det M) by A3;

 set gf = (g * f);



 A13: ( dom gf) = X by FUNCT_2:def 1;

 then

 A14: (gf * ( id X)) = gf by RELAT_1: 52;



 A15: P c= ( union (f .: X))

 proof

 let x be object;

 assume

 A16: x in P;

 then

 reconsider p = x as Permutation of X by MATRIX_1:def 12;



 A17: x in F(.) by A16;



 A18: ( rng p) = X by FUNCT_2:def 3;

 ( dom p) = X by FUNCT_2: 52;

 then

 A19: (p . i) in X by A2, A18, FUNCT_1:def 3;

 then

 A20: (f . (p . i)) in (f .: X) by A8, FUNCT_1:def 6;

 (f . (p . i)) = F(.) by A8, A19;

 hence thesis by A17, A20, TARSKI:def 4;

 end;

 set L = ( LaplaceExpL (M,i));

 ( len L) = n by Def7;

 then

 A21: ( dom L) = ( Seg n) by FINSEQ_1:def 3;

 then

 A22: ( dom ( id X)) = ( dom L);

 reconsider X9 = X as Element of ( Fin X) by FINSUB_1:def 5;

 P in ( Fin P) by FINSUB_1:def 5;

 then

 A23: ( In (P,( Fin P))) = P by SUBSET_1:def 8;

 (g . ( {}. ( Fin P))) = (aa $$ (( {}. P),Path)) by A3;

 then

 A24: (g . {} ) = ( the_unity_wrt aa) by FVSUM_1: 8, SETWISEO: 31;

 A25:

 now

 let x, y such that

 A26: x in X9 and

 A27: y in X9 and

 A28: (f . x) meets (f . y);

 consider z be object such that

 A29: z in (f . x) and

 A30: z in (f . y) by A28, XBOOLE_0: 3;

 (f . y) = F(y) by A8, A27;

 then

 A31: ex p st p = z & (p . i) = y by A30;

 (f . x) = F(x) by A8, A26;

 then ex p st p = z & (p . i) = x by A29;

 hence x = y by A31;

 end;

 now



 A32: ( rng f) c= ( Fin P) by RELAT_1:def 19;

 let x be object such that

 A33: x in ( dom gf);

 consider k be Nat such that

 A34: k = x and 1 <= k and k <= n by A13, A33;

 (f . k) in ( rng f) by A8, A33, A34, FUNCT_1:def 3;

 then

 reconsider Fk = F(k) as Element of ( Fin P) by A8, A33, A34, A32;



 A35: (f . k) = Fk by A8, A33, A34;

 (gf . k) = (g . (f . k)) by A8, A33, A34, FUNCT_1: 13;

 then

 A36: (gf . k) = G(Fk) by A3, A35;

 G(Fk) = ((M * (i,k)) * ( Cofactor (M,i,k))) by A2, A33, A34, Th23;

 hence (L . x) = (gf . x) by A21, A33, A34, A36, Def7;

 end;

 then

 A37: L = gf by A21, A13, FUNCT_1: 2;

 set Laa = ( [#] (L,( the_unity_wrt aa)));



 A38: ( rng ( id X)) = X9;



 A39: (Laa | ( dom L)) = L by SETWOP_2: 21;

 ( union (f .: X)) c= P

 proof

 let x be object;

 assume x in ( union (f .: X));

 then

 consider y be set such that

 A40: x in y and

 A41: y in (f .: X) by TARSKI:def 4;

 consider z be object such that

 A42: z in ( dom f) and z in X and

 A43: (f . z) = y by A41, FUNCT_1:def 6;

 y = F(z) by A8, A42, A43;

 then ex p st x = p & (p . i) = z by A40;

 hence thesis;

 end;

 then P = ( union (f .: X)) by A15, XBOOLE_0:def 10;

 then

 A44: (aa $$ ((f .: X9),g)) = (g . ( In (P,( Fin P)))) by A25, A4, A1, A24, A23, Th12;

 (aa $$ (X9,(g * f))) = (aa $$ ((f .: X9),g)) by A25, A4, A1, A24, Th12;



 hence ( Det M) = (aa $$ (( findom L),Laa)) by A22, A38, A39, A14, A37, A44, A12, SETWOP_2: 5

 .= ( Sum L) by FVSUM_1: 8, SETWOP_2:def 2;

 end;

 theorem :: LAPLACE:26



 Th26: for i st i in ( Seg n) holds ( LaplaceExpC (M,i)) = ( LaplaceExpL ((M @ ),i))

 proof

 let i such that

 A1: i in ( Seg n);

 set LL = ( LaplaceExpL ((M @ ),i));

 set LC = ( LaplaceExpC (M,i));

 reconsider I = i as Element of NAT by ORDINAL1:def 12;



 A2: ( len LL) = n by Def7;



 A3: ( len LC) = n by Def8;

 now

 let k be Nat such that

 A4: 1 <= k and

 A5: k <= n;



 A6: k in ( Seg n) by A4, A5;

 ( dom LC) = ( Seg n) by A3, FINSEQ_1:def 3;

 then

 A7: (LC . k) = ((M * (k,I)) * ( Cofactor (M,k,I))) by A6, Def8;

 ( Indices M) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

 then

 A8: [k, i] in ( Indices M) by A1, A6, ZFMISC_1: 87;

 ( dom LL) = ( Seg n) by A2, FINSEQ_1:def 3;

 then

 A9: (LL . k) = (((M @ ) * (I,k)) * ( Cofactor ((M @ ),I,k))) by A6, Def7;

 ( Cofactor (M,k,I)) = ( Cofactor ((M @ ),I,k)) by A1, A6, Th24;

 hence (LC . k) = (LL . k) by A8, A7, A9, MATRIX_0:def 6;

 end;

 hence thesis by A3, A2;

 end;

 theorem :: LAPLACE:27

 for j be Nat, M be Matrix of n, K st j in ( Seg n) holds ( Det M) = ( Sum ( LaplaceExpC (M,j)))

 proof

 let j be Nat, M be Matrix of n, K such that

 A1: j in ( Seg n);



 thus ( Det M) = ( Det (M @ )) by MATRIXR2: 43

 .= ( Sum ( LaplaceExpL ((M @ ),j))) by A1, Th25

 .= ( Sum ( LaplaceExpC (M,j))) by A1, Th26;

 end;

 theorem :: LAPLACE:28



 Th28: for p, i st ( len f) = n & i in ( Seg n) holds ( mlt (( Line (( Matrix_of_Cofactor M),i)),f)) = ( LaplaceExpL (( RLine (M,i,f)),i))

 proof

 let p, i such that

 A1: ( len f) = n and

 A2: i in ( Seg n);

 reconsider N = n as Element of NAT by ORDINAL1:def 12;

 set KK = the carrier of K;

 set C = ( Matrix_of_Cofactor M);

 reconsider Tp = f, TL = ( Line (C,i)) as Element of (N -tuples_on KK) by A1, FINSEQ_2: 92, MATRIX_0: 24;

 set R = ( RLine (M,i,f));

 set LL = ( LaplaceExpL (R,i));

 set MLT = ( mlt (TL,Tp));



 A3: ( len LL) = n by Def7;

 A4:

 now



 A5: ( dom LL) = ( Seg n) by A3, FINSEQ_1:def 3;



 A6: n = ( width M) by MATRIX_0: 24;

 let j be Nat such that

 A7: 1 <= j and

 A8: j <= n;



 A9: j in ( Seg n) by A7, A8;

 n = ( width C) by MATRIX_0: 24;

 then

 A10: (( Line (C,i)) . j) = (C * (i,j)) by A9, MATRIX_0:def 7;

 ( Indices M) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

 then [i, j] in ( Indices M) by A2, A9, ZFMISC_1: 87;

 then

 A11: (R * (i,j)) = (f . j) by A1, A6, MATRIX11:def 3;

 ( Indices C) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

 then [i, j] in ( Indices C) by A2, A9, ZFMISC_1: 87;

 then (( Line (C,i)) . j) = ( Cofactor (M,i,j)) by A10, Def6;

 then

 A12: (MLT . j) = (( Cofactor (M,i,j)) * (R * (i,j))) by A9, A11, FVSUM_1: 61;

 ( Cofactor (M,i,j)) = ( Cofactor (R,i,j)) by A2, A9, Th15;

 hence (MLT . j) = (LL . j) by A9, A5, A12, Def7;

 end;

 ( len MLT) = n by CARD_1:def 7;

 hence thesis by A3, A4;

 end;

 theorem :: LAPLACE:29



 Th29: i in ( Seg n) implies (( Line (M,j)) "*" ( Col ((( Matrix_of_Cofactor M) @ ),i))) = ( Det ( RLine (M,i,( Line (M,j)))))

 proof

 assume

 A1: i in ( Seg n);

 set C = ( Matrix_of_Cofactor M);

 ( len C) = n by MATRIX_0: 24;

 then ( dom C) = ( Seg n) by FINSEQ_1:def 3;

 then

 A2: ( Line (C,i)) = ( Col ((C @ ),i)) by A1, MATRIX_0: 58;

 ( width M) = n by MATRIX_0: 24;

 then

 A3: ( len ( Line (M,j))) = n by MATRIX_0:def 7;



 thus ( Det ( RLine (M,i,( Line (M,j))))) = ( Sum ( LaplaceExpL (( RLine (M,i,( Line (M,j)))),i))) by A1, Th25

 .= ( Sum ( mlt (( Col ((C @ ),i)),( Line (M,j))))) by A1, A2, A3, Th28

 .= (( Line (M,j)) "*" ( Col ((C @ ),i))) by FVSUM_1: 64;

 end;

 theorem :: LAPLACE:30



 Th30: ( Det M) <> ( 0. K) implies (M * ((( Det M) " ) * (( Matrix_of_Cofactor M) @ ))) = ( 1. (K,n))

 proof

 set D = ( Det M);

 set D9 = (D " );

 set C = ( Matrix_of_Cofactor M);

 set DC = (D9 * (C @ ));

 set MC = (M * DC);

 set ID = ( 1. (K,n));

 assume

 A1: D <> ( 0. K);

 now



 A2: ( Indices MC) = ( Indices ID) by MATRIX_0: 26;

 reconsider N = n as Element of NAT by ORDINAL1:def 12;

 let i,j be Nat such that

 A3: [i, j] in ( Indices MC);

 reconsider COL = ( Col ((C @ ),j)), L = ( Line (M,i)) as Element of (N -tuples_on the carrier of K) by MATRIX_0: 24;

 reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 12;



 A4: ( len DC) = n by MATRIX_0: 24;



 A5: ( Indices MC) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

 then

 A6: i in ( Seg n) by A3, ZFMISC_1: 87;



 A7: j in ( Seg n) by A3, A5, ZFMISC_1: 87;

 then

 A8: 1 <= j by FINSEQ_1: 1;

 ( width (C @ )) = n by MATRIX_0: 24;

 then j <= ( width (C @ )) by A7, FINSEQ_1: 1;

 then ( Col (DC,j)) = (D9 * COL) by A8, MATRIXR1: 19;

 then ( mlt (( Line (M,i)),( Col (DC,j)))) = (D9 * ( mlt (L,COL))) by FVSUM_1: 69;



 then

 A9: (( Line (M,i)) "*" ( Col (DC,j))) = (D9 * (( Line (M,i)) "*" ( Col ((C @ ),j)))) by FVSUM_1: 73

 .= (D9 * ( Det ( RLine (M,j9,( Line (M,i9)))))) by A7, Th29;



 A10: ( width M) = n by MATRIX_0: 24;

 then

 A11: (MC * (i,j)) = (D9 * ( Det ( RLine (M,j,( Line (M,i)))))) by A3, A4, A9, MATRIX_3:def 4;

 per cases ;

 suppose

 A12: i = j;

 then

 A13: ( RLine (M,j,( Line (M,i)))) = M by MATRIX11: 30;



 A14: (D * D9) = ( 1_ K) by A1, VECTSP_1:def 10;

 (ID * (i,j)) = ( 1_ K) by A3, A2, A12, MATRIX_1:def 3;

 hence (ID * (i,j)) = (MC * (i,j)) by A3, A10, A4, A9, A13, A14, MATRIX_3:def 4;

 end;

 suppose

 A15: i <> j;

 then

 A16: (ID * (i,j)) = ( 0. K) by A3, A2, MATRIX_1:def 3;

 ( Det ( RLine (M,j9,( Line (M,i9))))) = ( 0. K) by A6, A7, A15, MATRIX11: 51;

 hence (ID * (i,j)) = (MC * (i,j)) by A11, A16;

 end;

 end;

 hence thesis by MATRIX_0: 27;

 end;

 theorem :: LAPLACE:31



 Th31: for f, i st ( len f) = n & i in ( Seg n) holds ( mlt (( Col (( Matrix_of_Cofactor M),i)),f)) = ( LaplaceExpL (( RLine ((M @ ),i,f)),i))

 proof

 let f, i such that

 A1: ( len f) = n and

 A2: i in ( Seg n);

 reconsider N = n as Element of NAT by ORDINAL1:def 12;

 set KK = the carrier of K;

 set C = ( Matrix_of_Cofactor M);

 reconsider Tp = f, TC = ( Col (C,i)) as Element of (N -tuples_on KK) by A1, FINSEQ_2: 92, MATRIX_0: 24;

 set R = ( RLine ((M @ ),i,f));

 set LL = ( LaplaceExpL (R,i));

 set MCT = ( mlt (TC,Tp));



 A3: ( len LL) = n by Def7;

 A4:

 now



 A5: ( Indices (M @ )) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;



 A6: ( dom LL) = ( Seg n) by A3, FINSEQ_1:def 3;



 A7: ( width (M @ )) = n by MATRIX_0: 24;

 let j be Nat such that

 A8: 1 <= j and

 A9: j <= n;



 A10: j in ( Seg n) by A8, A9;

 then ( Delete ((M @ ),i,j)) = (( Delete (M,j,i)) @ ) by A2, Th14;

 then

 A11: ( Cofactor ((M @ ),i,j)) = ( Cofactor (M,j,i)) by MATRIXR2: 43;

 ( Indices C) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

 then [j, i] in ( Indices C) by A2, A10, ZFMISC_1: 87;

 then

 A12: (C * (j,i)) = ( Cofactor (M,j,i)) by Def6;

 n = ( len C) by MATRIX_0: 24;

 then ( dom C) = ( Seg n) by FINSEQ_1:def 3;

 then

 A13: (( Col (C,i)) . j) = (C * (j,i)) by A10, MATRIX_0:def 8;



 A14: ( Indices M) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

 then [i, j] in ( Indices M) by A2, A10, ZFMISC_1: 87;

 then (R * (i,j)) = (f . j) by A1, A7, A14, A5, MATRIX11:def 3;

 then

 A15: (MCT . j) = (( Cofactor (M,j,i)) * (R * (i,j))) by A10, A13, A12, FVSUM_1: 61;

 ( Cofactor (R,i,j)) = ( Cofactor ((M @ ),i,j)) by A2, A10, Th15;

 hence (MCT . j) = (LL . j) by A10, A11, A6, A15, Def7;

 end;

 ( len MCT) = n by CARD_1:def 7;

 hence thesis by A3, A4;

 end;

 theorem :: LAPLACE:32



 Th32: i in ( Seg n) & j in ( Seg n) implies (( Line ((( Matrix_of_Cofactor M) @ ),i)) "*" ( Col (M,j))) = ( Det ( RLine ((M @ ),i,( Line ((M @ ),j)))))

 proof

 assume that

 A1: i in ( Seg n) and

 A2: j in ( Seg n);

 set C = ( Matrix_of_Cofactor M);

 set L = ( Line ((M @ ),j));



 A3: ( width C) = n by MATRIX_0: 24;

 ( width (M @ )) = n by MATRIX_0: 24;

 then

 A4: ( len L) = n by MATRIX_0:def 7;



 A5: ( width M) = n by MATRIX_0: 24;



 thus ( Det ( RLine ((M @ ),i,L))) = ( Sum ( LaplaceExpL (( RLine ((M @ ),i,L)),i))) by A1, Th25

 .= ( Sum ( mlt (( Col (C,i)),L))) by A1, A4, Th31

 .= (( Line ((C @ ),i)) "*" L) by A1, A3, MATRIX_0: 59

 .= (( Line ((C @ ),i)) "*" ( Col (M,j))) by A2, A5, MATRIX_0: 59;

 end;

 theorem :: LAPLACE:33



 Th33: ( Det M) <> ( 0. K) implies (((( Det M) " ) * (( Matrix_of_Cofactor M) @ )) * M) = ( 1. (K,n))

 proof

 set D = ( Det M);

 set D9 = (D " );

 set C = ( Matrix_of_Cofactor M);

 set DC = (D9 * (C @ ));

 set CM = (DC * M);

 set ID = ( 1. (K,n));

 assume

 A1: D <> ( 0. K);

 now



 A2: ( Indices CM) = ( Indices ID) by MATRIX_0: 26;

 reconsider N = n as Element of NAT by ORDINAL1:def 12;

 let i,j be Nat such that

 A3: [i, j] in ( Indices CM);

 reconsider COL = ( Col (M,j)), L = ( Line ((C @ ),i)) as Element of (N -tuples_on the carrier of K) by MATRIX_0: 24;

 reconsider i9 = i, j9 = j as Element of NAT by ORDINAL1:def 12;



 A4: ( len M) = n by MATRIX_0: 24;



 A5: ( Indices CM) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

 then

 A6: i in ( Seg n) by A3, ZFMISC_1: 87;

 then

 A7: 1 <= i by FINSEQ_1: 1;



 A8: j in ( Seg n) by A3, A5, ZFMISC_1: 87;

 ( len (C @ )) = n by MATRIX_0: 24;

 then i <= ( len (C @ )) by A6, FINSEQ_1: 1;

 then ( Line (DC,i)) = (D9 * L) by A7, MATRIXR1: 20;

 then ( mlt (( Line (DC,i)),( Col (M,j)))) = (D9 * ( mlt (L,COL))) by FVSUM_1: 69;



 then

 A9: (( Line (DC,i)) "*" ( Col (M,j))) = (D9 * (( Line ((C @ ),i)) "*" ( Col (M,j)))) by FVSUM_1: 73

 .= (D9 * ( Det ( RLine ((M @ ),i9,( Line ((M @ ),j9)))))) by A6, A8, Th32;



 A10: ( width DC) = n by MATRIX_0: 24;

 then

 A11: (CM * (i,j)) = (D9 * ( Det ( RLine ((M @ ),i,( Line ((M @ ),j)))))) by A3, A4, A9, MATRIX_3:def 4;

 per cases ;

 suppose

 A12: i = j;

 then

 A13: ( RLine ((M @ ),i,( Line ((M @ ),j)))) = (M @ ) by MATRIX11: 30;



 A14: D = ( Det (M @ )) by MATRIXR2: 43;



 A15: (D9 * D) = ( 1_ K) by A1, VECTSP_1:def 10;

 (ID * (i,j)) = ( 1_ K) by A3, A2, A12, MATRIX_1:def 3;

 hence (ID * (i,j)) = (CM * (i,j)) by A3, A10, A4, A9, A13, A15, A14, MATRIX_3:def 4;

 end;

 suppose

 A16: i <> j;

 then

 A17: (ID * (i,j)) = ( 0. K) by A3, A2, MATRIX_1:def 3;

 ( Det ( RLine ((M @ ),i9,( Line ((M @ ),j9))))) = ( 0. K) by A6, A8, A16, MATRIX11: 51;

 hence (ID * (i,j)) = (CM * (i,j)) by A11, A17;

 end;

 end;

 hence thesis by MATRIX_0: 27;

 end;

 theorem :: LAPLACE:34



 Th34: M is invertible iff ( Det M) <> ( 0. K)

 proof

 thus M is invertible implies ( Det M) <> ( 0. K)

 proof

 reconsider N = n as Element of NAT by ORDINAL1:def 12;

 assume M is invertible;

 then

 consider M1 be Matrix of n, K such that

 A1: M is_reverse_of M1 by MATRIX_6:def 3;

 per cases by NAT_1: 14;

 suppose N = 0 ;

 then ( Det M) = ( 1_ K) by MATRIXR2: 41;

 hence thesis;

 end;

 suppose

 A2: N >= 1;



 A3: (M * M1) = ( 1. (K,n)) by A1, MATRIX_6:def 2;

 ( Det ( 1. (K,n))) = ( 1_ K) by A2, MATRIX_7: 16;

 then (( Det M) * ( Det M1)) = ( 1_ K) by A2, A3, MATRIX11: 62;

 hence thesis;

 end;

 end;

 set C = ((( Det M) " ) * (( Matrix_of_Cofactor M) @ ));

 assume

 A4: ( Det M) <> ( 0. K);

 then

 A5: (M * C) = ( 1. (K,n)) by Th30;

 (C * M) = ( 1. (K,n)) by A4, Th33;

 then M is_reverse_of C by A5, MATRIX_6:def 2;

 hence thesis by MATRIX_6:def 3;

 end;

 theorem :: LAPLACE:35



 Th35: ( Det M) <> ( 0. K) implies (M ~ ) = ((( Det M) " ) * (( Matrix_of_Cofactor M) @ ))

 proof

 set C = ((( Det M) " ) * (( Matrix_of_Cofactor M) @ ));

 assume

 A1: ( Det M) <> ( 0. K);

 then

 A2: (M * C) = ( 1. (K,n)) by Th30;

 (C * M) = ( 1. (K,n)) by A1, Th33;

 then

 A3: M is_reverse_of C by A2, MATRIX_6:def 2;

 M is invertible by A1, Th34;

 hence thesis by A3, MATRIX_6:def 4;

 end;

 theorem :: LAPLACE:36

 for M be Matrix of n, K st M is invertible holds for i, j st [i, j] in ( Indices (M ~ )) holds ((M ~ ) * (i,j)) = (((( Det M) " ) * (( power K) . (( - ( 1_ K)),(i + j)))) * ( Minor (M,j,i)))

 proof

 let M be Matrix of n, K;

 assume M is invertible;

 then

 A1: ( Det M) <> ( 0. K) by Th34;

 set D = ( Det M);

 set COF = ( Matrix_of_Cofactor M);

 let i, j;

 assume [i, j] in ( Indices (M ~ ));

 then

 A2: [i, j] in ( Indices (COF @ )) by MATRIX_0: 26;

 then

 A3: [j, i] in ( Indices COF) by MATRIX_0:def 6;



 thus ((M ~ ) * (i,j)) = (((D " ) * (COF @ )) * (i,j)) by A1, Th35

 .= ((D " ) * ((COF @ ) * (i,j))) by A2, MATRIX_3:def 5

 .= ((D " ) * (COF * (j,i))) by A3, MATRIX_0:def 6

 .= ((D " ) * ( Cofactor (M,j,i))) by A3, Def6

 .= (((D " ) * (( power K) . (( - ( 1_ K)),(i + j)))) * ( Minor (M,j,i))) by GROUP_1:def 3;

 end;

 theorem :: LAPLACE:37



 Th37: for A be Matrix of n, K st ( Det A) <> ( 0. K) holds for x,b be Matrix of K st ( len x) = n & (A * x) = b holds x = ((A ~ ) * b) & for i, j st [i, j] in ( Indices x) holds (x * (i,j)) = ((( Det A) " ) * ( Det ( ReplaceCol (A,i,( Col (b,j))))))

 proof

 let A be Matrix of n, K such that

 A1: ( Det A) <> ( 0. K);

 A is invertible by A1, Th34;

 then (A ~ ) is_reverse_of A by MATRIX_6:def 4;

 then

 A2: ((A ~ ) * A) = ( 1. (K,n)) by MATRIX_6:def 2;

 set MC = ( Matrix_of_Cofactor A);

 set D = ( Det A);



 A3: ( width MC) = n by MATRIX_0: 24;



 A4: ( len (MC @ )) = n by MATRIX_0: 24;



 A5: ( width (MC @ )) = n by MATRIX_0: 24;



 A6: ( width (A ~ )) = n by MATRIX_0: 24;



 A7: ( width A) = n by MATRIX_0: 24;

 let x,b be Matrix of K such that

 A8: ( len x) = n and

 A9: (A * x) = b;



 A10: ( len A) = n by MATRIX_0: 24;

 then

 A11: ( len b) = n by A8, A9, A7, MATRIX_3:def 4;

 x = (( 1. (K,n)) * x) by A8, MATRIXR2: 68;

 hence

 A12: x = ((A ~ ) * b) by A8, A9, A6, A10, A7, A2, MATRIX_3: 33;

 let i, j such that

 A13: [i, j] in ( Indices x);



 A14: ( len ( Col (b,j))) = n by A11, MATRIX_0:def 8;

 ( Indices x) = [:( Seg n), ( Seg ( width x)):] by A8, FINSEQ_1:def 3;

 then

 A15: i in ( Seg n) by A13, ZFMISC_1: 87;

 then

 A16: 1 <= i by FINSEQ_1: 1;



 A17: i <= n by A15, FINSEQ_1: 1;



 thus (x * (i,j)) = (( Line ((A ~ ),i)) "*" ( Col (b,j))) by A6, A12, A13, A11, MATRIX_3:def 4

 .= (( Line (((D " ) * (MC @ )),i)) "*" ( Col (b,j))) by A1, Th35

 .= (((D " ) * ( Line ((MC @ ),i))) "*" ( Col (b,j))) by A4, A16, A17, MATRIXR1: 20

 .= ( Sum ((D " ) * ( mlt (( Line ((MC @ ),i)),( Col (b,j)))))) by A5, A11, FVSUM_1: 68

 .= ((D " ) * (( Line ((MC @ ),i)) "*" ( Col (b,j)))) by FVSUM_1: 73

 .= ((D " ) * (( Col (MC,i)) "*" ( Col (b,j)))) by A3, A15, MATRIX_0: 59

 .= ((D " ) * ( Sum ( LaplaceExpL (( RLine ((A @ ),i,( Col (b,j)))),i)))) by A15, A14, Th31

 .= ((D " ) * ( Det ( RLine ((A @ ),i,( Col (b,j)))))) by A15, Th25

 .= ((D " ) * ( Det (( RLine ((A @ ),i,( Col (b,j)))) @ ))) by MATRIXR2: 43

 .= ((D " ) * ( Det ( RCol (A,i,( Col (b,j)))))) by Th19;

 end;

 theorem :: LAPLACE:38



 Th38: for A be Matrix of n, K st ( Det A) <> ( 0. K) holds for x,b be Matrix of K st ( width x) = n & (x * A) = b holds x = (b * (A ~ )) & for i, j st [i, j] in ( Indices x) holds (x * (i,j)) = ((( Det A) " ) * ( Det ( ReplaceLine (A,j,( Line (b,i))))))

 proof

 let A be Matrix of n, K such that

 A1: ( Det A) <> ( 0. K);

 A is invertible by A1, Th34;

 then (A ~ ) is_reverse_of A by MATRIX_6:def 4;

 then

 A2: (A * (A ~ )) = ( 1. (K,n)) by MATRIX_6:def 2;



 A3: ( width A) = n by MATRIX_0: 24;

 let x,b be Matrix of K such that

 A4: ( width x) = n and

 A5: (x * A) = b;



 A6: ( len A) = n by MATRIX_0: 24;

 then

 A7: ( width b) = n by A4, A5, A3, MATRIX_3:def 4;

 set MC = ( Matrix_of_Cofactor A);

 set D = ( Det A);



 A8: ( len (MC @ )) = n by MATRIX_0: 24;



 A9: ( width (MC @ )) = n by MATRIX_0: 24;

 ( len MC) = n by MATRIX_0: 24;

 then

 A10: ( Seg n) = ( dom MC) by FINSEQ_1:def 3;



 A11: ( len (A ~ )) = n by MATRIX_0: 24;

 x = (x * ( 1. (K,n))) by A4, MATRIXR2: 67;

 hence

 A12: x = (b * (A ~ )) by A4, A5, A11, A6, A3, A2, MATRIX_3: 33;

 let i, j such that

 A13: [i, j] in ( Indices x);



 A14: j in ( Seg n) by A4, A13, ZFMISC_1: 87;

 then

 A15: 1 <= j by FINSEQ_1: 1;



 A16: ( len ( Line (b,i))) = n by A7, MATRIX_0:def 7;



 A17: j <= n by A14, FINSEQ_1: 1;



 thus (x * (i,j)) = (( Line (b,i)) "*" ( Col ((A ~ ),j))) by A11, A12, A13, A7, MATRIX_3:def 4

 .= (( Line (b,i)) "*" ( Col (((D " ) * (MC @ )),j))) by A1, Th35

 .= (( Line (b,i)) "*" ((D " ) * ( Col ((MC @ ),j)))) by A9, A15, A17, MATRIXR1: 19

 .= (((D " ) * ( Col ((MC @ ),j))) "*" ( Line (b,i))) by FVSUM_1: 90

 .= ( Sum ((D " ) * ( mlt (( Col ((MC @ ),j)),( Line (b,i)))))) by A8, A7, FVSUM_1: 69

 .= ((D " ) * (( Col ((MC @ ),j)) "*" ( Line (b,i)))) by FVSUM_1: 73

 .= ((D " ) * (( Line (MC,j)) "*" ( Line (b,i)))) by A14, A10, MATRIX_0: 58

 .= ((D " ) * ( Sum ( LaplaceExpL (( RLine (A,j,( Line (b,i)))),j)))) by A14, A16, Th28

 .= ((D " ) * ( Det ( RLine (A,j,( Line (b,i)))))) by A14, Th25;

 end;

 begin

 definition

 let D be non empty set;

 let f be FinSequence of D;

 :: original: <*

 redefine

 func <*f*> -> Matrix of 1, ( len f), D ;

 coherence by MATRIX_0: 11;

 end

 definition

 let K;

 let M be Matrix of K;

 let f be FinSequence of K;

 :: LAPLACE:def9

 func M * f -> Matrix of K equals (M * ( <*f*> @ ));

 coherence ;

 :: LAPLACE:def10

 func f * M -> Matrix of K equals ( <*f*> * M);

 coherence ;

 end

 theorem :: LAPLACE:39

 for A be Matrix of n, K st ( Det A) <> ( 0. K) holds for x,b be FinSequence of K st ( len x) = n & (A * x) = ( <*b*> @ ) holds ( <*x*> @ ) = ((A ~ ) * b) & for i st i in ( Seg n) holds (x . i) = ((( Det A) " ) * ( Det ( ReplaceCol (A,i,b))))

 proof

 let A be Matrix of n, K such that

 A1: ( Det A) <> ( 0. K);

 let x,b be FinSequence of K such that

 A2: ( len x) = n and

 A3: (A * x) = ( <*b*> @ );

 set X = <*x*>;

 ( len X) = 1 by MATRIX_0:def 2;

 then

 A4: ( len x) = ( width X) by MATRIX_0: 20;

 then

 A5: ( len (X @ )) = ( len x) by MATRIX_0:def 6;

 hence (X @ ) = ((A ~ ) * b) by A1, A2, A3, Th37;

 set B = <*b*>;



 A6: 1 in ( Seg 1);

 then

 A7: ( Line (X,1)) = (X . 1) by MATRIX_0: 52;

 ( len B) = 1 by MATRIX_0:def 2;

 then

 A8: 1 in ( dom B) by A6, FINSEQ_1:def 3;



 A9: ( Line (B,1)) = (B . 1) by A6, MATRIX_0: 52;

 let i such that

 A10: i in ( Seg n);

 n > 0 by A10;



 then ( width (X @ )) = ( len X) by A2, A4, MATRIX_0: 54

 .= 1 by MATRIX_0:def 2;

 then ( Indices (X @ )) = [:( Seg n), ( Seg 1):] by A2, A5, FINSEQ_1:def 3;

 then

 A11: [i, 1] in ( Indices (X @ )) by A10, A6, ZFMISC_1: 87;

 then [1, i] in ( Indices X) by MATRIX_0:def 6;



 then ((X @ ) * (i,1)) = (X * (1,i)) by MATRIX_0:def 6

 .= (( Line (X,1)) . i) by A2, A4, A10, MATRIX_0:def 7

 .= (x . i) by A7, FINSEQ_1: 40;



 hence (x . i) = ((( Det A) " ) * ( Det ( ReplaceCol (A,i,( Col ((B @ ),1)))))) by A1, A2, A3, A5, A11, Th37

 .= ((( Det A) " ) * ( Det ( ReplaceCol (A,i,( Line (B,1)))))) by A8, MATRIX_0: 58

 .= ((( Det A) " ) * ( Det ( ReplaceCol (A,i,b)))) by A9, FINSEQ_1: 40;

 end;

 ::$Notion-Name

 theorem :: LAPLACE:40

 for A be Matrix of n, K st ( Det A) <> ( 0. K) holds for x,b be FinSequence of K st ( len x) = n & (x * A) = <*b*> holds <*x*> = (b * (A ~ )) & for i st i in ( Seg n) holds (x . i) = ((( Det A) " ) * ( Det ( ReplaceLine (A,i,b))))

 proof

 let A be Matrix of n, K such that

 A1: ( Det A) <> ( 0. K);

 let x,b be FinSequence of K such that

 A2: ( len x) = n and

 A3: (x * A) = <*b*>;

 set X = <*x*>;



 A4: ( width X) = ( len x) by MATRIX_0: 23;

 hence X = (b * (A ~ )) by A1, A2, A3, Th38;



 A5: [:( Seg 1), ( Seg n):] = ( Indices X) by A2, MATRIX_0: 23;

 set B = <*b*>;



 A6: 1 in ( Seg 1);

 then

 A7: ( Line (X,1)) = (X . 1) by MATRIX_0: 52;

 let i such that

 A8: i in ( Seg n);



 A9: [1, i] in [:( Seg 1), ( Seg n):] by A8, A6, ZFMISC_1: 87;



 A10: ( Line (B,1)) = (B . 1) by A6, MATRIX_0: 52;

 (X * (1,i)) = (( Line (X,1)) . i) by A2, A4, A8, MATRIX_0:def 7

 .= (x . i) by A7, FINSEQ_1: 40;



 hence (x . i) = ((( Det A) " ) * ( Det ( ReplaceLine (A,i,( Line (B,1)))))) by A1, A2, A3, A4, A9, A5, Th38

 .= ((( Det A) " ) * ( Det ( ReplaceLine (A,i,b)))) by A10, FINSEQ_1: 40;

 end;