:: Determinant of Some Matrices of Field Elements :: by Yatsuka Nakamura :: :: Received January 4, 2006 :: Copyright (c) 2006-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, NAT_1, FUNCT_2, FINSEQ_1, RELAT_1, FUNCT_1, TARSKI, FINSEQ_2, XBOOLE_0, SUBSET_1, XXREAL_0, ARYTM_3, JORDAN3, ORDINAL4, ARYTM_1, CARD_1, STRUCT_0, INT_1, CARD_3, GROUP_1, VECTSP_1, MATRIX_1, MATRIX_3, ALGSTR_0, SETWISEO, FINSUB_1, BINOP_1, FINSOP_1, ABIAN, TREES_1, SUPINF_2, FUNCOP_1, MESFUNC1, ZFMISC_1, QC_LANG1, PARTFUN1, FINSEQ_5, CLASSES1, RFINSEQ, FUNCSDOM, MATRIX_7, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XXREAL_0, ORDINAL1, NAT_1, NAT_D, RELAT_1, FUNCT_1, BINOP_1, ZFMISC_1, CARD_1, NUMBERS, VECTSP_1, FUNCT_2, FUNCOP_1, SETWISEO, PARTFUN1, GROUP_4, FINSUB_1, NEWTON, FINSOP_1, SETWOP_2, FINSEQ_1, FINSEQ_2, STRUCT_0, ALGSTR_0, MATRIX_1, MATRIX_3, FINSEQ_6, MATRIX_0, CLASSES1, RFINSEQ, FINSEQ_5, GROUP_1; constructors SETWISEO, REAL_1, NAT_1, NAT_D, FINSOP_1, NEWTON, RFINSEQ, FINSEQ_5, ALGSTR_1, GROUP_4, MATRIX_3, FINSEQ_6, CLASSES1, RELSET_1, BINOP_1, MATRIX_1; registrations SUBSET_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCT_2, FINSUB_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, GROUP_1, VECTSP_1, MATRIX_1, FVSUM_1, FINSET_1, CARD_1, RELSET_1, FINSEQ_2, MATRIX_0; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; definitions TARSKI, MATRIX_1; equalities XBOOLE_0, BINOP_1, FINSEQ_1, MATRIX_0, FINSEQ_2, GROUP_4, ALGSTR_0, RELAT_1; expansions TARSKI, XBOOLE_0, FINSEQ_1, MATRIX_1; theorems BINOP_1, RLVECT_1, MATRIX_3, MATRIX_0, GROUP_1, FUNCT_1, FINSEQ_1, NAT_1, FINSEQ_2, TARSKI, FINSOP_1, FVSUM_1, SETWISEO, FUNCT_2, XBOOLE_0, GROUP_4, ENUMSET1, ZFMISC_1, FINSEQ_6, XREAL_1, FINSEQ_5, INTEGRA2, FUNCOP_1, FINSUB_1, XBOOLE_1, RELAT_1, SUBSET_1, RFINSEQ, FINSEQ_3, XXREAL_0, ORDINAL1, NAT_D, PARTFUN1, XREAL_0, CLASSES1, CARD_1, MATRIX_1; schemes NAT_1, FUNCT_2, FINSEQ_1; begin reserve k,n,i,j for Nat; theorem Th1: for f being Permutation of Seg 2 holds f=<*1,2*> or f=<*2,1*> proof let f be Permutation of Seg 2; A1: rng f = Seg 2 by FUNCT_2:def 3; 2 in {1,2} by TARSKI:def 2; then A2: f.2 in Seg 2 by A1,FINSEQ_1:2,FUNCT_2:4; A3: dom f=Seg 2 by FUNCT_2:52; then reconsider p=f as FinSequence by FINSEQ_1:def 2; A4: len p= 2 by A3,FINSEQ_1:def 3; A5: 1 in dom f & 2 in dom f by A3; 1 in {1,2} by TARSKI:def 2; then A6: f.1 in Seg 2 by A1,FINSEQ_1:2,FUNCT_2:4; now per cases by A6,A2,FINSEQ_1:2,TARSKI:def 2; case f.1=1 & f.2=1; hence contradiction by A5,FUNCT_1:def 4; end; case f.1=1 & f.2=2; hence thesis by A4,FINSEQ_1:44; end; case f.1=2 & f.2=1; hence thesis by A4,FINSEQ_1:44; end; case f.1=2 & f.2=2; hence contradiction by A5,FUNCT_1:def 4; end; end; hence thesis; end; theorem Th2: for f being FinSequence st f=<*1,2*> or f=<*2,1*> holds f is Permutation of Seg 2 proof let f be FinSequence; assume A1: f=<*1,2*> or f=<*2,1*>; len (<*1,2*>)=2 & len (<*2,1*>)=2 by FINSEQ_1:44; then A2: dom f =Seg 2 by A1,FINSEQ_1:def 3; rng f c= Seg 2 proof let y be object; assume y in rng f; then ex x being object st x in dom f & y=f.x by FUNCT_1:def 3; then y=f.1 or y=f.2 by A2,FINSEQ_1:2,TARSKI:def 2; then y=1 or y=2 or (y=2 or y=1) by A1,FINSEQ_1:44; hence thesis; end; then reconsider g=f as Function of Seg 2,Seg 2 by A2,FUNCT_2:2; now per cases by A1; case A3: f=<*1,2*>; for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1=f.x2 holds x1=x2 proof let x1,x2 be object; assume that A4: x1 in dom f & x2 in dom f and A5: f.x1=f.x2; now per cases by A2,A4,FINSEQ_1:2,TARSKI:def 2; case x1=1 & x2=1; hence thesis; end; case A6: x1=1 & x2=2; then f.x1=1 by A3,FINSEQ_1:44; hence contradiction by A3,A5,A6,FINSEQ_1:44; end; case A7: x1=2 & x2=1; then f.x1=2 by A3,FINSEQ_1:44; hence contradiction by A3,A5,A7,FINSEQ_1:44; end; case x1=2 & x2=2; hence thesis; end; end; hence thesis; end; then A8: f is one-to-one by FUNCT_1:def 4; now let x be object; assume x in rng f; then consider z being object such that A9: z in dom f and A10: f.z=x by FUNCT_1:def 3; len f=2 by A3,FINSEQ_1:44; then dom f=Seg 2 by FINSEQ_1:def 3; then z=1 or z=2 by A9,FINSEQ_1:2,TARSKI:def 2; then x =1 or x=2 by A3,A10,FINSEQ_1:44; hence x in Seg 2; end; then A11: rng f c= Seg 2; Seg 2 c= rng f proof let z be object; assume z in Seg 2; then z=1 or z=2 by FINSEQ_1:2,TARSKI:def 2; then A12: z=f.1 or z=f.2 by A3,FINSEQ_1:44; 1 in dom f & 2 in dom f by A2; hence thesis by A12,FUNCT_1:def 3; end; then rng f = Seg 2 by A11; then g is onto by FUNCT_2:def 3; hence thesis by A8; end; case A13: f=<*2,1*>; for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1=f.x2 holds x1=x2 proof let x1,x2 be object; assume that A14: x1 in dom f & x2 in dom f and A15: f.x1=f.x2; now per cases by A2,A14,FINSEQ_1:2,TARSKI:def 2; case x1=1 & x2=1; hence thesis; end; case A16: x1=1 & x2=2; then f.x1=2 by A13,FINSEQ_1:44; hence contradiction by A13,A15,A16,FINSEQ_1:44; end; case A17: x1=2 & x2=1; then f.x1=1 by A13,FINSEQ_1:44; hence contradiction by A13,A15,A17,FINSEQ_1:44; end; case x1=2 & x2=2; hence thesis; end; end; hence thesis; end; then A18: f is one-to-one by FUNCT_1:def 4; now let x be object; assume x in rng f; then consider z being object such that A19: z in dom f and A20: f.z=x by FUNCT_1:def 3; len f=2 by A13,FINSEQ_1:44; then dom f=Seg 2 by FINSEQ_1:def 3; then z=1 or z=2 by A19,FINSEQ_1:2,TARSKI:def 2; then x =2 or x=1 by A13,A20,FINSEQ_1:44; hence x in Seg 2; end; then A21: rng f c= Seg 2; Seg 2 c= rng f proof let z be object; assume z in Seg 2; then z=1 or z=2 by FINSEQ_1:2,TARSKI:def 2; then A22: z=f.2 or z=f.1 by A13,FINSEQ_1:44; 2 in dom f & 1 in dom f by A2; hence thesis by A22,FUNCT_1:def 3; end; then rng f = Seg 2 by A21; then g is onto by FUNCT_2:def 3; hence thesis by A18; end; end; hence thesis; end; theorem Th3: Permutations(2)={<*1,2*>,<*2,1*>} proof now let x be object; assume A1: x in {idseq 2,<*2,1*>}; now per cases by A1,TARSKI:def 2; case x=idseq 2; hence x in Permutations(2) by MATRIX_1:def 12; end; case A2: x=<*2,1*>; <*2,1*> is Permutation of Seg 2 by Th2; hence x in Permutations(2) by A2,MATRIX_1:def 12; end; end; hence x in Permutations(2); end; then A3: {idseq 2,<*2,1*>} c=Permutations(2); now let p be object; assume p in Permutations(2); then reconsider q=p as Permutation of Seg 2 by MATRIX_1:def 12; q=<*1,2*> or q=<*2,1*> by Th1; hence p in {idseq 2,<*2,1*>} by FINSEQ_2:52,TARSKI:def 2; end; then Permutations(2) c={idseq 2,<*2,1*>}; hence thesis by A3,FINSEQ_2:52; end; theorem Th4: for p being Permutation of Seg 2 st p is being_transposition holds p = <*2,1*> proof let p be Permutation of Seg 2; assume A1: p is being_transposition; now set p0=<*1,2*>; assume A2: p=<*1,2*>; consider i,j being Nat such that A3: i in dom p and A4: j in dom p & i<>j and A5: p.i=j and p.j=i and for k being Nat st k <>i & k<>j & k in dom p holds p.k=k by A1; len p0=2 by FINSEQ_1:44; then A6: dom p ={1,2} by A2,FINSEQ_1:2,def 3; then A7: i=1 or i=2 by A3,TARSKI:def 2; now per cases by A4,A6,A7,TARSKI:def 2; case i=1 & j=2; hence contradiction by A2,A5,FINSEQ_1:44; end; case i=2 & j=1; hence contradiction by A2,A5,FINSEQ_1:44; end; end; hence contradiction; end; hence thesis by Th1; end; theorem Th5: for D being non empty set, f being FinSequence of D, k2 being Nat st 1<=k2 & k2< len f holds f = mid(f,1,k2)^mid(f,k2+1,len f) proof let D be non empty set, f be FinSequence of D, k2 be Nat; assume A1: 1<=k2 & k2< len f; then mid(f,1,len f) = mid(f,1,k2)^mid(f,k2+1,len f) by INTEGRA2:4; hence thesis by A1,FINSEQ_6:120,XXREAL_0:2; end; theorem Th6: for D being non empty set, f being FinSequence of D st 2<= len f holds f = (f|(len f-'2))^mid(f,len f-'1,len f) proof let D be non empty set, f be FinSequence of D; assume A1: 2<= len f; then A2: len f-'2=len f-2 by XREAL_1:233; then A3: len f-'2+1=len f-1-1+1 .=len f-'1 by A1,XREAL_1:233,XXREAL_0:2; now per cases; case len f-'2>0; then A4: 0+1<=len f-'2 by NAT_1:13; len f0; then A3: 0+1<=len f-'1 by NAT_1:13; len f <> <*2,1*> by FINSEQ_1:77; theorem Th8: for a being Element of Group_of_Perm 2 st (ex q being Element of Permutations 2 st q=a & q is being_transposition) holds a = <*2,1*> proof let a be Element of Group_of_Perm 2; given q being Element of Permutations 2 such that A1: q=a and A2: q is being_transposition; the carrier of Group_of_Perm 2 = Permutations 2 by MATRIX_1:def 13; then reconsider b=a as Permutation of Seg 2 by MATRIX_1:def 12; ex i,j being Nat st i in dom q & j in dom q & i<>j & q. i=j & q.j=i & for k being Nat st k <>i & k<>j & k in dom q holds q.k=k by A2; then b is being_transposition by A1; hence thesis by Th4; end; theorem for n being Nat,a,b being Element of Group_of_Perm n, pa,pb being Element of Permutations n st a=pa & b=pb holds a*b=pb*pa by MATRIX_1:def 13; theorem Th10: for a,b being Element of Group_of_Perm 2 st (ex p being Element of Permutations 2 st p=a & p is being_transposition)& (ex q being Element of Permutations 2 st q=b & q is being_transposition) holds a*b = <*1,2*> proof let a,b be Element of Group_of_Perm 2; assume that A1: ex p being Element of Permutations 2 st p=a & p is being_transposition and A2: ex q being Element of Permutations 2 st q=b & q is being_transposition; consider p being Element of Permutations 2 such that A3: p=a and A4: p is being_transposition by A1; the carrier of Group_of_Perm 2 =Permutations 2 by MATRIX_1:def 13; then A5: a*b = <*1,2*> or a*b = <*2,1*> by Th3,TARSKI:def 2; reconsider p2=p as FinSequence by A3,A4,Th8; A6: a= <*2,1*> by A1,Th8; then len p2=2 by A3,FINSEQ_1:44; then 1 in Seg len p2; then A7: 1 in dom p2 by FINSEQ_1:def 3; consider q being Element of Permutations 2 such that A8: q=b and A9: q is being_transposition by A2; reconsider q2=q as FinSequence by A8,A9,Th8; b= <*2,1*> by A2,Th8; then A10: q2.2=1 by A8,FINSEQ_1:44; A11: a*b=q*p by A3,A8,MATRIX_1:def 13; p2.1=2 by A6,A3,FINSEQ_1:44; then (q*p).1=1 by A10,A7,FUNCT_1:13; hence thesis by A5,A11,FINSEQ_1:44; end; theorem Th11: for l being FinSequence of Group_of_Perm 2 st (len l) mod 2=0 & (for i st i in dom l holds (ex q being Element of Permutations 2 st l.i=q & q is being_transposition)) holds Product l = <*1,2*> proof defpred P[Nat] means for f being FinSequence of Group_of_Perm 2 st len f=2*$1 & (for i st i in dom f holds (ex q being Element of Permutations 2 st f.i=q & q is being_transposition)) holds Product f = <*1,2*>; let l be FinSequence of Group_of_Perm 2; assume that A1: (len l)mod 2=0 and A2: for i st i in dom l holds ex q being Element of Permutations 2 st l. i=q & q is being_transposition; ( ex t being Nat st len l = 2 * t + 0 & 0 < 2 ) or 0 = 0 & 2 = 0 by A1, NAT_D:def 2; then consider t being Nat such that A3: len l = 2 * t; A4: for s being Nat st P[s] holds P[s+1] proof let s be Nat; assume A5: P[s]; for f being FinSequence of Group_of_Perm 2 st len f=2*(s+1) & (for i st i in dom f holds (ex q being Element of Permutations 2 st f.i=q & q is being_transposition)) holds Product f = <*1,2*> proof let f be FinSequence of Group_of_Perm 2; assume that A6: len f=2*(s+1) and A7: for i st i in dom f holds ex q being Element of Permutations 2 st f .i=q & q is being_transposition; A8: len f = 2*s+2 by A6; then A9: 2 <= len f by NAT_1:11; then A10: len f-'1=len f-1 by XREAL_1:233,XXREAL_0:2; A11: len f-(len f-'1)+1=len f-(len f-1)+1 by A9,XREAL_1:233,XXREAL_0:2 .=2; set g=mid(f,len f-'1,len f); A12: len f-'1<= len f by NAT_D:35; A13: 1 <= len f by A9,XXREAL_0:2; then len f in Seg len f; then len f in dom f by FINSEQ_1:def 3; then A14: ex q being Element of Permutations 2 st f.(len f)=q & q is being_transposition by A7; reconsider pw2=Product mid(g,len g,len g) as Element of Group_of_Perm 2; reconsider pw1=Product (g|(len g-'1)) as Element of Group_of_Perm 2; A15: 1+(len f-'1)-'1=1+(len f-'1)-1 by NAT_1:11,XREAL_1:233 .=len f-'1; A16: 1+1-1<=len f-1 by A9,XREAL_1:13; then A17: 1<=len f-'1 by A9,XREAL_1:233,XXREAL_0:2; then A18: len (mid(f,len f-'1,len f)) = len f-'(len f-'1)+1 by A13,A12,FINSEQ_6:118 .=len f-(len f-'1)+1 by NAT_D:35,XREAL_1:233 .=len f-(len f-1)+1 by A9,XREAL_1:233,XXREAL_0:2 .=2; then len g-'1=len g-1 by XREAL_1:233; then A19: (g|(len g-'1)).1=g.1 by A18,FINSEQ_3:112 .=f.(len f-'1) by A16,A12,A11,A15,FINSEQ_6:122; A20: for i st i in dom (f|(len f-'2)) holds ex q being Element of Permutations 2 st (f|(len f-'2)).i=q & q is being_transposition proof let i; assume i in dom (f|(len f-'2)); then A21: i in Seg len (f|(len f-'2)) by FINSEQ_1:def 3; then A22: 1<= i by FINSEQ_1:1; A23: i<= len (f|(len f-'2)) by A21,FINSEQ_1:1; len (f|(len f-'2)) <= len f by FINSEQ_5:16; then i<=len f by A23,XXREAL_0:2; then i in dom f by A22,FINSEQ_3:25; then A24: ex q being Element of Permutations 2 st f.i=q & q is being_transposition by A7; len (f|(len f-'2))=len f-'2 by FINSEQ_1:59,NAT_D:35; hence thesis by A23,A24,FINSEQ_3:112; end; len (f|(len f-'2))=len f-'2 by FINSEQ_1:59,NAT_D:35 .= 2*s by A8,NAT_D:34; then Product (f|(len f-'2))=<*1,2*> by A5,A20; then A25: 1_Group_of_Perm 2=(Product (f|(len f-'2))) by FINSEQ_2:52,MATRIX_1:15; f = (f|(len f-'2))^mid(f,len f-'1,len f) by A8,Th6,NAT_1:11; then A26: Product f = (Product (f|(len f-'2)))*(Product (mid(f,len f-'1,len f ))) by GROUP_4:5 .= (Product (mid(f,len f-'1,len f))) by A25,GROUP_1:def 4; 2<=2+(len f-'1) by NAT_1:11; then A27: 2+(len f-'1)-'1=2+(len f-'1)-1 by XREAL_1:233,XXREAL_0:2 .=len f by A10; A28: len f-(len f-'1)+1=len f-(len f-1)+1 by A9,XREAL_1:233,XXREAL_0:2 .= 1+1; A29: 1+ len g-'1=1+len g-1 by NAT_1:11,XREAL_1:233; A30: len (g|(len g-'1)) = len g-'1 by FINSEQ_1:59,NAT_D:35 .= len g-1 by A18,XREAL_1:233 .=1 by A18; then 1 in Seg len (g|(len g-'1)); then 1 in dom (g|(len g-'1)) by FINSEQ_1:def 3; then rng (g|(len g-'1)) c= the carrier of Group_of_Perm 2 & (g|(len g-'1 )).1 in rng (g|(len g-'1)) by FINSEQ_1:def 4,FUNCT_1:def 3; then reconsider r=(g|(len g-'1)).1 as Element of Group_of_Perm 2; A31: pw1 = Product (<* r *>) by A30,FINSEQ_1:40 .=f.(len f-'1) by A19,FINSOP_1:11; 1<=len g-len g+1; then A32: (mid(g,len g,len g)).1=g.(1+len g-'1) by A18,FINSEQ_6:122 .=f.(len f) by A16,A12,A18,A28,A29,A27,FINSEQ_6:122; A33: len mid(g,len g,len g)=len g-'len g+1 by A18,FINSEQ_6:118 .= 0+1 by XREAL_1:232 .=1; then 1 in Seg len (mid(g,len g,len g)); then 1 in dom (mid(g,len g,len g)) by FINSEQ_1:def 3; then rng (mid(g,len g,len g)) c= the carrier of Group_of_Perm 2 & (mid(g ,len g, len g)).1 in rng (mid(g,len g,len g)) by FINSEQ_1:def 4,FUNCT_1:def 3; then reconsider s=(mid(g,len g,len g)).1 as Element of Group_of_Perm 2; A34: pw2 = Product (<* s *>) by A33,FINSEQ_1:40 .=f.len f by A32,FINSOP_1:11; len f-'1 in Seg len f by A17,A12; then len f-'1 in dom f by FINSEQ_1:def 3; then A35: ex q being Element of Permutations 2 st f.(len f-'1)=q & q is being_transposition by A7; g= (g|(len g-'1))^mid(g,len g,len g) by A18,Th7; then Product g=(Product ((g|(len g-'1))))*(Product mid(g,len g,len g)) by GROUP_4:5 .= <*1,2*> by A35,A14,A31,A34,Th10; hence thesis by A26; end; hence thesis; end; for f being FinSequence of Group_of_Perm 2 st len f=2*0 & (for i st i in dom f holds (ex q being Element of Permutations 2 st f.i=q & q is being_transposition)) holds Product f = <*1,2*> proof set G=Group_of_Perm 2; let f be FinSequence of Group_of_Perm 2; assume that A36: len f=2*0 and for i st i in dom f holds ex q being Element of Permutations 2 st f. i =q & q is being_transposition; A37: 1_G= <*1,2*> by FINSEQ_2:52,MATRIX_1:15; f=<*> (the carrier of G) by A36; hence thesis by A37,GROUP_4:8; end; then A38: P[0]; A39: for s being Nat holds P[s] from NAT_1:sch 2(A38,A4); reconsider t as Nat; len l = 2 * t by A3; hence thesis by A2,A39; end; theorem for K being Field, M being Matrix of 2,K holds Det M = (M*(1,1))*(M*(2 ,2))-(M*(1,2))*(M*(2,1)) proof reconsider s1=<*1,2*>, s2=<*2,1*> as Permutation of Seg 2 by Th2; let K be Field, M be Matrix of 2,K; A1: now A2: s1.1=1 by FINSEQ_1:44; assume s1=s2; hence contradiction by A2,FINSEQ_1:44; end; set D0={s1,s2}; reconsider l0=<*>D0 as FinSequence of Group_of_Perm(2) by Th3,MATRIX_1:def 13 ; set X=Permutations 2; reconsider p1 = s1, p2 = s2 as Element of Permutations(2) by MATRIX_1:def 12; set Y=the carrier of K; set f=Path_product M; set F=the addF of K; set di=(the multF of K) $$ (Path_matrix(p1,M)); set B=In (Permutations 2,Fin Permutations 2); Permutations 2 in Fin Permutations 2 by FINSUB_1:def 5; then A3: B=Permutations 2 by SUBSET_1:def 8; Det M=(the addF of K) $$ (In(Permutations 2,Fin Permutations 2) ,Path_product M) by MATRIX_3:def 9; then consider G being Function of Fin X, Y such that A4: Det M = G.B and for e being Element of Y st e is_a_unity_wrt F holds G.{} = e and A5: for x being Element of X holds G.{x} = f.x and A6: for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being Element of X st x in B \ B9 holds G.(B9 \/ {x}) = F.(G.B9,f.x) by A3, SETWISEO:def 3; A7: G.{p1} = f.p1 by A5; A8: G.B = (the addF of K).(f.p1,f.p2) proof reconsider B9={.p1.} as Element of Fin X; A9: B9 c= B proof let y be object; assume y in B9; then y=p1 by TARSKI:def 1; hence thesis by A3; end; B\B9 ={s2} by A1,A3,Th3,ZFMISC_1:17; then s2 in B\B9 by TARSKI:def 1; then G.(B9 \/ {p2}) = F.(G.B9,f.p2) by A6,A9; hence thesis by A3,A7,Th3,ENUMSET1:1; end; set dj=(the multF of K) $$ (Path_matrix(p2,M)); A10: p1.2 = 2 by FINSEQ_1:44; A11: p2.2 = 1 by FINSEQ_1:44; A12: len Path_matrix(p1,M) = 2 by MATRIX_3:def 7; then consider f3 being sequence of the carrier of K such that A13: f3.1 = (Path_matrix(p1,M)).1 and A14: for n being Nat st 0 <> n & n < 2 holds f3.(n + 1) = ( the multF of K).(f3.n,(Path_matrix(p1,M)).(n + 1)) and A15: di = f3.2 by FINSOP_1:def 1; A16: 1 in Seg 2; then A17: 1 in dom Path_matrix(p1,M) by A12,FINSEQ_1:def 3; A18: 2 in Seg 2; then 2 in dom Path_matrix(p1,M) by A12,FINSEQ_1:def 3; then A19: p1.1 = 1 & Path_matrix(p1,M).2=M*(2,2) by A10,FINSEQ_1:44,MATRIX_3:def 7; A20: len Path_matrix(p2,M) = 2 by MATRIX_3:def 7; then consider f4 being sequence of the carrier of K such that A21: f4.1 = (Path_matrix(p2,M)).1 and A22: for n being Nat st 0 <> n & n < 2 holds f4.(n + 1) = ( the multF of K).(f4.n,(Path_matrix(p2,M)).(n + 1)) and A23: dj = f4.2 by FINSOP_1:def 1; A24: 1 in dom Path_matrix(p2,M) by A20,A16,FINSEQ_1:def 3; 2 in dom Path_matrix(p2,M) by A20,A18,FINSEQ_1:def 3; then A25: p2.1 = 2 & Path_matrix(p2,M).2=M*(2,1) by A11,FINSEQ_1:44,MATRIX_3:def 7; A26: f4.(1+1)=(the multF of K).(f4.1,(Path_matrix(p2,M)).(1+1)) by A22 .=(M*(1,2))*(M*(2,1)) by A24,A25,A21,MATRIX_3:def 7; A27: len Permutations 2 = 2 by MATRIX_1:9; not ex l be FinSequence of Group_of_Perm 2 st (len l)mod 2=0 & s2= Product l & for i st i in dom l ex q being Element of Permutations 2 st l.i=q & q is being_transposition by Lm1,Th11; then f.p2 = -((the multF of K) "**" (Path_matrix(p2,M)),p2) & p2 is odd by A27,MATRIX_3:def 8; then A28: f.p2 = - dj by MATRIX_1:def 16; A29: Product l0=Product <*> (the carrier of Group_of_Perm 2) .= 1_(Group_of_Perm(2)) by GROUP_4:8 .= p1 by FINSEQ_2:52,MATRIX_1:15; A30: 0 mod 2=0 by NAT_D:26; ex l be FinSequence of Group_of_Perm 2 st (len l)mod 2=0 & s1=Product l & for i st i in dom l ex q being Element of Permutations 2 st l.i=q & q is being_transposition proof take l0; thus (len l0)mod 2=0 & s1=Product l0 by A30,A29; let i; thus thesis; end; then A31: f.p1 = -((the multF of K) "**" (Path_matrix(p1,M)),p1) & p1 is even by A27 ,MATRIX_3:def 8; f3.(1+1)=(the multF of K).(f3.1,(Path_matrix(p1,M)).(1+1)) by A14 .=(M*(1,1))*(M*(2,2)) by A17,A19,A13,MATRIX_3:def 7; hence thesis by A4,A8,A15,A23,A26,A31,A28,MATRIX_1:def 16; end; definition let n be Nat,K be commutative Ring; let M be (Matrix of n,K), a be Element of K; redefine func a*M -> Matrix of n,K; coherence proof A1: width (a*M)=width M by MATRIX_3:def 5; A2: len M =n by MATRIX_0:def 2; A3: len (a*M)=len M by MATRIX_3:def 5; A4: len M = n by MATRIX_0:def 2; now per cases; case A5: len M>0; then n=width M by A2,MATRIX_0:20; hence thesis by A2,A3,A1,A5,MATRIX_0:20; end; case len M<=0; then A6: len (a*M)=0 by MATRIX_3:def 5; then A7: Seg len (a*M)={}; for p being FinSequence of K st p in rng (a*M) holds len p = 0 proof let p be FinSequence of K; assume p in rng (a*M); then ex x being object st x in dom (a*M) & p=(a*M).x by FUNCT_1:def 3; hence thesis by A7,FINSEQ_1:def 3; end; hence thesis by A4,A3,A6,MATRIX_0:def 2; end; end; hence thesis; end; end; theorem Th13: for K being Ring, n,m being Nat holds len (0.(K,n,m))=n & dom (0.(K,n,m))=Seg n proof let K be Ring, n,m be Nat; len (n |-> (m |-> 0.K))=n by CARD_1:def 7; hence len (0.(K,n,m)) =n by MATRIX_3:def 1; hence thesis by FINSEQ_1:def 3; end; theorem Th14: for K being Ring, n being Nat, p being Element of Permutations n, i being Nat st i in Seg n holds p.i in Seg n proof let K be Ring, n be Nat, p be Element of Permutations(n),i be Nat; A1: p is Permutation of Seg n by MATRIX_1:def 12; assume i in Seg n; hence thesis by A1,FUNCT_2:5; end; theorem for K being Ring, n being Nat st n>=1 holds Det (0.(K,n,n) ) = 0.K proof let K be Ring, n be Nat; set B=In(Permutations n,Fin Permutations n); set f=Path_product(0.(K,n,n)); set F=the addF of K; set Y=the carrier of K; set X=Permutations n; reconsider G0= Fin X --> 0.K as Function of Fin X, Y; A1: G0.B=0.K by FUNCOP_1:7; A2: for e being Element of Y st e is_a_unity_wrt F holds G0.({}) = e proof let e be Element of Y; 0.K is_a_unity_wrt F by FVSUM_1:6; then A3: F.(0.K,e)=e by BINOP_1:3; assume e is_a_unity_wrt F; then F.(0.K,e)=0.K by BINOP_1:3; hence thesis by A3,FINSUB_1:7,FUNCOP_1:7; end; assume A4: n>=1; A5: for x being object st x in dom (Path_product(0.(K,n,n))) holds ( Path_product(0.(K,n,n))).x=(Permutations(n) --> 0.K).x proof let x be object; assume x in dom (Path_product(0.(K,n,n))); for p being Element of Permutations(n) holds (Permutations(n) --> 0.K) .p = -((the multF of K) $$ Path_matrix(p,(0.(K,n,n))),p) proof defpred P[Nat] means (the multF of K) $$ ( ($1+1) |-> 0.K)=0. K; let p be Element of Permutations(n); A6: for k being Nat st P[k] holds P[k+1] proof let k be Nat; A7: (k+1+1) |-> 0.K = ((k+1) |-> 0.K) ^ <* 0.K *> by FINSEQ_2:60; assume P[k]; then (the multF of K) $$ ( (k+1+1) |-> 0.K) = (0.K)*(0.K) by A7, FINSOP_1:4 .= 0.K; hence thesis; end; (1 |-> 0.K)= <* 0.K *> by FINSEQ_2:59; then A8: P[0] by FINSOP_1:11; A9: for k being Nat holds P[k] from NAT_1:sch 2(A8,A6); A10: now per cases; case p is even; hence -(0.K,p)=(0.K) by MATRIX_1:def 16; end; case not p is even; then -(0.K,p)= -(0.K) by MATRIX_1:def 16 .=0.K by RLVECT_1:12; hence -(0.K,p)=(0.K); end; end; A11: for i,j st i in dom (n |-> 0.K) & j=p.i holds (n |-> 0.K).i=(0.(K,n, n))*(i,j) proof let i,j; assume that A12: i in dom (n |-> 0.K) and A13: j=p.i; A14: i in Seg n by A12,FUNCOP_1:13; then j in Seg n by A13,Th14; then A15: j in Seg width (0.(K,n,n)) by A4,MATRIX_0:23; i in dom (0.(K,n,n)) by A14,Th13; then A16: [i,j] in Indices (0.(K,n,n)) by A15,ZFMISC_1:def 2; (n |-> 0.K).i=0.K by A14,FUNCOP_1:7; hence thesis by A16,MATRIX_3:1; end; len (n |-> 0.K)=n by CARD_1:def 7; then A17: Path_matrix(p,(0.(K,n,n)))=(n |-> 0.K) by A11,MATRIX_3:def 7; n-'1=n-1 by A4,XREAL_1:233; then A18: n-'1+1=n; (Permutations(n) --> 0.K).p = 0.K by FUNCOP_1:7; hence thesis by A17,A9,A18,A10; end; hence thesis by MATRIX_3:def 8; end; dom (Permutations(n) --> 0.K)=Permutations(n) by FUNCOP_1:13; then dom (Path_product(0.(K,n,n)))=dom (Permutations(n) --> 0.K) by FUNCT_2:def 1; then A19: Path_product(0.(K,n,n))=Permutations(n) --> 0.K by A5,FUNCT_1:2; A20: for x being Element of X holds G0.({x}) = f.x proof let x be Element of X; G0.({.x.})=0.K by FUNCOP_1:7; hence thesis by A19,FUNCOP_1:7; end; A21: for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being Element of X st x in B\B9 holds G0.(B9 \/ {x}) = F.(G0.B9,f.x) proof let B9 be Element of Fin X; assume that B9 c= B and B9 <> {}; thus for x being Element of X st x in B\B9 holds G0.(B9 \/ {x}) = F.(G0.B9 ,f.x) proof let x be Element of X; assume x in B\B9; A22: G0.(B9 \/ {.x.})=0.K & G0.B9=0.K by FUNCOP_1:7; f.x= 0.K & 0.K is_a_unity_wrt F by A19,FUNCOP_1:7,FVSUM_1:6; hence thesis by A22,BINOP_1:3; end; end; X in Fin X by FINSUB_1:def 5; then B = X by SUBSET_1:def 8; then B <> {} or F is having_a_unity; then (the addF of K) $$ (In(Permutations(n),Fin Permutations n), Path_product(0.(K,n,n)))= 0.K by A1,A2,A20,A21,SETWISEO:def 3; hence thesis by MATRIX_3:def 9; end; definition let x be object; let y be set; let a,b be object; func IFIN(x,y,a,b) -> object equals :Def1: a if x in y otherwise b; correctness; end; theorem for K being Ring, n being Nat st n>=1 holds Det (1.(K,n)) = 1_K proof let K be Ring, n be Nat; assume A1: n>=1; deffunc F2(object) = IFEQ(idseq n,$1,1_K,0.K); set X=Permutations(n); set Y=the carrier of K; A2: for x being object st x in X holds F2(x) in Y; ex f2 being Function of X,Y st for x being object st x in X holds f2.x = F2(x) from FUNCT_2:sch 2(A2); then consider f2 being Function of X,Y such that A3: for x being object st x in X holds f2.x = F2(x); A4: id (Seg n) is even by MATRIX_1:16; A5: for x being object st x in dom (Path_product(1.(K,n))) holds (Path_product(1.(K,n))).x=f2.x proof let x be object; assume x in dom (Path_product(1.(K,n))); for p being Element of Permutations(n) holds f2.p = -((the multF of K ) $$ Path_matrix(p,(1.(K,n))),p) proof defpred P[Nat] means (the multF of K) $$ ( ($1+1) |-> 1_K)= 1_K; let p be Element of Permutations(n); A6: for k being Nat st P[k] holds P[k+1] proof let k be Nat; A7: (k+1+1) |-> 1_K = ((k+1) |-> 1_K) ^ <* 1_K *> by FINSEQ_2:60; assume P[k]; then (the multF of K) $$ ( (k+1+1) |-> 1_K) = (1_K)*(1_K) by A7, FINSOP_1:4 .= 1_K; hence thesis; end; A8: now per cases; case p is even; hence -(0.K,p)=(0.K) by MATRIX_1:def 16; end; case not p is even; then -(0.K,p)= -(0.K) by MATRIX_1:def 16 .=0.K by RLVECT_1:12; hence -(0.K,p)=0.K; end; end; n-'1=n-1 by A1,XREAL_1:233; then A9: n-'1+1=n; (1 |-> 1_K)= <* 1_K *> by FINSEQ_2:59; then A10: P[0] by FINSOP_1:11; for k being Nat holds P[k] from NAT_1:sch 2(A10,A6); then A11: len (n |-> 1_K)=n & (the multF of K) $$ (n |-> 1_K)=1_K by A9, CARD_1:def 7; now per cases; case A12: p=idseq n; A13: for i,j st i in dom (n |-> 1_K) & j=p.i holds (n |-> 1_K).i=(1. (K,n))*(i,j) proof A14: Indices (1.(K,n))=[: Seg n,Seg n:] by A1,MATRIX_0:23; let i,j; assume that A15: i in dom (n |-> 1_K) and A16: j=p.i; A17: i in Seg n by A15,FUNCOP_1:13; then j in Seg n by A16,Th14; then A18: [i,j] in Indices (1.(K,n)) by A17,A14,ZFMISC_1:def 2; (n |-> 1_K).i=1_K & p.i=i by A12,A17,FUNCOP_1:7,FUNCT_1:17; hence thesis by A16,A18,MATRIX_1:def 3; end; len Permutations n = n by MATRIX_1:9; then A19: -((the multF of K) $$ Path_matrix(p,(1.(K,n))),p) = (the multF of K) $$ Path_matrix(p,(1.(K,n))) by A4,A12,MATRIX_1:def 16; f2.p=F2(p) by A3 .= 1_K by A12,FUNCOP_1:def 8; hence thesis by A11,A19,A13,MATRIX_3:def 7; end; case A20: p<>idseq n; reconsider A=NAT as non empty set; defpred P3[Nat] means $1 < n implies ex p3 being FinSequence of K st len p3=$1+1 & p3.1=(Path_matrix(p,(1.(K,n)))).1 & (for n3 being Nat st 0 <> n3 & n3 < $1+1 & n3 as FinSequence of K; A23: for n3 being Nat st 0 <> n3 & n3 < 0+1 & n3< n holds q3.(n3 + 1) = (the multF of K). (q3.n3,(Path_matrix(p,(1.(K,n)))).(n3 + 1)) by NAT_1:13; A24: dom p = Seg len Permutations n by FUNCT_2:52; then A25: dom p = Seg n by MATRIX_1:9; then dom p = dom idseq n by RELAT_1:45; then consider i0 being object such that A26: i0 in dom p and A27: p.i0 <> (idseq n).i0 by A20,FUNCT_1:2; reconsider i0 as Element of NAT by A24,A26; A28: p.i0<>i0 by A25,A26,A27,FUNCT_1:18; A29: for k being Nat st P3[k] holds P3[k+1] proof let k be Nat; assume A30: P3[k]; now per cases; case A31: k+1 n3 & n3 < k+1 & n3 as FinSequence of K; A39: len q3=(len p3) + len (<*e*>) by FINSEQ_1:22 .=k+1+1 by A32,FINSEQ_1:40; A40: for n3 being Nat st 0 <> n3 & n3 < k+1+1 & n3< n holds q3.(n3 + 1) = (the multF of K). (q3.n3,(Path_matrix(p,(1.(K,n)))).(n3 + 1)) proof let n3 be Nat; assume that A41: 0 <> n3 and A42: n3 < k+1+1 and A43: n3=k+1; A48: n3+1<=k+1+1 by A42,NAT_1:13; A49: n3+1>k+1 by A47,NAT_1:13; then n3+1>=k+1+1 by NAT_1:13; then A50: n3+1=k+1+1 by A48,XXREAL_0:1; 1<=k+1 by NAT_1:12; then A51: k+1 in Seg (k+1); then k+1 in dom p3 by A32,FINSEQ_1:def 3; then A52: q3.(k+1)=p3.(k+1) by FINSEQ_1:def 7; (q3).(n3+1) = (<*e*>).(n3+1 - (k+1)) by A32,A39,A49,A48, FINSEQ_1:24 .= e by A50,FINSEQ_1:def 8; hence thesis by A38,A50,A51,A52; end; end; hence thesis; end; 1<=k+1 by NAT_1:12; then 1 in Seg len p3 by A32; then 1 in dom p3 by FINSEQ_1:def 3; then q3.1=(Path_matrix(p,(1.(K,n)))).1 by A33,FINSEQ_1:def 7; hence thesis by A39,A40; end; case k+1>=n; hence thesis; end; end; hence thesis; end; n n3 & n3 < n-'1+1 & n3< n holds p3.(n3 + 1) = (the multF of K). (p3.n3,(Path_matrix(p,(1.(K,n)))).(n3 + 1)) by A55,A53; defpred P[set,set] means ($1 in Seg n implies $2=p3.$1)& (not $1 in Seg n implies $2=0.K); A60: for x3 being Element of A ex y3 being Element of K st P[x3,y3] proof let x3 be Element of A; now per cases; case A61: x3 in Seg n; then x3 in dom p3 by A55,A57,FINSEQ_1:def 3; then rng p3 c= the carrier of K & p3.x3 in rng p3 by FINSEQ_1:def 4,FUNCT_1:def 3; hence thesis by A61; end; case not x3 in Seg n; hence thesis; end; end; hence thesis; end; ex f4 being Function of A,the carrier of K st for x2 being Element of A holds P[x2,f4.x2] from FUNCT_2:sch 3(A60); then consider f4 being sequence of the carrier of K such that A62: for x4 being Element of NAT holds (x4 in Seg n implies f4. x4=p3.x4)& (not x4 in Seg n implies f4.x4=0.K); p is Permutation of Seg n by MATRIX_1:def 12; then A63: p.i0 in Seg n by A25,A26,FUNCT_2:5; then reconsider j0=p.i0 as Element of NAT; Indices (1.(K,n))=[: Seg n,Seg n:] by A1,MATRIX_0:23; then A64: [i0,j0] in Indices (1.(K,n)) by A25,A26,A63,ZFMISC_1:def 2; i0 <= n by A25,A26,FINSEQ_1:1; then A65: n-'i0 =n-i0 by XREAL_1:233; i0 in dom (Path_matrix(p,(1.(K,n)))) by A25,A26,A22,FINSEQ_1:def 3; then A66: (Path_matrix(p,(1.(K,n)))).i0=(1.(K,n))*(i0,j0) by MATRIX_3:def 7; defpred P5[Nat] means f4.(i0+$1)=0.K; A67: 0n; then not i0+(k+1) in Seg n by FINSEQ_1:1; hence thesis by A62; end; end; hence thesis; end; 1 in Seg n by A1; then A75: f4.1=(Path_matrix(p,(1.(K,n)))).1 by A58,A62; A76: for n3 being Nat st 0 <> n3 & n3 < len (Path_matrix (p,(1.(K,n)))) holds f4.(n3 + 1) = (the multF of K). (f4.n3,(Path_matrix(p,(1.( K,n)))).(n3 + 1)) proof let n3 be Nat; assume that A77: 0 <> n3 and A78: n3 < len (Path_matrix(p,(1.(K,n)))); A79: n3+1<=len (Path_matrix(p,(1.(K,n)))) by A78,NAT_1:13; A80: 0+1<=n3 by A77,NAT_1:13; then A81: n3 in Seg n by A22,A78; 11; reconsider a=f4.(i0-'1) as Element of K; i0 1-1 by A84,XREAL_1:14; then f4.(i0) = (the multF of K). (f4.(i0-'1),(Path_matrix(p,(1. (K,n)))).(i0)) by A76,A86,A87 .= a*(0.K) by A28,A66,A64,MATRIX_1:def 3 .= 0.K; hence P5[0]; end; end; then A88: P5[0]; for k being Nat holds P5[k] from NAT_1:sch 2(A88, A68); then P5[n-'i0]; then f4.(i0+(n-'i0))=0.K; hence thesis by A1,A8,A54,A22,A75,A76,A65,FINSOP_1:2; end; end; hence thesis; end; hence thesis by MATRIX_3:def 8; end; deffunc F3(set) = IFIN(idseq n,$1,1_K,0.K); :: dla rodzin zbir? ??? !!! set F=(the addF of K); set f=Path_product(1.(K,n)); set B=In(Permutations(n),Fin Permutations n); A89: for x being set st x in Fin X holds F3(x) in Y proof let x be set; assume x in Fin X; now per cases; case idseq n in x; then F3(x)=1_K by Def1; hence thesis; end; case not idseq n in x; then F3(x)=0.K by Def1; hence thesis; end; end; hence thesis; end; ex f2 being Function of Fin X,Y st for x being set st x in Fin X holds f2.x = F3(x) from FUNCT_2:sch 11(A89); then consider G0 being Function of Fin X,Y such that A90: for x being set st x in Fin X holds G0.x = F3(x); dom (f2)=Permutations(n) by FUNCT_2:def 1; then A91: dom (Path_product(1.(K,n)))=dom f2 by FUNCT_2:def 1; then A92: Path_product(1.(K,n))=f2 by A5,FUNCT_1:2; A93: for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being Element of X st x in B\B9 holds G0.(B9 \/ {x}) = F.(G0.B9,f.x) proof let B9 be Element of Fin X; assume that B9 c= B and B9 <> {}; thus for x being Element of X st x in B\B9 holds G0.(B9 \/ {x}) = F.(G0.B9 ,f.x) proof let x be Element of X; assume A94: x in B\B9; A95: now assume A96: not idseq n in B9 \/ {x}; thus G0.(B9 \/ {x})=IFIN(idseq n,B9 \/ {.x.},1_K,0.K) by A90 .=0.K by A96,Def1; end; A97: 0.K is_a_unity_wrt F by FVSUM_1:6; A98: now assume A99: not idseq n in B9; thus G0.(B9)=IFIN(idseq n,B9,1_K,0.K) by A90 .=0.K by A99,Def1; end; A100: now assume A101: not idseq n in B9 \/ {x}; then not idseq n in {x} by XBOOLE_0:def 3; then A102: not idseq n=x by TARSKI:def 1; f.x=F2(x) by A3,A92 .=0.K by A102,FUNCOP_1:def 8; hence F.(G0.B9,f.x)=0.K by A98,A97,A101,BINOP_1:3,XBOOLE_0:def 3; end; A103: now assume A104: idseq n in B9; thus G0.(B9)=IFIN(idseq n,B9,1_K,0.K) by A90 .=1_K by A104,Def1; end; A105: now assume idseq n in B9 \/ {x}; then A106: idseq n in B9 or idseq n in {x} by XBOOLE_0:def 3; now per cases by A106,TARSKI:def 1; case A107: idseq n in B9; A108: not x in B9 by A94,XBOOLE_0:def 5; f.x=F2(x) by A3,A92 .=0.K by A107,A108,FUNCOP_1:def 8; hence F.(G0.B9,f.x)=1_K by A103,A97,A107,BINOP_1:3; end; case A109: idseq n=x; f.x=F2(x) by A3,A92 .=1_K by A109,FUNCOP_1:def 8; hence F.(G0.B9,f.x)=1_K by A94,A98,A97,A109,BINOP_1:3 ,XBOOLE_0:def 5; end; end; hence F.(G0.B9,f.x)=1_K; end; now assume A110: idseq n in B9 \/ {x}; thus G0.(B9 \/ {x})=IFIN(idseq n,B9 \/ {.x.},1_K,0.K) by A90 .=1_K by A110,Def1; end; hence thesis by A95,A105,A100; end; end; A111: for x being Element of X holds G0.({x}) = f.x proof let x be Element of X; now per cases; case A112: x=idseq n; then idseq n in {x} by TARSKI:def 1; then A113: IFIN(idseq n,{x},1_K,0.K)=1_K by Def1; f2.x=F2(x) by A3 .=1_K by A112,FUNCOP_1:def 8; hence G0.({.x.})=f2.x by A90,A113; end; case A114: x <> idseq n; then not idseq n in {x} by TARSKI:def 1; then A115: IFIN(idseq n,{x},1_K,0.K)=0.K by Def1; f2.x=F2(x) by A3 .=0.K by A114,FUNCOP_1:def 8; hence G0.({.x.})=f2.x by A90,A115; end; end; hence thesis by A91,A5,FUNCT_1:2; end; A116: for e being Element of Y st e is_a_unity_wrt F holds G0.({}) = e proof let e be Element of Y; assume e is_a_unity_wrt F; then A117: F.(0.K,e)=0.K by BINOP_1:3; 0.K is_a_unity_wrt F by FVSUM_1:6; then A118: F.(0.K,e)=e by BINOP_1:3; IFIN(idseq n,{},1_K,0.K)=0.K by Def1; hence thesis by A90,A117,A118,FINSUB_1:7; end; A119: now assume A120: idseq n in B; thus G0.(B)=IFIN(idseq n,B,1_K,0.K) by A90 .=1_K by A120,Def1; end; S: (idseq n) is Element of Group_of_Perm(n) by MATRIX_1:11; Permutations n in Fin Permutations n by FINSUB_1:def 5; then B=Permutations(n) & (idseq n) in the carrier of Group_of_Perm(n) by S,SUBSET_1:def 8; then (the addF of K) $$ (In(Permutations n,Fin Permutations n), Path_product(1.(K,n)))= 1_K by A119,A116,A111,A93,MATRIX_1:def 13,SETWISEO:def 3; hence thesis by MATRIX_3:def 9; end; definition let n be Nat, K be Field, M be Matrix of n,K; redefine attr M is diagonal means for i,j being Nat st i in Seg n & j in Seg n & i <> j holds M*(i,j) = 0.K; compatibility proof hereby assume A1: M is diagonal; let i, j be Nat; assume that A2: i in Seg n & j in Seg n and A3: i <> j; [i,j] in [:Seg n, Seg n:] by A2,ZFMISC_1:def 2; then [i,j] in Indices M by MATRIX_0:24; hence M*(i,j) = 0.K by A1,A3; end; assume A4: for i,j being Nat st i in Seg n & j in Seg n & i <> j holds M*(i,j) = 0.K; let i,j be Nat; assume that A5: [i,j] in Indices M and A6: M*(i,j) <> 0.K; [i,j] in [:Seg n, Seg n:] by A5,MATRIX_0:24; then i in Seg n & j in Seg n by ZFMISC_1:87; hence thesis by A4,A6; end; end; theorem for K being Field, n being Nat, A being Matrix of n,K st n >=1 & A is diagonal holds Det A = (the multF of K) $$ (diagonal_of_Matrix A) proof let K be Field, n be Nat, A be Matrix of n,K; assume that A1: n>=1 and A2: A is diagonal; set k1=(the multF of K)$$(diagonal_of_Matrix A); set X=Permutations n; set Y=the carrier of K; reconsider p0=idseq n as Permutation of Seg n; A3: len (diagonal_of_Matrix A)=n by MATRIX_3:def 10; deffunc F2(object) = IFEQ(idseq n,$1,k1,0.K); A4: for x being object st x in X holds F2(x) in Y; ex f2 being Function of X,Y st for x being object st x in X holds f2.x = F2(x) from FUNCT_2:sch 2(A4); then consider f2 being Function of X,Y such that A5: for x being object st x in X holds f2.x = F2(x); A6: p0 is even by MATRIX_1:16; A7: for x being object st x in dom (Path_product A) holds (Path_product A).x= f2.x proof let x be object; assume x in dom Path_product A; for p being Element of Permutations n holds f2.p = -((the multF of K) $$ Path_matrix(p,A),p) proof let p be Element of Permutations n; A8: now per cases; suppose p is even; hence -(0.K,p)=(0.K) by MATRIX_1:def 16; end; suppose p is odd; then -(0.K,p)= -(0.K) by MATRIX_1:def 16 .=0.K by RLVECT_1:12; hence -(0.K,p)=0.K; end; end; now per cases; case A9: p=idseq n; A10: for i,j st i in dom ((diagonal_of_Matrix A)) & j=p.i holds ( diagonal_of_Matrix A) .i=(A)*(i,j) proof let i,j; assume that A11: i in dom ((diagonal_of_Matrix A)) and A12: j=p.i; A13: i in Seg n by A3,A11,FINSEQ_1:def 3; then p.i=i by A9,FUNCT_1:17; hence thesis by A12,A13,MATRIX_3:def 10; end; len Permutations n = n by MATRIX_1:9; then A14: -((the multF of K) $$ Path_matrix(p,A),p) = (the multF of K) $$ Path_matrix(p,(A)) by A6,A9,MATRIX_1:def 16; f2.p=F2(p) by A5 .= k1 by A9,FUNCOP_1:def 8; hence thesis by A3,A14,A10,MATRIX_3:def 7; end; case A15: p<>idseq n; reconsider Ab=NAT as non empty set; defpred P3[Nat] means $1 < n implies ex p3 being FinSequence of K st len p3=$1+1 & p3.1=(Path_matrix(p,A)).1 & (for n3 being Nat st 0 <> n3 & n3 < $1+1 & n3 as FinSequence of K; A18: for n3 being Nat st 0 <> n3 & n3 < 0+1 & n3< n holds q3.(n3 + 1) = (the multF of K). (q3.n3,(Path_matrix(p,A)).(n3 + 1)) by NAT_1:13 ; A19: for k being Nat st P3[k] holds P3[k+1] proof let k be Nat; assume A20: P3[k]; now per cases; case A21: k+1 n3 & n3 < k+1 & n3 as FinSequence of K; A29: len q3=(len p3) + len (<*e*>) by FINSEQ_1:22 .=k+1+1 by A22,FINSEQ_1:40; A30: for n3 being Nat st 0 <> n3 & n3 < k+1+1 & n3< n holds q3.(n3 + 1) = (the multF of K). (q3.n3,(Path_matrix(p,(A))).(n3 + 1)) proof let n3 be Nat; assume that A31: 0 <> n3 and A32: n3 < k+1+1 and A33: n3=k+1; A38: n3+1<=k+1+1 by A32,NAT_1:13; A39: n3+1>k+1 by A37,NAT_1:13; then n3+1>=k+1+1 by NAT_1:13; then A40: n3+1=k+1+1 by A38,XXREAL_0:1; 1<=k+1 by NAT_1:12; then A41: k+1 in Seg (k+1); then k+1 in dom p3 by A22,FINSEQ_1:def 3; then A42: q3.(k+1)=p3.(k+1) by FINSEQ_1:def 7; (q3).(n3+1) = (<*e*>).(n3+1 - (k+1)) by A22,A29,A39,A38, FINSEQ_1:24 .= e by A40,FINSEQ_1:def 8; hence thesis by A28,A40,A41,A42; end; end; hence thesis; end; 1<=k+1 by NAT_1:12; then 1 in Seg len p3 by A22; then 1 in dom p3 by FINSEQ_1:def 3; then q3.1=(Path_matrix(p,(A))).1 by A23,FINSEQ_1:def 7; hence thesis by A29,A30; end; case k+1>=n; hence thesis; end; end; hence thesis; end; A43: f2.p=F2(p) by A5 .= 0.K by A15,FUNCOP_1:def 8; n (idseq n).i0 by A15,FUNCT_1:2; A49: i0 in Seg n by A45,A47,MATRIX_1:9; reconsider i0 as Nat by A45,A47; A50: p.i0<>i0 by A46,A47,A48,FUNCT_1:18; p is Permutation of Seg n by MATRIX_1:def 12; then A51: p.i0 in Seg n by A46,A47,FUNCT_2:5; then reconsider j0=p.i0 as Nat; A52: n-1=n-'1 by A1,XREAL_1:233; len q3=1 & q3.1=(Path_matrix(p,A)).1 by FINSEQ_1:40; then A53: P3[0] by A18; for k being Nat holds P3[k] from NAT_1:sch 2(A53, A19); then consider p3 being FinSequence of K such that A54: len p3=n-'1+1 and A55: p3.1=(Path_matrix(p,A)).1 and A56: for n3 being Nat st 0 <> n3 & n3 < n-'1+1 & n3< n holds p3.(n3 + 1) = (the multF of K). (p3.n3,(Path_matrix(p,(A))).(n3 + 1)) by A52,A44; defpred P[set,set] means ($1 in Seg n implies $2=p3.$1)& (not $1 in Seg n implies $2=0.K); A57: for x3 being Element of Ab ex y3 being Element of K st P[x3,y3 ] proof let x3 be Element of Ab; now per cases; case A58: x3 in Seg n; then x3 in dom p3 by A52,A54,FINSEQ_1:def 3; then rng p3 c= the carrier of K & p3.x3 in rng p3 by FINSEQ_1:def 4,FUNCT_1:def 3; hence thesis by A58; end; case not x3 in Seg n; hence thesis; end; end; hence thesis; end; ex f4 being Function of Ab,the carrier of K st for x2 being Element of Ab holds P[x2,f4.x2] from FUNCT_2:sch 3(A57); then consider f4 being sequence of the carrier of K such that A59: for x4 being Element of NAT holds (x4 in Seg n implies f4. x4=p3.x4)& (not x4 in Seg n implies f4.x4=0.K); A60: for n3 being Nat st 0 <> n3 & n3 < len (Path_matrix(p,A)) holds f4.(n3 + 1) = (the multF of K). (f4.n3,(Path_matrix(p,A)).(n3 + 1)) proof let n3 be Nat; assume that A61: 0 <> n3 and A62: n3 < len (Path_matrix(p,A)); A63: n3+1<=len (Path_matrix(p,A)) by A62,NAT_1:13; A64: 0+1<=n3 by A61,NAT_1:13; then A65: n3 in Seg n by A17,A62; 1n; then not i0+(k+1) in Seg n by FINSEQ_1:1; hence thesis by A59; end; end; hence thesis; end; 1 in Seg n by A1; then A79: f4.1=(Path_matrix(p,A)).1 by A55,A59; A80: 1<=i0 by A45,A47,FINSEQ_1:1; now per cases; case i0<=1; then i0=1 by A80,XXREAL_0:1; hence P5[0] by A2,A49,A50,A51,A69,A79; end; case A81: i0>1; reconsider a=f4.(i0-'1) as Element of K; i0 1-1 by A81,XREAL_1:14; then f4.i0 = (the multF of K). (f4.(i0-'1),(Path_matrix(p,A)). i0) by A60,A82,A83 .= a*(0.K) by A2,A49,A50,A51,A69 .= 0.K; hence P5[0]; end; end; then A84: P5[0]; for k being Nat holds P5[k] from NAT_1:sch 2(A84, A71); then P5[n-'i0]; hence thesis by A1,A8,A43,A17,A79,A60,A68,FINSOP_1:2; end; end; hence thesis; end; hence thesis by MATRIX_3:def 8; end; deffunc F3(set) = IFIN(idseq n,$1,k1,0.K); set F=the addF of K; set f=Path_product(A); set B=In(Permutations(n),Fin Permutations n); A85: for x being set st x in Fin X holds F3(x) in Y proof let x be set; assume x in Fin X; per cases; suppose idseq n in x; then F3(x)=k1 by Def1; hence thesis; end; suppose not idseq n in x; then F3(x)=0.K by Def1; hence thesis; end; end; ex f2 being Function of Fin X,Y st for x being set st x in Fin X holds f2.x = F3(x) from FUNCT_2:sch 11(A85); then consider G0 being Function of Fin X,Y such that A86: for x being set st x in Fin X holds G0.x = F3(x); dom (f2)=Permutations(n) by FUNCT_2:def 1; then A87: dom (Path_product A)=dom f2 by FUNCT_2:def 1; then A88: Path_product(A)=f2 by A7,FUNCT_1:2; A89: for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being Element of X st x in B\B9 holds G0.(B9 \/ {x}) = F.(G0.B9,f.x) proof let B9 be Element of Fin X; assume that B9 c= B and B9 <> {}; thus for x being Element of X st x in B\B9 holds G0.(B9 \/ {x}) = F.(G0.B9 ,f.x) proof let x be Element of X; assume A90: x in B\B9; A91: now assume A92: not idseq n in B9 \/ {x}; thus G0.(B9 \/ {x})=IFIN(idseq n,B9 \/ {.x.},k1,0.K) by A86 .=0.K by A92,Def1; end; A93: 0.K is_a_unity_wrt F by FVSUM_1:6; A94: now assume A95: not idseq n in B9; thus G0.(B9)=IFIN(idseq n,B9,k1,0.K) by A86 .=0.K by A95,Def1; end; A96: now assume A97: not idseq n in B9 \/ {x}; then not idseq n in {x} by XBOOLE_0:def 3; then A98: not idseq n=x by TARSKI:def 1; f.x=F2(x) by A5,A88 .=0.K by A98,FUNCOP_1:def 8; hence F.(G0.B9,f.x)=0.K by A94,A93,A97,BINOP_1:3,XBOOLE_0:def 3; end; A99: now assume A100: idseq n in B9; thus G0.(B9)=IFIN(idseq n,B9,k1,0.K) by A86 .=k1 by A100,Def1; end; A101: now assume idseq n in B9 \/ {x}; then A102: idseq n in B9 or idseq n in {x} by XBOOLE_0:def 3; now per cases by A102,TARSKI:def 1; case A103: idseq n in B9; A104: not x in B9 by A90,XBOOLE_0:def 5; f.x=F2(x) by A5,A88 .=0.K by A103,A104,FUNCOP_1:def 8; hence F.(G0.B9,f.x)=k1 by A99,A93,A103,BINOP_1:3; end; case A105: idseq n=x; f.x=F2(x) by A5,A88 .=k1 by A105,FUNCOP_1:def 8; hence F.(G0.B9,f.x)=k1 by A90,A94,A93,A105,BINOP_1:3,XBOOLE_0:def 5 ; end; end; hence F.(G0.B9,f.x)=k1; end; now assume A106: idseq n in B9 \/ {x}; thus G0.(B9 \/ {x})=IFIN(idseq n,B9 \/ {.x.},k1,0.K) by A86 .=k1 by A106,Def1; end; hence thesis by A91,A101,A96; end; end; A107: for x being Element of X holds G0.({x}) = f.x proof let x be Element of X; now per cases; case A108: x=idseq n; then idseq n in {x} by TARSKI:def 1; then A109: IFIN(idseq n,{x},k1,0.K)=k1 by Def1; f2.x=F2(x) by A5 .=k1 by A108,FUNCOP_1:def 8; hence G0.({.x.})=f2.x by A86,A109; end; case A110: x <> idseq n; then not idseq n in {x} by TARSKI:def 1; then A111: IFIN(idseq n,{x},k1,0.K)=0.K by Def1; f2.x=F2(x) by A5 .=0.K by A110,FUNCOP_1:def 8; hence G0.({.x.})=f2.x by A86,A111; end; end; hence thesis by A87,A7,FUNCT_1:2; end; A112: for e being Element of Y st e is_a_unity_wrt F holds G0.({}) = e proof let e be Element of Y; assume e is_a_unity_wrt F; then A113: F.(0.K,e)=0.K by BINOP_1:3; 0.K is_a_unity_wrt F by FVSUM_1:6; then A114: F.(0.K,e)=e by BINOP_1:3; IFIN(idseq n,{},k1,0.K)=0.K by Def1; hence thesis by A86,A113,A114,FINSUB_1:7; end; A115: now assume A116: idseq n in B; thus G0.(B)=IFIN(idseq n,B,k1,0.K) by A86 .=(the multF of K)$$ (diagonal_of_Matrix A) by A116,Def1; end; S: (idseq n) is Element of Group_of_Perm(n) by MATRIX_1:11; Permutations n in Fin Permutations n by FINSUB_1:def 5; then B=Permutations(n) & (idseq n) in the carrier of Group_of_Perm(n) by S,SUBSET_1:def 8; then (the addF of K) $$ (In(Permutations(n),Fin Permutations n), Path_product(A))= (the multF of K)$$ (diagonal_of_Matrix A) by A115,A112,A107,A89,MATRIX_1:def 13 ,SETWISEO:def 3; hence thesis by MATRIX_3:def 9; end; theorem Th18: for p being Element of Permutations(n) holds p" is Element of Permutations(n) proof let p be Element of Permutations(n); p" is Element of Group_of_Perm(n) by MATRIX_1:14; hence thesis by MATRIX_1:def 13; end; definition let n; let p be Element of Permutations(n); redefine func p" -> Element of Permutations(n); coherence by Th18; end; ::$CT theorem for G being Group, f1,f2 being FinSequence of G holds (Product (f1^f2))" = (Product f2)" * (Product f1)" proof let G be Group,f1,f2 be FinSequence of G; thus (Product (f1^f2))" = ((Product f1) * (Product f2))" by GROUP_4:5 .= (Product f2)" * (Product f1)" by GROUP_1:17; end; definition let G be Group, f be FinSequence of G; ::$CD func f" -> FinSequence of G means :Def3: len it = len f & for i being Nat st i in dom f holds it/.i = (f/.i)"; existence proof deffunc F(Nat) = (f/.$1)"; ex p being FinSequence st len p = len f & for k being Nat st k in dom p holds p.k=F(k) from FINSEQ_1:sch 2; then consider p being FinSequence such that A1: len p = len f and A2: for k being Nat st k in dom p holds p.k=F(k); rng p c= the carrier of G proof let y be object; assume y in rng p; then consider x being object such that A3: x in dom p and A4: y=p.x by FUNCT_1:def 3; reconsider k=x as Nat by A3; p.k=(f/.k)" by A2,A3; hence thesis by A4; end; then reconsider q=p as FinSequence of G by FINSEQ_1:def 4; A5: dom p = dom f by A1,FINSEQ_3:29; for i being Nat st i in dom f holds q/.i=(f/.i)" proof let i be Nat; assume A6: i in dom f; hence q/.i=p.i by A5,PARTFUN1:def 6 .=(f/.i)" by A2,A5,A6; end; hence thesis by A1; end; uniqueness proof thus for g1,g2 being FinSequence of G st (len g1=len f & for i being Nat st i in dom f holds g1/.i=(f/.i)")& (len g2=len f & for j being Nat st j in dom f holds g2/.j=(f/.j)") holds g1=g2 proof let g1,g2 be FinSequence of G; assume that A7: len g1=len f and A8: for i being Nat st i in dom f holds g1/.i=(f /.i)" and A9: len g2=len f and A10: for j being Nat st j in dom f holds g2/. j=(f/.j)"; A11: dom g1 = dom f by A7,FINSEQ_3:29; for k being Nat st 1<= k & k<= len g1 holds g1.k=g2.k proof let k be Nat; assume A12: 1<= k & k<= len g1; k in Seg len g2 by A7,A9,A12; then k in dom g2 by FINSEQ_1:def 3; then A13: g2.k=g2/.k by PARTFUN1:def 6; k in Seg len g1 by A12; then A14: k in dom g1 by FINSEQ_1:def 3; then g1.k=g1/.k & g1/.k=(f/.k)" by A8,A11,PARTFUN1:def 6; hence thesis by A10,A11,A14,A13; end; hence thesis by A7,A9; end; end; end; theorem Th20: for G being Group holds (<*>(the carrier of G))"=<*>(the carrier of G) proof let G be Group; len (<*>(the carrier of G))=0; then len ((<*>(the carrier of G))" qua FinSequence of G)=0 by Def3; hence thesis; end; theorem Th21: for G being Group, f,g being FinSequence of G holds (f^g)"=(f")^ (g") proof let G be Group, f,g be FinSequence of G; A1: len ((f^g)")=len (f^g) by Def3 .= len f+len g by FINSEQ_1:22; A2: len f+len g=len (f") +len g by Def3 .=len (f") + len (g") by Def3 .= len ((f")^(g")) by FINSEQ_1:22; A3: len ((f^g)")=len (f^g) by Def3; for i being Nat st 1<=i & i<= len ((f^g)") holds ((f^g)").i=((f")^(g")). i proof let i be Nat; assume that A4: 1<=i and A5: i<= len ((f^g)"); now per cases; case len f>0; A6: len (f")=len f by Def3; len ((f^g)")=len (f^g) by Def3; then A7: dom ((f^g)")=dom (f^g) by FINSEQ_3:29; i in Seg len ((f^g)") by A4,A5; then A8: i in dom ((f^g)") by FINSEQ_1:def 3; then A9: ((f^g)") .i=(((f^g)"))/.i by PARTFUN1:def 6 .= ((f^g)/.i)" by A7,A8,Def3; A10: len (g")=len g by Def3; now per cases; case i<=len f; then A11: i in Seg len f by A4; then A12: i in dom f by FINSEQ_1:def 3; A13: i in dom (f") by A6,A11,FINSEQ_1:def 3; (f^g)/.i=(f^g).i by A7,A8,PARTFUN1:def 6 .=f.i by A12,FINSEQ_1:def 7 .=f/.i by A12,PARTFUN1:def 6; then ((f^g)/.i)" =(f")/.i by A12,Def3 .=(f").i by A13,PARTFUN1:def 6; hence thesis by A9,A13,FINSEQ_1:def 7; end; case A14: i>len f; then 1+len f<=i by NAT_1:13; then A15: 1+len f -len f<=i-len f by XREAL_1:9; A16: i-'len f=i-len f by A14,XREAL_1:233; i-len f <= len g+len f -len f by A1,A5,XREAL_1:9; then A17: i-'len f in Seg len g by A16,A15; then A18: i-'len f in dom g by FINSEQ_1:def 3; A19: i-'len f in dom (g") by A10,A17,FINSEQ_1:def 3; (f^g)/.i=(f^g).i by A7,A8,PARTFUN1:def 6 .=g.(i-len (f)) by A3,A5,A14,FINSEQ_1:24 .=g/.(i-'len f) by A16,A18,PARTFUN1:def 6; then ((f^g)/.i)" =(g")/.(i-'len f) by A18,Def3 .=(g").(i-len (f")) by A6,A16,A19,PARTFUN1:def 6; hence thesis by A1,A2,A5,A6,A9,A14,FINSEQ_1:24; end; end; hence thesis; end; case len f<=0; then f={}; then ((f^g)")=g" & f"=<*>(the carrier of G) by Th20,FINSEQ_1:34; hence thesis by FINSEQ_1:34; end; end; hence thesis; end; hence thesis by A1,A2; end; theorem Th22: for G being Group,a being Element of G holds (<*a*>)" =<* a" *> proof let G be Group,a be Element of G; A1: len ((<*a*>)")=len (<* a *>) by Def3 .=1 by FINSEQ_1:39 .=len (<* a" *>) by FINSEQ_1:39; for i being Nat st 1<=i & i<= len <*a" *> holds ((<*a*>)").i=(<* a" *>). i proof let i be Nat; assume A2: 1<=i & i<= len <*a" *>; A3: len <*a" *>=1 by FINSEQ_1:39; then A4: i=1 by A2,XXREAL_0:1; len (<* a *>) =1 by FINSEQ_1:39; then i in Seg len (<*a*>) by A2,A3; then A5: i in dom (<*a*>) by FINSEQ_1:def 3; i in Seg len ((<*a*>)") by A1,A2; then i in dom ((<*a*>)") by FINSEQ_1:def 3; then A6: ((<*a*>)").i=((<*a*>)")/.i by PARTFUN1:def 6 .= ((<* a *>)/.i)" by A5,Def3; (<* a *>)/.i= ((<* a *>).i) by A5,PARTFUN1:def 6 .= a by A4,FINSEQ_1:40; hence thesis by A4,A6,FINSEQ_1:40; end; hence thesis by A1; end; theorem Th23: for G being Group, f being FinSequence of G holds Product (f^( Rev f)")=1_G proof let G be Group,f be FinSequence of G; defpred P[Nat] means for g being FinSequence of G st len g <=$1 holds Product (g^(Rev g)")=1_G; A1: for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume A2: P[k]; for g being FinSequence of G st len g <= k+1 holds Product (g^(Rev g) ")=1_G proof let g be FinSequence of G; assume A3: len g <= k+1; now per cases by A3,XXREAL_0:1; case len g ^ (<* g/.(k + 1) *>)") =Product (<* g/. (k+1) *>) * Product ((<* g/.(k + 1) *>)") by GROUP_4:5 .=(g/.(k+1))*Product ((<* g/.(k + 1) *>)") by FINSOP_1:11 .=(g/.(k+1))*Product ((<* (g/.(k + 1))" *>)) by Th22 .=(g/.(k+1))*(g/.(k + 1))" by FINSOP_1:11 .=1_G by GROUP_1:def 5; A7: g=h^<* g/.(k+1) *> by A4,FINSEQ_5:21; then Rev g=<* g/.(k+1) *> ^ (Rev h) by FINSEQ_5:63; then (Rev g)"=(<* g/.(k + 1) *>)" ^ (Rev h)" by Th21; then g^(Rev g)"=h^ (<* g/.(k+1) *> ^ ((<* g/.(k + 1) *>)" ^ (Rev h)" )) by A7,FINSEQ_1:32 .=h^ (<* g/.(k+1) *> ^ (<* g/.(k + 1) *>)" ^ (Rev h)") by FINSEQ_1:32; then Product (g^(Rev g)") =Product (h) * Product (<* g/.(k+1) *> ^ ( <* g/.(k + 1) *>)" ^ (Rev h)") by GROUP_4:5 .=Product (h) * (Product (<* g/.(k+1) *> ^ (<* g/.(k + 1) *>)" ) * Product ((Rev h)")) by GROUP_4:5 .=Product (h) * Product ((Rev h)") by A6,GROUP_1:def 4 .=Product (h^((Rev h)")) by GROUP_4:5; hence thesis by A2,A5; end; end; hence thesis; end; hence thesis; end; for g being FinSequence of G st len g <= 0 holds Product (g^(Rev g)")= 1_G proof let g be FinSequence of G; assume len g <= 0; then A8: g=<*>(the carrier of G); then Rev g=<*>(the carrier of G) by FINSEQ_5:79; then (Rev g)" = <*>(the carrier of G) by Th20; then g^(Rev g)"=<*>(the carrier of G) by A8,FINSEQ_1:34; hence thesis by GROUP_4:8; end; then A9: P[0]; for j being Nat holds P[j] from NAT_1:sch 2(A9,A1); then P[len f]; hence thesis; end; theorem Th24: for G being Group,f being FinSequence of G holds Product ((Rev f )" ^f)=1_G proof let G be Group,f be FinSequence of G; A1: len f=len Rev f by FINSEQ_5:def 3; A2: len Rev ((Rev f)")=len ((Rev ((Rev f)"))") by Def3; then A3: dom Rev ((Rev f)")=dom ((Rev ((Rev f)"))") by FINSEQ_3:29; A4: len ((Rev f)") = len Rev ((Rev f)") by FINSEQ_5:def 3; A5: len Rev f = len ((Rev f)") by Def3; then A6: dom Rev f = dom ((Rev f)") by FINSEQ_3:29; for i being Nat st 1<= i & i <= len f holds f.i = ((Rev ((Rev f)") )").i proof let i be Nat; assume that A7: 1<= i and A8: i <= len f; len f-i+1=len f-'i+1 by A8,XREAL_1:233; then reconsider j=len f-i+1 as Nat; A9: i+j=len f+1; A10: i in Seg len f by A7,A8; then A11: i in dom ((Rev ((Rev f)"))") by A1,A5,A4,A2,FINSEQ_1:def 3; i-1>=0 by A7,XREAL_1:48; then len f +0 <=len f+(i-1) by XREAL_1:7; then A12: len f-(i-1)<=len f+(i-1)-(i-1) by XREAL_1:13; len f-i=len f-'i by A8,XREAL_1:233; then len f-i+1>=0+1 by XREAL_1:6; then j in Seg len f by A12; then A13: j in dom ((Rev f)") by A1,A5,FINSEQ_1:def 3; A14: j+i=len f+1; A15: i in dom f by A10,FINSEQ_1:def 3; then f.i=f/.i by PARTFUN1:def 6 .= (Rev f)/.j by A15,A9,FINSEQ_5:66 .= ((Rev f)/.j)"" .= (((Rev f)")/.j)" by A6,A13,Def3 .= ((Rev ((Rev f)"))/.i)" by A1,A5,A13,A14,FINSEQ_5:66 .= ((Rev ((Rev f)"))")/.i by A3,A11,Def3 .=((Rev ((Rev f)"))").i by A11,PARTFUN1:def 6; hence thesis; end; then (Rev ((Rev f)") )"=f by A1,A5,A4,A2; hence thesis by Th23; end; theorem Th25: for G being Group,f being FinSequence of G holds (Product f)" = Product ((Rev f)") proof let G be Group,f be FinSequence of G; Product(f ^ (Rev f)")=1_G by Th23; then A1: (Product f) * Product ((Rev f)") = 1_G by GROUP_4:5; Product((Rev f)" ^ f)=1_G by Th24; then Product ((Rev f)") * (Product f) = 1_G by GROUP_4:5; hence thesis by A1,GROUP_1:5; end; theorem Th26: for ITP being Element of Permutations(n), ITG being Element of Group_of_Perm(n) st ITG=ITP & n>=1 holds ITP"=ITG" proof let ITP be Element of Permutations(n), ITG be Element of Group_of_Perm(n); assume that A1: ITG=ITP and A2: n>=1; reconsider qf=ITP as Function of Seg n,Seg n by MATRIX_1:def 12; dom qf=Seg n by A2,FUNCT_2:def 1; then A3: ITP"*ITP=id Seg n by FUNCT_1:39; ITP is Permutation of Seg n by MATRIX_1:def 12; then rng qf = Seg n by FUNCT_2:def 3; then A4: ITP*ITP"=id Seg n by FUNCT_1:39; reconsider pf=ITP" as Element of Group_of_Perm n by MATRIX_1:def 13; A5: idseq n=1_Group_of_Perm n & ITG*pf=(the multF of (Group_of_Perm(n))).( ITG,pf ) by MATRIX_1:15; A6: pf*ITG=(the multF of (Group_of_Perm(n))).(pf,ITG); (the multF of (Group_of_Perm n)).(ITG,pf)=(ITP")*ITP & (the multF of ( Group_of_Perm n)).(pf,ITG)=ITP*(ITP") by A1,MATRIX_1:def 13; hence thesis by A3,A4,A5,A6,GROUP_1:def 5; end; Lm2: for n being Nat, IT being Element of Permutations(n) st IT is even & n>=1 holds IT" is even proof let n be Nat, IT be Element of Permutations(n); assume that A1: IT is even and A2: n>=1; reconsider ITP=IT as Element of Permutations n; reconsider ITG=ITP as Element of Group_of_Perm n by MATRIX_1:def 13; A3: len Permutations n=n by MATRIX_1:9; then consider l being FinSequence of Group_of_Perm n such that A4: (len l)mod 2=0 and A5: IT=Product l and A6: for i st i in dom l ex q being Element of Permutations n st l.i=q & q is being_transposition by A1; set m=len l; reconsider lv=(Rev l)" as FinSequence of Group_of_Perm n; A7: len l =len Rev l by FINSEQ_5:def 3; then A8: len l=len lv by Def3; A9: for i st i in dom lv ex q2 being Element of Permutations(n) st lv.i=q2 & q2 is being_transposition proof let i; reconsider ii=i as Nat; assume A10: i in dom lv; then A11: i in dom Rev l by A7,A8,FINSEQ_3:29; A12: i in Seg len lv by A10,FINSEQ_1:def 3; then 1<=i by FINSEQ_1:1; then m+1<=m+i by XREAL_1:7; then A13: m+1-i<=m+i-i by XREAL_1:9; i<=m by A8,A12,FINSEQ_1:1; then A14: m-i>=0 by XREAL_1:48; then m-i+1=m-'i+1 by XREAL_0:def 2; then reconsider j=len l-i+1 as Nat; m-i+1>=0+1 by A14,XREAL_1:7; then j in Seg len l by A13; then A15: j in dom l by FINSEQ_1:def 3; then consider q being Element of Permutations n such that A16: l.j=q and A17: q is being_transposition by A6; lv.i=lv/.i by A10,PARTFUN1:def 6; then reconsider qq=lv.i as Element of Permutations(n) by MATRIX_1:def 13; reconsider qqf=qq as Function of Seg n,Seg n by MATRIX_1:def 12; A18: i+j=len l+1; reconsider qf=q as Function of Seg n,Seg n by MATRIX_1:def 12; consider i1,j1 being Nat such that A19: i1 in dom q & j1 in dom q & i1<>j1 & q.i1=j1 & q.j1=i1 and A20: for k being Nat st k <>i1 & k<>j1 & k in dom q holds q.k=k by A17; A21: dom qf=Seg n & dom qqf=Seg n by A2,FUNCT_2:def 1; A22: qq=(Rev l)"/.i by A10,PARTFUN1:def 6 .=((Rev l)/.ii)" by A11,Def3 .=(l/.j)" by A18,A15,FINSEQ_5:66 .=q" by A2,A15,A16,Th26,PARTFUN1:def 6; A23: for k being Nat st k <>j1 & k<>i1 & k in dom qq holds qq.k =k proof let k be Nat; assume that A24: k <>j1 & k<>i1 and A25: k in dom qq; q.k=k by A20,A21,A24,A25; hence thesis by A21,A22,A25,FUNCT_1:32; end; A26: qq=(Rev l)"/.i by A10,PARTFUN1:def 6 .=((Rev l)/.ii)" by A11,Def3 .=(l/.j)" by A18,A15,FINSEQ_5:66 .=q" by A2,A15,A16,Th26,PARTFUN1:def 6; ex i,j st i in dom qq & j in dom qq & i<>j & qq.i=j & qq.j=i & for k st k <>i & k<>j & k in dom qq holds qq.k=k proof take i=i1,j=j1; thus i in dom qq & j in dom qq & i<>j & qq.i=j & qq.j=i by A19,A21,A26, FUNCT_1:32; let k; thus thesis by A23; end; then qq is being_transposition; hence thesis; end; ITG"=ITP" by A2,Th26; then IT"=Product lv by A5,Th25; hence thesis by A3,A4,A8,A9; end; theorem Th27: for n being Nat, IT being Element of Permutations(n) st n>=1 holds IT is even iff IT" is even proof let n be Nat, IT be Element of Permutations(n); assume A1: n>=1; hence IT is even implies IT" is even by Lm2; now assume IT" is even; then IT"" is even by A1,Lm2; hence IT is even by FUNCT_1:43; end; hence thesis; end; theorem Th28: for n being Nat,K being commutative Ring, p being Element of Permutations(n), x being Element of K st n>=1 holds -(x,p) = -(x,p") proof let n be Nat,K be commutative Ring, p be Element of Permutations(n), x be Element of K; assume A1: n>=1; reconsider pf=p as Permutation of Seg n by MATRIX_1:def 12; A2: len ((Permutations(n)))=n by MATRIX_1:9; per cases; suppose p is even; then -(x,p) = x & pf" is even by A1,A2,Th27,MATRIX_1:def 16; hence thesis by A2,MATRIX_1:def 16; end; suppose not p is even; then -(x,p) = -x & not p" is even by A1,Th27,MATRIX_1:def 16; hence thesis by MATRIX_1:def 16; end; end; theorem for K being commutative Ring, f1,f2 being FinSequence of K holds (the multF of K) $$ (f1^f2) = ((the multF of K)$$f1)*((the multF of K)$$f2) by FINSOP_1:5; theorem Th30: for K being commutative Ring,R1,R2 be FinSequence of K st R1,R2 are_fiberwise_equipotent holds (the multF of K)$$ R1 = (the multF of K)$$ R2 proof let K be commutative Ring; defpred P[Nat] means for f,g be FinSequence of K st f,g are_fiberwise_equipotent & len f = $1 holds (the multF of K)$$ f = (the multF of K)$$ g; let R1,R2 be FinSequence of K; assume A1: R1,R2 are_fiberwise_equipotent; A2: len R1 = len R1; A3: for n st P[n] holds P[n+1] proof let n; assume A4: P[n]; reconsider n1=n as Nat; let f,g be FinSequence of K; assume that A5: f,g are_fiberwise_equipotent and A6: len f = n+1; A7: rng f c= the carrier of K by FINSEQ_1:def 4; 0+1<=n+1 by NAT_1:13; then A8: n+1 in dom f by A6,FINSEQ_3:25; then f.(n+1) in rng f by FUNCT_1:def 3; then reconsider a = f.(n+1) as Element of K by A7; rng f = rng g by A5,CLASSES1:75; then a in rng g by A8,FUNCT_1:def 3; then consider m be Nat such that A9: m in dom g and A10: g.m = a by FINSEQ_2:10; A11: g = (g|m)^(g/^m) by RFINSEQ:8; set gg = g/^m, gm = g|m; A12: 1<=m by A9,FINSEQ_3:25; then max(0,m-1) = m-1 by FINSEQ_2:4; then reconsider m1 = m-1 as Nat by FINSEQ_2:5; m in Seg m by A12; then A13: gm.m = a by A9,A10,RFINSEQ:6; A14: m = m1+1; then m1<=m by NAT_1:11; then A15: Seg m1 c= Seg m by FINSEQ_1:5; m<=len g by A9,FINSEQ_3:25; then len gm = m by FINSEQ_1:59; then A16: gm = (gm|m1)^<*a*> by A14,A13,RFINSEQ:7; set fn = f|n1; A17: f = fn ^ <*a*> by A6,RFINSEQ:7; A18: gm|m1 = g|((Seg m)/\(Seg m1)) by RELAT_1:71 .= g|m1 by A15,XBOOLE_1:28; now let x be object; card Coim(f,x) = card Coim(g,x) by A5,CLASSES1:def 10; then card(fn"{x})+card(<*a*>"{x}) = card(((g|m1)^<*a*>^(g/^m))"{x}) by A11,A16,A18,A17,FINSEQ_3:57 .= card(((g|m1)^<*a*>)"{x})+card((g/^m)"{x}) by FINSEQ_3:57 .= card((g|m1)"{x})+card(<*a*>"{x})+card((g/^m)"{x}) by FINSEQ_3:57 .= card((g|m1)"{x})+card((g/^m)"{x})+card(<*a*>"{x}) .= card(((g|m1)^(g/^m))"{x})+card(<*a*>"{x}) by FINSEQ_3:57; hence card Coim(fn,x) = card Coim((g|m1)^(g/^m),x); end; then A19: fn, (g|m1)^(g/^m) are_fiberwise_equipotent by CLASSES1:def 10; len fn = n by A6,FINSEQ_1:59,NAT_1:11; then (the multF of K)$$ fn = (the multF of K)$$((g|m1)^gg) by A4,A19; hence (the multF of K)$$ f = (the multF of K)$$((g|m1)^gg)*(the multF of K) $$ <*a*> by A17,FINSOP_1:5 .= (the multF of K)$$(g|m1)*(the multF of K)$$ gg*(the multF of K)$$ <*a*> by FINSOP_1:5 .= (the multF of K)$$(g|m1)*(the multF of K)$$ <*a*>*(the multF of K) $$ gg by GROUP_1:def 3 .= (the multF of K)$$ gm*(the multF of K)$$ gg by A16,A18,FINSOP_1:5 .= (the multF of K)$$ g by A11,FINSOP_1:5; end; A20: P[0] proof let f,g be FinSequence of K; assume f,g are_fiberwise_equipotent & len f = 0; then A21: len g = 0 & f = <*>(the carrier of K) by RFINSEQ:3; then g = <*>(the carrier of K); hence thesis by A21; end; for n holds P[n] from NAT_1:sch 2(A20,A3); hence thesis by A1,A2; end; theorem Th31: for n being Nat, K being commutative Ring, p being Element of Permutations(n), f,g being FinSequence of K st len f=n & g=f*p holds f,g are_fiberwise_equipotent proof let n be Nat, K be commutative Ring, p be Element of Permutations(n), f,g be FinSequence of K; assume that A1: len f=n and A2: g=f*p; reconsider fp=p as Function of Seg n,Seg n by MATRIX_1:def 12; A3: p is Permutation of Seg n by MATRIX_1:def 12; then A4: rng p=Seg n by FUNCT_2:def 3; rng fp = Seg n by A3,FUNCT_2:def 3; then rng p c= dom f by A1,FINSEQ_1:def 3; then A5: dom (f*p)=dom fp by RELAT_1:27; dom f=Seg n by A1,FINSEQ_1:def 3; hence thesis by A2,A5,A4,CLASSES1:77; end; theorem for n being Nat, K being commutative Ring, p being Element of Permutations(n), f,g being FinSequence of K st n>=1 & len f=n & g=f*p holds ( the multF of K) $$ f = (the multF of K) $$ g by Th30,Th31; theorem Th33: for n being Nat, K being Ring, p being Element of Permutations(n), f being FinSequence of K st n>=1 & len f=n holds f*p is FinSequence of K proof let n be Nat, K be Ring, p be Element of Permutations(n), f be FinSequence of K; assume that A1: n>=1 and A2: len f=n; reconsider q=p as Function of Seg n,Seg n by MATRIX_1:def 12; p is bijective Function of Seg n,Seg n by MATRIX_1:def 12; then rng q = Seg n by FUNCT_2:def 3; then rng p c= dom f by A2,FINSEQ_1:def 3; then dom (f*p)=dom q by RELAT_1:27 .=Seg n by A1,FUNCT_2:def 1; then reconsider h=f*p as FinSequence by FINSEQ_1:def 2; rng h c= rng f & rng f c= the carrier of K by FINSEQ_1:def 4,RELAT_1:26; then rng h c= the carrier of K; hence thesis by FINSEQ_1:def 4; end; theorem Th34: for n being Nat, K being commutative Ring, p being Element of Permutations(n), A being Matrix of n,K st n>=1 holds Path_matrix(p",A@) = ( Path_matrix(p,A))*p" proof let n be Nat, K be commutative Ring,p be Element of Permutations(n), A be Matrix of n,K; set f=(Path_matrix(p,A)); reconsider fp=p" as Function of Seg n,Seg n by MATRIX_1:def 12; reconsider fp0=p as Function of Seg n,Seg n by MATRIX_1:def 12; assume A1: n>=1; then A2: dom fp =Seg n by FUNCT_2:def 1; A3: len (Path_matrix(p,A))=n by MATRIX_3:def 7; then reconsider m=(Path_matrix(p,A))*p" as FinSequence of K by A1,Th33; p" is Permutation of Seg n by MATRIX_1:def 12; then A4: rng fp = Seg n by FUNCT_2:def 3; then rng (p") c= dom f by A3,FINSEQ_1:def 3; then A5: dom (f*p")=dom fp by RELAT_1:27; A6: p is Permutation of Seg n by MATRIX_1:def 12; A7: for i,j st i in dom (m) & j=(p").i holds m.i=(A@)*(i,j) proof let i,j; assume that A8: i in dom (m) and A9: j=(p").i; A10: j in Seg n by A4,A5,A8,A9,FUNCT_1:def 3; then A11: j in dom f by A3,FINSEQ_1:def 3; rng fp0 = Seg n by A6,FUNCT_2:def 3; then i=p.j by A5,A2,A8,A9,FUNCT_1:32; then A12: (Path_matrix(p,A)).j=A*(j,i) by A11,MATRIX_3:def 7; A13: dom A=Seg len A by FINSEQ_1:def 3 .= Seg n by MATRIX_0:def 2; len A=n by MATRIX_0:def 2; then i in Seg width A by A1,A5,A2,A8,MATRIX_0:20; then A14: [j,i] in Indices A by A10,A13,ZFMISC_1:def 2; ((Path_matrix(p,A))*p").i=(Path_matrix(p,A)).((p").i) by A5,A8,FUNCT_1:13; hence thesis by A9,A12,A14,MATRIX_0:def 6; end; n in NAT by ORDINAL1:def 12; then len m=n by A5,A2,FINSEQ_1:def 3; hence thesis by A7,MATRIX_3:def 7; end; theorem Th35: for n being Nat, K being commutative Ring, p being Element of Permutations(n), A being Matrix of n,K st n>=1 holds (Path_product(A@)).(p") = (Path_product(A)).p proof let n be Nat, K be commutative Ring, p be Element of Permutations n, A be Matrix of n,K; assume A1: n>=1; A2: len (Path_matrix(p,A))=n by MATRIX_3:def 7; then reconsider g=Path_matrix(p,A)*(p") as FinSequence of K by A1,Th33; (Path_product(A@)).(p") = -((the multF of K) $$ Path_matrix(p",A@),p") by MATRIX_3:def 8 .= -((the multF of K) $$ g,p") by A1,Th34 .= -((the multF of K) $$ g,p) by A1,Th28 .= -((the multF of K) $$ (Path_matrix(p,A)),p) by A2,Th30,Th31; hence thesis by MATRIX_3:def 8; end; theorem for n being Nat, K being commutative Ring, A being Matrix of n,K st n >=1 holds Det (A) = Det (A@) proof let n be Nat, K be commutative Ring, A be Matrix of n,K; set f=Path_product(A); set f2=Path_product(A@); set F=(the addF of K); set Y=the carrier of K; set X=Permutations(n); set B=In(X,Fin X); set I=(the addF of K) $$ (B,Path_product(A@)); A1: Det A = (the addF of K) $$ (B,Path_product A) by MATRIX_3:def 9; X in Fin X by FINSUB_1:def 5; then A2: B=Permutations(n) by SUBSET_1:def 8; A3: {p" where p is Permutation of Seg n : p in B} c= B proof let z be object; assume z in {p" where p is Permutation of Seg n : p in B}; then ex p being Permutation of Seg n st z=p" & p in B; hence thesis by A2,MATRIX_1:def 12; end; A4: B c= {p" where p is Permutation of Seg n : p in B} proof let z be object; assume z in B; then reconsider q2=z as Permutation of Seg n by A2,MATRIX_1:def 12; set q3=q2"; q3"=q2 & q3 in B by A2,FUNCT_1:43,MATRIX_1:def 12; hence thesis; end; X in Fin X by FINSUB_1:def 5; then A5: B <> {} or F is having_a_unity by SUBSET_1:def 8; then consider G0 being Function of Fin X, Y such that A6: I = G0.B and A7: for e being Element of Y st e is_a_unity_wrt F holds G0.{} = e and A8: for x being Element of X holds G0.{x} = f2.x and A9: for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being Element of X st x in B \ B9 holds G0.(B9 \/ {x}) = F.(G0.B9,f2.x) by SETWISEO:def 3; deffunc F8(set) = G0.{p" where p is Permutation of Seg n : p in $1}; A10: for x2 being set st x2 in Fin X holds F8(x2) in Y proof let x2 be set; assume x2 in Fin X; {p" where p is Permutation of Seg n : p in x2} c= X proof let r be object; assume r in {p" where p is Permutation of Seg n : p in x2}; then ex p being Permutation of Seg n st r=p" & p in x2; hence thesis by MATRIX_1:def 12; end; then {p" where p is Permutation of Seg n : p in x2} is Element of Fin X by FINSUB_1:17; hence thesis by FUNCT_2:5; end; consider G1 being Function of Fin X,Y such that A11: for x5 being set st x5 in Fin X holds G1.x5 = F8(x5) from FUNCT_2: sch 11(A10); assume A12: n>=1; A13: for x being Element of X holds G1.{x} = f.x proof let x be Element of X; reconsider B4={.x.} as Element of Fin X; reconsider q=x as Permutation of Seg n by MATRIX_1:def 12; A14: q" is Element of X by MATRIX_1:def 12; A15: {p" where p is Permutation of Seg n : p in B4} c= {q"} proof let z be object; assume z in {p" where p is Permutation of Seg n : p in B4}; then consider p being Permutation of Seg n such that A16: z=p" and A17: p in B4; p=x by A17,TARSKI:def 1; hence thesis by A16,TARSKI:def 1; end; {q"} c= {p" where p is Permutation of Seg n : p in B4} proof let z be object; assume z in {q"}; then q in B4 & z=q" by TARSKI:def 1; hence thesis; end; then {p" where p is Permutation of Seg n : p in B4}={q"} by A15; then G1.B4=G0.{q"} by A11 .=f2.(q") by A8,A14 .=(Path_product A).q by A12,Th35; hence thesis; end; A18: for B9 being Element of Fin X st B9 c= B & B9 <> {} for x being Element of X st x in B \ B9 holds G1.(B9 \/ {x}) = F.(G1.B9,f.x) proof let B9 be Element of Fin X; assume that A19: B9 c= B and A20: B9 <> {}; thus for x being Element of X st x in B \ B9 holds G1.(B9 \/ {x}) = F.(G1. B9,f.x) proof {p" where p is Permutation of Seg n : p in B9} c= X proof let v be object; assume v in {p" where p is Permutation of Seg n : p in B9}; then ex p being Permutation of Seg n st p"=v & p in B9; hence thesis by MATRIX_1:def 12; end; then reconsider B2={p" where p is Permutation of Seg n : p in B9} as Element of Fin X by FINSUB_1:17; set d = the Element of B9; let x be Element of X; reconsider px=x as Permutation of Seg n by MATRIX_1:def 12; reconsider y=px" as Element of X by MATRIX_1:def 12; A21: B2 \/ {y} c={p" where p is Permutation of Seg n : p in B9 \/ {x}} proof let z be object; assume z in B2 \/ {y}; then A22: z in B2 or z in {y} by XBOOLE_0:def 3; now per cases by A22,TARSKI:def 1; case z in B2; then consider p being Permutation of Seg n such that A23: z=p" and A24: p in B9; p in B9 \/ {x} by A24,XBOOLE_0:def 3; hence thesis by A23; end; case A25: z=y; px in {x} by TARSKI:def 1; then px in B9 \/ {x} by XBOOLE_0:def 3; hence thesis by A25; end; end; hence thesis; end; A26: B2 c= B proof let u be object; assume u in B2; then ex p being Permutation of Seg n st p"=u & p in B9; hence thesis by A2,MATRIX_1:def 12; end; assume x in B \ B9; then A27: not x in B9 by XBOOLE_0:def 5; now assume y in B2; then consider pp being Permutation of Seg n such that A28: y=pp" and A29: pp in B9; px=(pp")" by A28,FUNCT_1:43; hence contradiction by A27,A29,FUNCT_1:43; end; then A30: y in B\B2 by A2,XBOOLE_0:def 5; d in B by A19,A20; then reconsider pd=d as Permutation of Seg n by A2,MATRIX_1:def 12; A31: pd" in B2 by A20; A32: G1.(B9 \/ {.x.})= G0.{p" where p is Permutation of Seg n : p in B9 \/ {x}} & G0.B2=G1.B9 by A11; {p" where p is Permutation of Seg n : p in B9 \/ {x}} c= B2 \/ {y} proof let z be object; assume z in {p" where p is Permutation of Seg n : p in B9 \/ {x}}; then consider p being Permutation of Seg n such that A33: z=p" and A34: p in B9 \/ {x}; now per cases by A34,XBOOLE_0:def 3; case p in B9; hence z in B2 or z in {y} by A33; end; case p in {x}; then p=x by TARSKI:def 1; hence z in B2 or z in {y} by A33,TARSKI:def 1; end; end; hence thesis by XBOOLE_0:def 3; end; then B2 \/ {y} ={p" where p is Permutation of Seg n : p in B9 \/ {x}} by A21; then G0.{p" where p is Permutation of Seg n : p in B9 \/ {x}} = F.(G0.B2 ,f2.y) by A9,A26,A31,A30; hence thesis by A12,A32,Th35; end; end; A35: for e being Element of Y st e is_a_unity_wrt F holds G1.{} = e proof {} is Subset of X by SUBSET_1:1; then reconsider B3={} as Element of Fin X by FINSUB_1:17; let e be Element of Y; {p" where p is Permutation of Seg n : p in B3} c= {} proof let s be object; assume s in {p" where p is Permutation of Seg n : p in B3}; then ex p being Permutation of Seg n st s=p" & p in B3; hence thesis; end; then A36: {p" where p is Permutation of Seg n : p in B3}= {}; assume e is_a_unity_wrt F; then G0.{p" where p is Permutation of Seg n : p in B3}=e by A7,A36; hence thesis by A11; end; G1.B =G0.{p" where p is Permutation of Seg n : p in B} by A11; then I=G1.B by A6,A3,A4,XBOOLE_0:def 10; then (the addF of K) $$ (In(Permutations n,Fin Permutations n), Path_product A) =(the addF of K) $$ (In(Permutations n,Fin Permutations n), Path_product(A@)) by A5,A35,A13,A18,SETWISEO:def 3; hence thesis by A1,MATRIX_3:def 9; end;