:: FINSEQ_4 semantic presentation begin definition let f be Function; let x be set ; predf is_one-to-one_at x means :Def1: :: FINSEQ_4:def 1 f " (Im (f,x)) = {x}; end; :: deftheorem Def1 defines is_one-to-one_at FINSEQ_4:def_1_:_ for f being Function for x being set holds ( f is_one-to-one_at x iff f " (Im (f,x)) = {x} ); theorem Th1: :: FINSEQ_4:1 for f being Function for x being set st f is_one-to-one_at x holds x in dom f proof let f be Function; ::_thesis: for x being set st f is_one-to-one_at x holds x in dom f let x be set ; ::_thesis: ( f is_one-to-one_at x implies x in dom f ) assume f is_one-to-one_at x ; ::_thesis: x in dom f then f " (Im (f,x)) = {x} by Def1; then x in f " (Im (f,x)) by TARSKI:def_1; hence x in dom f by FUNCT_1:def_7; ::_thesis: verum end; theorem Th2: :: FINSEQ_4:2 for f being Function for x being set holds ( f is_one-to-one_at x iff ( x in dom f & f " {(f . x)} = {x} ) ) proof let f be Function; ::_thesis: for x being set holds ( f is_one-to-one_at x iff ( x in dom f & f " {(f . x)} = {x} ) ) let x be set ; ::_thesis: ( f is_one-to-one_at x iff ( x in dom f & f " {(f . x)} = {x} ) ) thus ( f is_one-to-one_at x implies ( x in dom f & f " {(f . x)} = {x} ) ) ::_thesis: ( x in dom f & f " {(f . x)} = {x} implies f is_one-to-one_at x ) proof assume A1: f is_one-to-one_at x ; ::_thesis: ( x in dom f & f " {(f . x)} = {x} ) hence A2: x in dom f by Th1; ::_thesis: f " {(f . x)} = {x} f " (Im (f,x)) = {x} by A1, Def1; hence f " {(f . x)} = {x} by A2, FUNCT_1:59; ::_thesis: verum end; assume ( x in dom f & f " {(f . x)} = {x} ) ; ::_thesis: f is_one-to-one_at x hence f " (Im (f,x)) = {x} by FUNCT_1:59; :: according to FINSEQ_4:def_1 ::_thesis: verum end; theorem Th3: :: FINSEQ_4:3 for f being Function for x being set holds ( f is_one-to-one_at x iff ( x in dom f & ( for z being set st z in dom f & x <> z holds f . x <> f . z ) ) ) proof let f be Function; ::_thesis: for x being set holds ( f is_one-to-one_at x iff ( x in dom f & ( for z being set st z in dom f & x <> z holds f . x <> f . z ) ) ) let x be set ; ::_thesis: ( f is_one-to-one_at x iff ( x in dom f & ( for z being set st z in dom f & x <> z holds f . x <> f . z ) ) ) thus ( f is_one-to-one_at x implies ( x in dom f & ( for z being set st z in dom f & x <> z holds f . x <> f . z ) ) ) ::_thesis: ( x in dom f & ( for z being set st z in dom f & x <> z holds f . x <> f . z ) implies f is_one-to-one_at x ) proof assume A1: f is_one-to-one_at x ; ::_thesis: ( x in dom f & ( for z being set st z in dom f & x <> z holds f . x <> f . z ) ) hence x in dom f by Th1; ::_thesis: for z being set st z in dom f & x <> z holds f . x <> f . z let z be set ; ::_thesis: ( z in dom f & x <> z implies f . x <> f . z ) assume that A2: z in dom f and A3: x <> z and A4: f . x = f . z ; ::_thesis: contradiction f . x in {(f . x)} by TARSKI:def_1; then z in f " {(f . x)} by A2, A4, FUNCT_1:def_7; then z in {x} by A1, Th2; hence contradiction by A3, TARSKI:def_1; ::_thesis: verum end; assume that A5: x in dom f and A6: for z being set st z in dom f & x <> z holds f . x <> f . z and A7: not f is_one-to-one_at x ; ::_thesis: contradiction f " {(f . x)} <> {x} by A5, A7, Th2; then consider y being set such that A8: ( ( y in f " {(f . x)} & not y in {x} ) or ( y in {x} & not y in f " {(f . x)} ) ) by TARSKI:1; f . x in {(f . x)} by TARSKI:def_1; then A9: x in f " {(f . x)} by A5, FUNCT_1:def_7; now__::_thesis:_contradiction percases ( ( y in f " {(f . x)} & not y in {x} ) or ( not y in f " {(f . x)} & y in {x} ) ) by A8; supposeA10: ( y in f " {(f . x)} & not y in {x} ) ; ::_thesis: contradiction then f . y in {(f . x)} by FUNCT_1:def_7; then A11: f . y = f . x by TARSKI:def_1; ( y in dom f & x <> y ) by A10, FUNCT_1:def_7, TARSKI:def_1; hence contradiction by A6, A11; ::_thesis: verum end; suppose ( not y in f " {(f . x)} & y in {x} ) ; ::_thesis: contradiction hence contradiction by A9, TARSKI:def_1; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; theorem :: FINSEQ_4:4 for f being Function holds ( ( for x being set st x in dom f holds f is_one-to-one_at x ) iff f is one-to-one ) proof let f be Function; ::_thesis: ( ( for x being set st x in dom f holds f is_one-to-one_at x ) iff f is one-to-one ) thus ( ( for x being set st x in dom f holds f is_one-to-one_at x ) implies f is one-to-one ) ::_thesis: ( f is one-to-one implies for x being set st x in dom f holds f is_one-to-one_at x ) proof assume A1: for x being set st x in dom f holds f is_one-to-one_at x ; ::_thesis: f is one-to-one let x1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x1 in dom f or not b1 in dom f or not f . x1 = f . b1 or x1 = b1 ) let x2 be set ; ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 ) assume that A2: x1 in dom f and A3: ( x2 in dom f & f . x1 = f . x2 ) ; ::_thesis: x1 = x2 f is_one-to-one_at x1 by A1, A2; hence x1 = x2 by A3, Th3; ::_thesis: verum end; assume A4: f is one-to-one ; ::_thesis: for x being set st x in dom f holds f is_one-to-one_at x let x be set ; ::_thesis: ( x in dom f implies f is_one-to-one_at x ) assume A5: x in dom f ; ::_thesis: f is_one-to-one_at x then for z being set st z in dom f & x <> z holds f . x <> f . z by A4, FUNCT_1:def_4; hence f is_one-to-one_at x by A5, Th3; ::_thesis: verum end; definition let R be Relation; let y be set ; predR just_once_values y means :Def2: :: FINSEQ_4:def 2 card (Coim (R,y)) = 1; end; :: deftheorem Def2 defines just_once_values FINSEQ_4:def_2_:_ for R being Relation for y being set holds ( R just_once_values y iff card (Coim (R,y)) = 1 ); theorem Th5: :: FINSEQ_4:5 for f being Function for y being set st f just_once_values y holds y in rng f proof let f be Function; ::_thesis: for y being set st f just_once_values y holds y in rng f let y be set ; ::_thesis: ( f just_once_values y implies y in rng f ) assume f just_once_values y ; ::_thesis: y in rng f then card (Coim (f,y)) = 1 by Def2; then rng f meets {y} by CARD_1:27, RELAT_1:138; then consider x being set such that A1: x in (rng f) /\ {y} by XBOOLE_0:4; x in {y} by A1, XBOOLE_0:def_4; then y = x by TARSKI:def_1; hence y in rng f by A1, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th6: :: FINSEQ_4:6 for f being Function for y being set holds ( f just_once_values y iff ex x being set st {x} = f " {y} ) proof let f be Function; ::_thesis: for y being set holds ( f just_once_values y iff ex x being set st {x} = f " {y} ) let y be set ; ::_thesis: ( f just_once_values y iff ex x being set st {x} = f " {y} ) thus ( f just_once_values y implies ex x being set st {x} = f " {y} ) ::_thesis: ( ex x being set st {x} = f " {y} implies f just_once_values y ) proof assume A1: f just_once_values y ; ::_thesis: ex x being set st {x} = f " {y} then y in rng f by Th5; then consider x being set such that A2: x in dom f and A3: f . x = y by FUNCT_1:def_3; take x ; ::_thesis: {x} = f " {y} card (Coim (f,y)) = 1 by A1, Def2; then consider z being set such that A4: f " {y} = {z} by CARD_2:42; f . x in {y} by A3, TARSKI:def_1; then x in {z} by A2, A4, FUNCT_1:def_7; hence {x} = f " {y} by A4, TARSKI:def_1; ::_thesis: verum end; assume ex x being set st {x} = f " {y} ; ::_thesis: f just_once_values y hence card (Coim (f,y)) = 1 by CARD_1:30; :: according to FINSEQ_4:def_2 ::_thesis: verum end; theorem Th7: :: FINSEQ_4:7 for f being Function for y being set holds ( f just_once_values y iff ex x being set st ( x in dom f & y = f . x & ( for z being set st z in dom f & z <> x holds f . z <> y ) ) ) proof let f be Function; ::_thesis: for y being set holds ( f just_once_values y iff ex x being set st ( x in dom f & y = f . x & ( for z being set st z in dom f & z <> x holds f . z <> y ) ) ) let y be set ; ::_thesis: ( f just_once_values y iff ex x being set st ( x in dom f & y = f . x & ( for z being set st z in dom f & z <> x holds f . z <> y ) ) ) thus ( f just_once_values y implies ex x being set st ( x in dom f & y = f . x & ( for z being set st z in dom f & z <> x holds f . z <> y ) ) ) ::_thesis: ( ex x being set st ( x in dom f & y = f . x & ( for z being set st z in dom f & z <> x holds f . z <> y ) ) implies f just_once_values y ) proof assume A1: f just_once_values y ; ::_thesis: ex x being set st ( x in dom f & y = f . x & ( for z being set st z in dom f & z <> x holds f . z <> y ) ) then A2: card (Coim (f,y)) = 1 by Def2; y in rng f by A1, Th5; then consider x1 being set such that A3: x1 in dom f and A4: f . x1 = y by FUNCT_1:def_3; f . x1 in {y} by A4, TARSKI:def_1; then A5: x1 in f " {y} by A3, FUNCT_1:def_7; take x1 ; ::_thesis: ( x1 in dom f & y = f . x1 & ( for z being set st z in dom f & z <> x1 holds f . z <> y ) ) thus ( x1 in dom f & y = f . x1 ) by A3, A4; ::_thesis: for z being set st z in dom f & z <> x1 holds f . z <> y let z be set ; ::_thesis: ( z in dom f & z <> x1 implies f . z <> y ) assume that A6: z in dom f and A7: z <> x1 and A8: f . z = y ; ::_thesis: contradiction A9: f " {y} is finite by A2; f . z in {y} by A8, TARSKI:def_1; then z in f " {y} by A6, FUNCT_1:def_7; then {z,x1} c= f " {y} by A5, ZFMISC_1:32; then card {z,x1} <= 1 by A9, A2, NAT_1:43; then 2 <= 1 by A7, CARD_2:57; hence contradiction ; ::_thesis: verum end; given x being set such that A10: x in dom f and A11: y = f . x and A12: for z being set st z in dom f & z <> x holds f . z <> y ; ::_thesis: f just_once_values y A13: {x} = f " {y} proof thus {x} c= f " {y} :: according to XBOOLE_0:def_10 ::_thesis: f " {y} c= {x} proof let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in {x} or x1 in f " {y} ) assume x1 in {x} ; ::_thesis: x1 in f " {y} then A14: x1 = x by TARSKI:def_1; f . x in {y} by A11, TARSKI:def_1; hence x1 in f " {y} by A10, A14, FUNCT_1:def_7; ::_thesis: verum end; let x1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x1 in f " {y} or x1 in {x} ) assume A15: x1 in f " {y} ; ::_thesis: x1 in {x} then f . x1 in {y} by FUNCT_1:def_7; then A16: f . x1 = y by TARSKI:def_1; x1 in dom f by A15, FUNCT_1:def_7; then x1 = x by A12, A16; hence x1 in {x} by TARSKI:def_1; ::_thesis: verum end; card (Coim (f,y)) = 1 by A13, CARD_1:30; hence f just_once_values y by Def2; ::_thesis: verum end; theorem Th8: :: FINSEQ_4:8 for f being Function holds ( f is one-to-one iff for y being set st y in rng f holds f just_once_values y ) proof let f be Function; ::_thesis: ( f is one-to-one iff for y being set st y in rng f holds f just_once_values y ) thus ( f is one-to-one implies for y being set st y in rng f holds f just_once_values y ) ::_thesis: ( ( for y being set st y in rng f holds f just_once_values y ) implies f is one-to-one ) proof assume A1: f is one-to-one ; ::_thesis: for y being set st y in rng f holds f just_once_values y let y be set ; ::_thesis: ( y in rng f implies f just_once_values y ) assume y in rng f ; ::_thesis: f just_once_values y then consider x being set such that A2: ( x in dom f & f . x = y ) by FUNCT_1:def_3; for z being set st z in dom f & z <> x holds f . z <> y by A1, A2, FUNCT_1:def_4; hence f just_once_values y by A2, Th7; ::_thesis: verum end; assume A3: for y being set st y in rng f holds f just_once_values y ; ::_thesis: f is one-to-one let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y ) assume that A4: x in dom f and A5: ( y in dom f & f . x = f . y ) ; ::_thesis: x = y f . x in rng f by A4, FUNCT_1:def_3; then f just_once_values f . x by A3; then consider x1 being set such that A6: {x1} = f " {(f . x)} by Th6; A7: f . x in {(f . x)} by TARSKI:def_1; then A8: y in f " {(f . x)} by A5, FUNCT_1:def_7; x in f " {(f . x)} by A4, A7, FUNCT_1:def_7; then x = x1 by A6, TARSKI:def_1; hence x = y by A6, A8, TARSKI:def_1; ::_thesis: verum end; theorem Th9: :: FINSEQ_4:9 for f being Function for x being set holds ( f is_one-to-one_at x iff ( x in dom f & f just_once_values f . x ) ) proof let f be Function; ::_thesis: for x being set holds ( f is_one-to-one_at x iff ( x in dom f & f just_once_values f . x ) ) let x be set ; ::_thesis: ( f is_one-to-one_at x iff ( x in dom f & f just_once_values f . x ) ) thus ( f is_one-to-one_at x implies ( x in dom f & f just_once_values f . x ) ) ::_thesis: ( x in dom f & f just_once_values f . x implies f is_one-to-one_at x ) proof assume A1: f is_one-to-one_at x ; ::_thesis: ( x in dom f & f just_once_values f . x ) hence x in dom f by Th1; ::_thesis: f just_once_values f . x {x} = f " {(f . x)} by A1, Th2; hence f just_once_values f . x by Th6; ::_thesis: verum end; assume that A2: x in dom f and A3: f just_once_values f . x ; ::_thesis: f is_one-to-one_at x consider z being set such that A4: f " {(f . x)} = {z} by A3, Th6; f . x in {(f . x)} by TARSKI:def_1; then x in {z} by A2, A4, FUNCT_1:def_7; then x = z by TARSKI:def_1; hence f is_one-to-one_at x by A2, A4, Th2; ::_thesis: verum end; definition let f be Function; let y be set ; assume A1: f just_once_values y ; funcf <- y -> set means :Def3: :: FINSEQ_4:def 3 ( it in dom f & f . it = y ); existence ex b1 being set st ( b1 in dom f & f . b1 = y ) proof y in rng f by A1, Th5; then consider x being set such that A2: ( x in dom f & f . x = y ) by FUNCT_1:def_3; take x ; ::_thesis: ( x in dom f & f . x = y ) thus ( x in dom f & f . x = y ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being set st b1 in dom f & f . b1 = y & b2 in dom f & f . b2 = y holds b1 = b2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom f & f . x1 = y & x2 in dom f & f . x2 = y implies x1 = x2 ) assume that A3: ( x1 in dom f & f . x1 = y ) and A4: ( x2 in dom f & f . x2 = y ) ; ::_thesis: x1 = x2 consider x being set such that x in dom f and f . x = y and A5: for z being set st z in dom f & z <> x holds f . z <> y by A1, Th7; x = x1 by A3, A5; hence x1 = x2 by A4, A5; ::_thesis: verum end; end; :: deftheorem Def3 defines <- FINSEQ_4:def_3_:_ for f being Function for y being set st f just_once_values y holds for b3 being set holds ( b3 = f <- y iff ( b3 in dom f & f . b3 = y ) ); theorem :: FINSEQ_4:10 for f being Function for y being set st f just_once_values y holds Im (f,(f <- y)) = {y} proof let f be Function; ::_thesis: for y being set st f just_once_values y holds Im (f,(f <- y)) = {y} let y be set ; ::_thesis: ( f just_once_values y implies Im (f,(f <- y)) = {y} ) assume A1: f just_once_values y ; ::_thesis: Im (f,(f <- y)) = {y} then f <- y in dom f by Def3; hence Im (f,(f <- y)) = {(f . (f <- y))} by FUNCT_1:59 .= {y} by A1, Def3 ; ::_thesis: verum end; theorem Th11: :: FINSEQ_4:11 for f being Function for y being set st f just_once_values y holds f " {y} = {(f <- y)} proof let f be Function; ::_thesis: for y being set st f just_once_values y holds f " {y} = {(f <- y)} let y be set ; ::_thesis: ( f just_once_values y implies f " {y} = {(f <- y)} ) assume A1: f just_once_values y ; ::_thesis: f " {y} = {(f <- y)} then consider x being set such that A2: {x} = f " {y} by Th6; A3: x in f " {y} by A2, ZFMISC_1:31; then f . x in {y} by FUNCT_1:def_7; then A4: f . x = y by TARSKI:def_1; x in dom f by A3, FUNCT_1:def_7; hence f " {y} = {(f <- y)} by A1, A2, A4, Def3; ::_thesis: verum end; theorem :: FINSEQ_4:12 for f being Function for y being set st f is one-to-one & y in rng f holds (f ") . y = f <- y proof let f be Function; ::_thesis: for y being set st f is one-to-one & y in rng f holds (f ") . y = f <- y let y be set ; ::_thesis: ( f is one-to-one & y in rng f implies (f ") . y = f <- y ) assume that A1: f is one-to-one and A2: y in rng f ; ::_thesis: (f ") . y = f <- y consider x being set such that A3: ( x in dom f & f . x = y ) by A2, FUNCT_1:def_3; f just_once_values y by A1, A2, Th8; then x = f <- y by A3, Def3; hence (f ") . y = f <- y by A1, A3, FUNCT_1:32; ::_thesis: verum end; theorem :: FINSEQ_4:13 for f being Function for x being set st f is_one-to-one_at x holds f <- (f . x) = x proof let f be Function; ::_thesis: for x being set st f is_one-to-one_at x holds f <- (f . x) = x let x be set ; ::_thesis: ( f is_one-to-one_at x implies f <- (f . x) = x ) assume f is_one-to-one_at x ; ::_thesis: f <- (f . x) = x then ( x in dom f & f just_once_values f . x ) by Th9; hence f <- (f . x) = x by Def3; ::_thesis: verum end; theorem :: FINSEQ_4:14 for f being Function for y being set st f just_once_values y holds f is_one-to-one_at f <- y proof let f be Function; ::_thesis: for y being set st f just_once_values y holds f is_one-to-one_at f <- y let y be set ; ::_thesis: ( f just_once_values y implies f is_one-to-one_at f <- y ) assume A1: f just_once_values y ; ::_thesis: f is_one-to-one_at f <- y A2: now__::_thesis:_for_x_being_set_st_x_in_dom_f_&_x_<>_f_<-_y_holds_ f_._x_<>_f_._(f_<-_y) let x be set ; ::_thesis: ( x in dom f & x <> f <- y implies f . x <> f . (f <- y) ) assume ( x in dom f & x <> f <- y ) ; ::_thesis: f . x <> f . (f <- y) then f . x <> y by A1, Def3; hence f . x <> f . (f <- y) by A1, Def3; ::_thesis: verum end; f <- y in dom f by A1, Def3; hence f is_one-to-one_at f <- y by A2, Th3; ::_thesis: verum end; definition let D be non empty set ; let d1, d2 be Element of D; :: original: <* redefine func<*d1,d2*> -> FinSequence of D; coherence <*d1,d2*> is FinSequence of D by FINSEQ_2:13; end; definition let D be non empty set ; let d1, d2, d3 be Element of D; :: original: <* redefine func<*d1,d2,d3*> -> FinSequence of D; coherence <*d1,d2,d3*> is FinSequence of D by FINSEQ_2:14; end; theorem :: FINSEQ_4:15 for i being Nat for D being set for P being FinSequence of D st 1 <= i & i <= len P holds P /. i = P . i proof let i be Nat; ::_thesis: for D being set for P being FinSequence of D st 1 <= i & i <= len P holds P /. i = P . i let D be set ; ::_thesis: for P being FinSequence of D st 1 <= i & i <= len P holds P /. i = P . i let P be FinSequence of D; ::_thesis: ( 1 <= i & i <= len P implies P /. i = P . i ) assume ( 1 <= i & i <= len P ) ; ::_thesis: P /. i = P . i then i in dom P by FINSEQ_3:25; hence P /. i = P . i by PARTFUN1:def_6; ::_thesis: verum end; theorem :: FINSEQ_4:16 for D being non empty set for d being Element of D holds <*d*> /. 1 = d proof let D be non empty set ; ::_thesis: for d being Element of D holds <*d*> /. 1 = d let d be Element of D; ::_thesis: <*d*> /. 1 = d A1: 1 in {1} by FINSEQ_1:2; ( dom <*d*> = {1} & <*d*> . 1 = d ) by FINSEQ_1:2, FINSEQ_1:def_8; hence <*d*> /. 1 = d by A1, PARTFUN1:def_6; ::_thesis: verum end; theorem :: FINSEQ_4:17 for D being non empty set for d1, d2 being Element of D holds ( <*d1,d2*> /. 1 = d1 & <*d1,d2*> /. 2 = d2 ) proof let D be non empty set ; ::_thesis: for d1, d2 being Element of D holds ( <*d1,d2*> /. 1 = d1 & <*d1,d2*> /. 2 = d2 ) let d1, d2 be Element of D; ::_thesis: ( <*d1,d2*> /. 1 = d1 & <*d1,d2*> /. 2 = d2 ) set s = <*d1,d2*>; A1: ( <*d1,d2*> . 2 = d2 & 1 in {1,2} ) by FINSEQ_1:2, FINSEQ_1:44; A2: 2 in {1,2} by FINSEQ_1:2; ( dom <*d1,d2*> = {1,2} & <*d1,d2*> . 1 = d1 ) by FINSEQ_1:2, FINSEQ_1:44, FINSEQ_1:89; hence ( <*d1,d2*> /. 1 = d1 & <*d1,d2*> /. 2 = d2 ) by A1, A2, PARTFUN1:def_6; ::_thesis: verum end; theorem :: FINSEQ_4:18 for D being non empty set for d1, d2, d3 being Element of D holds ( <*d1,d2,d3*> /. 1 = d1 & <*d1,d2,d3*> /. 2 = d2 & <*d1,d2,d3*> /. 3 = d3 ) proof let D be non empty set ; ::_thesis: for d1, d2, d3 being Element of D holds ( <*d1,d2,d3*> /. 1 = d1 & <*d1,d2,d3*> /. 2 = d2 & <*d1,d2,d3*> /. 3 = d3 ) let d1, d2, d3 be Element of D; ::_thesis: ( <*d1,d2,d3*> /. 1 = d1 & <*d1,d2,d3*> /. 2 = d2 & <*d1,d2,d3*> /. 3 = d3 ) set s = <*d1,d2,d3*>; A1: ( <*d1,d2,d3*> . 2 = d2 & <*d1,d2,d3*> . 3 = d3 ) by FINSEQ_1:45; A2: ( 1 in {1,2,3} & 2 in {1,2,3} ) by FINSEQ_3:1; A3: 3 in {1,2,3} by FINSEQ_3:1; ( dom <*d1,d2,d3*> = {1,2,3} & <*d1,d2,d3*> . 1 = d1 ) by FINSEQ_1:45, FINSEQ_1:89, FINSEQ_3:1; hence ( <*d1,d2,d3*> /. 1 = d1 & <*d1,d2,d3*> /. 2 = d2 & <*d1,d2,d3*> /. 3 = d3 ) by A1, A2, A3, PARTFUN1:def_6; ::_thesis: verum end; definition let p be FinSequence; let x be set ; funcx .. p -> Element of NAT equals :: FINSEQ_4:def 4 (Sgm (p " {x})) . 1; coherence (Sgm (p " {x})) . 1 is Element of NAT proof set q = Sgm (p " {x}); percases ( not 1 in dom (Sgm (p " {x})) or 1 in dom (Sgm (p " {x})) ) ; suppose not 1 in dom (Sgm (p " {x})) ; ::_thesis: (Sgm (p " {x})) . 1 is Element of NAT then (Sgm (p " {x})) . 1 = 0 by FUNCT_1:def_2; hence (Sgm (p " {x})) . 1 is Element of NAT ; ::_thesis: verum end; supposeA1: 1 in dom (Sgm (p " {x})) ; ::_thesis: (Sgm (p " {x})) . 1 is Element of NAT A2: rng (Sgm (p " {x})) c= NAT by FINSEQ_1:def_4; (Sgm (p " {x})) . 1 in rng (Sgm (p " {x})) by A1, FUNCT_1:def_3; hence (Sgm (p " {x})) . 1 is Element of NAT by A2; ::_thesis: verum end; end; end; end; :: deftheorem defines .. FINSEQ_4:def_4_:_ for p being FinSequence for x being set holds x .. p = (Sgm (p " {x})) . 1; theorem Th19: :: FINSEQ_4:19 for p being FinSequence for x being set st x in rng p holds p . (x .. p) = x proof let p be FinSequence; ::_thesis: for x being set st x in rng p holds p . (x .. p) = x let x be set ; ::_thesis: ( x in rng p implies p . (x .. p) = x ) set q = Sgm (p " {x}); A1: ( p " {x} c= dom p & dom p = Seg (len p) ) by FINSEQ_1:def_3, RELAT_1:132; assume x in rng p ; ::_thesis: p . (x .. p) = x then p " {x} <> {} by FUNCT_1:72; then rng (Sgm (p " {x})) <> {} by A1, FINSEQ_1:def_13; then 1 in dom (Sgm (p " {x})) by FINSEQ_3:32; then A2: (Sgm (p " {x})) . 1 in rng (Sgm (p " {x})) by FUNCT_1:def_3; rng (Sgm (p " {x})) = p " {x} by A1, FINSEQ_1:def_13; then p . (x .. p) in {x} by A2, FUNCT_1:def_7; hence p . (x .. p) = x by TARSKI:def_1; ::_thesis: verum end; theorem Th20: :: FINSEQ_4:20 for p being FinSequence for x being set st x in rng p holds x .. p in dom p proof let p be FinSequence; ::_thesis: for x being set st x in rng p holds x .. p in dom p let x be set ; ::_thesis: ( x in rng p implies x .. p in dom p ) A1: ( p " {x} c= dom p & dom p = Seg (len p) ) by FINSEQ_1:def_3, RELAT_1:132; assume x in rng p ; ::_thesis: x .. p in dom p then p " {x} <> {} by FUNCT_1:72; then rng (Sgm (p " {x})) <> {} by A1, FINSEQ_1:def_13; then 1 in dom (Sgm (p " {x})) by FINSEQ_3:32; then x .. p in rng (Sgm (p " {x})) by FUNCT_1:def_3; then x .. p in p " {x} by A1, FINSEQ_1:def_13; hence x .. p in dom p by FUNCT_1:def_7; ::_thesis: verum end; theorem Th21: :: FINSEQ_4:21 for p being FinSequence for x being set st x in rng p holds ( 1 <= x .. p & x .. p <= len p ) proof let p be FinSequence; ::_thesis: for x being set st x in rng p holds ( 1 <= x .. p & x .. p <= len p ) let x be set ; ::_thesis: ( x in rng p implies ( 1 <= x .. p & x .. p <= len p ) ) assume x in rng p ; ::_thesis: ( 1 <= x .. p & x .. p <= len p ) then x .. p in dom p by Th20; hence ( 1 <= x .. p & x .. p <= len p ) by FINSEQ_3:25; ::_thesis: verum end; theorem Th22: :: FINSEQ_4:22 for p being FinSequence for x being set st x in rng p holds ( (x .. p) - 1 is Element of NAT & (len p) - (x .. p) is Element of NAT ) proof let p be FinSequence; ::_thesis: for x being set st x in rng p holds ( (x .. p) - 1 is Element of NAT & (len p) - (x .. p) is Element of NAT ) let x be set ; ::_thesis: ( x in rng p implies ( (x .. p) - 1 is Element of NAT & (len p) - (x .. p) is Element of NAT ) ) assume x in rng p ; ::_thesis: ( (x .. p) - 1 is Element of NAT & (len p) - (x .. p) is Element of NAT ) then ( 1 <= x .. p & x .. p <= len p ) by Th21; hence ( (x .. p) - 1 is Element of NAT & (len p) - (x .. p) is Element of NAT ) by INT_1:5; ::_thesis: verum end; theorem Th23: :: FINSEQ_4:23 for p being FinSequence for x being set st x in rng p holds x .. p in p " {x} proof let p be FinSequence; ::_thesis: for x being set st x in rng p holds x .. p in p " {x} let x be set ; ::_thesis: ( x in rng p implies x .. p in p " {x} ) assume A1: x in rng p ; ::_thesis: x .. p in p " {x} then p . (x .. p) = x by Th19; then A2: p . (x .. p) in {x} by TARSKI:def_1; x .. p in dom p by A1, Th20; hence x .. p in p " {x} by A2, FUNCT_1:def_7; ::_thesis: verum end; theorem Th24: :: FINSEQ_4:24 for p being FinSequence for x being set for k being Nat st k in dom p & k < x .. p holds p . k <> x proof let p be FinSequence; ::_thesis: for x being set for k being Nat st k in dom p & k < x .. p holds p . k <> x let x be set ; ::_thesis: for k being Nat st k in dom p & k < x .. p holds p . k <> x let k be Nat; ::_thesis: ( k in dom p & k < x .. p implies p . k <> x ) set q = Sgm (p " {x}); assume that A1: k in dom p and A2: k < x .. p and A3: p . k = x ; ::_thesis: contradiction A4: x in {x} by TARSKI:def_1; A5: ( p " {x} c= dom p & dom p = Seg (len p) ) by FINSEQ_1:def_3, RELAT_1:132; then rng (Sgm (p " {x})) = p " {x} by FINSEQ_1:def_13; then k in rng (Sgm (p " {x})) by A1, A3, A4, FUNCT_1:def_7; then consider y being set such that A6: y in dom (Sgm (p " {x})) and A7: (Sgm (p " {x})) . y = k by FUNCT_1:def_3; reconsider y = y as Element of NAT by A6; A8: now__::_thesis:_1_<_y assume not 1 < y ; ::_thesis: contradiction then ( 1 = y or y < 1 ) by XXREAL_0:1; hence contradiction by A2, A6, A7, FINSEQ_3:24, NAT_1:14; ::_thesis: verum end; dom (Sgm (p " {x})) = Seg (len (Sgm (p " {x}))) by FINSEQ_1:def_3; then y <= len (Sgm (p " {x})) by A6, FINSEQ_1:1; hence contradiction by A2, A5, A7, A8, FINSEQ_1:def_13; ::_thesis: verum end; theorem Th25: :: FINSEQ_4:25 for p being FinSequence for x being set st p just_once_values x holds p <- x = x .. p proof let p be FinSequence; ::_thesis: for x being set st p just_once_values x holds p <- x = x .. p let x be set ; ::_thesis: ( p just_once_values x implies p <- x = x .. p ) assume A1: p just_once_values x ; ::_thesis: p <- x = x .. p then x in rng p by Th5; then ( x .. p in dom p & p . (x .. p) = x ) by Th19, Th20; hence p <- x = x .. p by A1, Def3; ::_thesis: verum end; theorem Th26: :: FINSEQ_4:26 for p being FinSequence for x being set st p just_once_values x holds for k being Nat st k in dom p & k <> x .. p holds p . k <> x proof let p be FinSequence; ::_thesis: for x being set st p just_once_values x holds for k being Nat st k in dom p & k <> x .. p holds p . k <> x let x be set ; ::_thesis: ( p just_once_values x implies for k being Nat st k in dom p & k <> x .. p holds p . k <> x ) assume A1: p just_once_values x ; ::_thesis: for k being Nat st k in dom p & k <> x .. p holds p . k <> x let k be Nat; ::_thesis: ( k in dom p & k <> x .. p implies p . k <> x ) assume A2: ( k in dom p & k <> x .. p & p . k = x ) ; ::_thesis: contradiction p <- x = x .. p by A1, Th25; hence contradiction by A1, A2, Def3; ::_thesis: verum end; theorem Th27: :: FINSEQ_4:27 for p being FinSequence for x being set st x in rng p & ( for k being Nat st k in dom p & k <> x .. p holds p . k <> x ) holds p just_once_values x proof let p be FinSequence; ::_thesis: for x being set st x in rng p & ( for k being Nat st k in dom p & k <> x .. p holds p . k <> x ) holds p just_once_values x let x be set ; ::_thesis: ( x in rng p & ( for k being Nat st k in dom p & k <> x .. p holds p . k <> x ) implies p just_once_values x ) assume that A1: x in rng p and A2: for k being Nat st k in dom p & k <> x .. p holds p . k <> x ; ::_thesis: p just_once_values x A3: for z being set st z in dom p & z <> x .. p holds p . z <> x by A2; ( p . (x .. p) = x & x .. p in dom p ) by A1, Th19, Th20; hence p just_once_values x by A3, Th7; ::_thesis: verum end; theorem Th28: :: FINSEQ_4:28 for p being FinSequence for x being set holds ( p just_once_values x iff ( x in rng p & {(x .. p)} = p " {x} ) ) proof let p be FinSequence; ::_thesis: for x being set holds ( p just_once_values x iff ( x in rng p & {(x .. p)} = p " {x} ) ) let x be set ; ::_thesis: ( p just_once_values x iff ( x in rng p & {(x .. p)} = p " {x} ) ) thus ( p just_once_values x implies ( x in rng p & {(x .. p)} = p " {x} ) ) ::_thesis: ( x in rng p & {(x .. p)} = p " {x} implies p just_once_values x ) proof assume A1: p just_once_values x ; ::_thesis: ( x in rng p & {(x .. p)} = p " {x} ) then x .. p = p <- x by Th25; hence ( x in rng p & {(x .. p)} = p " {x} ) by A1, Th5, Th11; ::_thesis: verum end; assume that A2: x in rng p and A3: {(x .. p)} = p " {x} ; ::_thesis: p just_once_values x A4: now__::_thesis:_for_z_being_set_st_z_in_dom_p_&_z_<>_x_.._p_holds_ not_p_._z_=_x let z be set ; ::_thesis: ( z in dom p & z <> x .. p implies not p . z = x ) assume that A5: z in dom p and A6: z <> x .. p and A7: p . z = x ; ::_thesis: contradiction p . z in {x} by A7, TARSKI:def_1; then z in p " {x} by A5, FUNCT_1:def_7; hence contradiction by A3, A6, TARSKI:def_1; ::_thesis: verum end; ( p . (x .. p) = x & x .. p in dom p ) by A2, Th19, Th20; hence p just_once_values x by A4, Th7; ::_thesis: verum end; theorem :: FINSEQ_4:29 for p being FinSequence for x being set st p is one-to-one & x in rng p holds {(x .. p)} = p " {x} proof let p be FinSequence; ::_thesis: for x being set st p is one-to-one & x in rng p holds {(x .. p)} = p " {x} let x be set ; ::_thesis: ( p is one-to-one & x in rng p implies {(x .. p)} = p " {x} ) assume that A1: p is one-to-one and A2: x in rng p ; ::_thesis: {(x .. p)} = p " {x} thus {(x .. p)} c= p " {x} :: according to XBOOLE_0:def_10 ::_thesis: p " {x} c= {(x .. p)} proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {(x .. p)} or y in p " {x} ) assume y in {(x .. p)} ; ::_thesis: y in p " {x} then y = x .. p by TARSKI:def_1; hence y in p " {x} by A2, Th23; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in p " {x} or y in {(x .. p)} ) assume A3: y in p " {x} ; ::_thesis: y in {(x .. p)} then A4: y in dom p by FUNCT_1:def_7; p . y in {x} by A3, FUNCT_1:def_7; then A5: p . y = x by TARSKI:def_1; ( p . (x .. p) = x & x .. p in dom p ) by A2, Th19, Th20; then x .. p = y by A1, A4, A5, FUNCT_1:def_4; hence y in {(x .. p)} by TARSKI:def_1; ::_thesis: verum end; theorem Th30: :: FINSEQ_4:30 for p being FinSequence for x being set holds ( p just_once_values x iff len (p - {x}) = (len p) - 1 ) proof let p be FinSequence; ::_thesis: for x being set holds ( p just_once_values x iff len (p - {x}) = (len p) - 1 ) let x be set ; ::_thesis: ( p just_once_values x iff len (p - {x}) = (len p) - 1 ) thus ( p just_once_values x implies len (p - {x}) = (len p) - 1 ) ::_thesis: ( len (p - {x}) = (len p) - 1 implies p just_once_values x ) proof assume p just_once_values x ; ::_thesis: len (p - {x}) = (len p) - 1 then ( len (p - {x}) = (len p) - (card (p " {x})) & p " {x} = {(x .. p)} ) by Th28, FINSEQ_3:59; hence len (p - {x}) = (len p) - 1 by CARD_1:30; ::_thesis: verum end; A1: p " {x} = Coim (p,x) ; assume len (p - {x}) = (len p) - 1 ; ::_thesis: p just_once_values x then (len p) + (- 1) = (len p) - (card (p " {x})) by FINSEQ_3:59 .= (len p) + (- (card (p " {x}))) ; hence p just_once_values x by A1, Def2; ::_thesis: verum end; theorem Th31: :: FINSEQ_4:31 for p being FinSequence for x being set st p just_once_values x holds for k being Nat st k in dom (p - {x}) holds ( ( k < x .. p implies (p - {x}) . k = p . k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) ) proof let p be FinSequence; ::_thesis: for x being set st p just_once_values x holds for k being Nat st k in dom (p - {x}) holds ( ( k < x .. p implies (p - {x}) . k = p . k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) ) let x be set ; ::_thesis: ( p just_once_values x implies for k being Nat st k in dom (p - {x}) holds ( ( k < x .. p implies (p - {x}) . k = p . k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) ) ) assume A1: p just_once_values x ; ::_thesis: for k being Nat st k in dom (p - {x}) holds ( ( k < x .. p implies (p - {x}) . k = p . k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) ) set q = p - {x}; let k be Nat; ::_thesis: ( k in dom (p - {x}) implies ( ( k < x .. p implies (p - {x}) . k = p . k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) ) ) assume A2: k in dom (p - {x}) ; ::_thesis: ( ( k < x .. p implies (p - {x}) . k = p . k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) ) set A = { L where L is Element of NAT : ( L in dom p & L <= k & p . L in {x} ) } ; A3: dom (p - {x}) c= dom p by FINSEQ_3:63; thus ( k < x .. p implies (p - {x}) . k = p . k ) ::_thesis: ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) proof assume A4: k < x .. p ; ::_thesis: (p - {x}) . k = p . k { L where L is Element of NAT : ( L in dom p & L <= k & p . L in {x} ) } c= {} proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { L where L is Element of NAT : ( L in dom p & L <= k & p . L in {x} ) } or y in {} ) assume y in { L where L is Element of NAT : ( L in dom p & L <= k & p . L in {x} ) } ; ::_thesis: y in {} then consider L being Element of NAT such that y = L and A5: ( L in dom p & L <= k ) and A6: p . L in {x} ; p . L <> x by A1, A4, A5, Th26; hence y in {} by A6, TARSKI:def_1; ::_thesis: verum end; then A7: { L where L is Element of NAT : ( L in dom p & L <= k & p . L in {x} ) } = {} ; p . k <> x by A1, A2, A3, A4, Th26; then not p . k in {x} by TARSKI:def_1; then (p - {x}) . (k - 0) = p . k by A2, A3, A7, CARD_1:27, FINSEQ_3:85; hence (p - {x}) . k = p . k ; ::_thesis: verum end; set B = { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } ; assume A8: x .. p <= k ; ::_thesis: (p - {x}) . k = p . (k + 1) A9: x in rng p by A1, Th5; A10: { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } = {(x .. p)} proof thus { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } c= {(x .. p)} :: according to XBOOLE_0:def_10 ::_thesis: {(x .. p)} c= { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } or y in {(x .. p)} ) assume y in { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } ; ::_thesis: y in {(x .. p)} then consider M being Element of NAT such that A11: M = y and A12: M in dom p and M <= k + 1 and A13: p . M in {x} ; p . M = x by A13, TARSKI:def_1; then M = x .. p by A1, A12, Th26; hence y in {(x .. p)} by A11, TARSKI:def_1; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {(x .. p)} or y in { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } ) assume y in {(x .. p)} ; ::_thesis: y in { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } then A14: y = x .. p by TARSKI:def_1; p . (x .. p) = x by A9, Th19; then A15: p . (x .. p) in {x} by TARSKI:def_1; ( x .. p in dom p & x .. p <= k + 1 ) by A9, A8, Th20, NAT_1:12; hence y in { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } by A14, A15; ::_thesis: verum end; then reconsider B = { M where M is Element of NAT : ( M in dom p & M <= k + 1 & p . M in {x} ) } as finite set ; ( dom (p - {x}) = Seg (len (p - {x})) & len (p - {x}) = (len p) - 1 ) by A1, Th30, FINSEQ_1:def_3; then k <= (len p) - 1 by A2, FINSEQ_1:1; then ( 1 <= k + 1 & k + 1 <= len p ) by NAT_1:12, XREAL_1:19; then k + 1 in Seg (len p) ; then A16: k + 1 in dom p by FINSEQ_1:def_3; now__::_thesis:_not_p_._(k_+_1)_in_{x} x .. p <> k + 1 by A8, XREAL_1:29; then A17: p . (k + 1) <> x by A1, A16, Th26; assume p . (k + 1) in {x} ; ::_thesis: contradiction hence contradiction by A17, TARSKI:def_1; ::_thesis: verum end; then (p - {x}) . ((k + 1) - (card B)) = p . (k + 1) by A16, FINSEQ_3:85; then (p - {x}) . ((k + 1) - 1) = p . (k + 1) by A10, CARD_1:30; hence (p - {x}) . k = p . (k + 1) ; ::_thesis: verum end; theorem :: FINSEQ_4:32 for p being FinSequence for x being set st p is one-to-one & x in rng p holds for k being Nat st k in dom (p - {x}) holds ( ( (p - {x}) . k = p . k implies k < x .. p ) & ( k < x .. p implies (p - {x}) . k = p . k ) & ( (p - {x}) . k = p . (k + 1) implies x .. p <= k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) ) proof let p be FinSequence; ::_thesis: for x being set st p is one-to-one & x in rng p holds for k being Nat st k in dom (p - {x}) holds ( ( (p - {x}) . k = p . k implies k < x .. p ) & ( k < x .. p implies (p - {x}) . k = p . k ) & ( (p - {x}) . k = p . (k + 1) implies x .. p <= k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) ) let x be set ; ::_thesis: ( p is one-to-one & x in rng p implies for k being Nat st k in dom (p - {x}) holds ( ( (p - {x}) . k = p . k implies k < x .. p ) & ( k < x .. p implies (p - {x}) . k = p . k ) & ( (p - {x}) . k = p . (k + 1) implies x .. p <= k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) ) ) assume that A1: p is one-to-one and A2: x in rng p ; ::_thesis: for k being Nat st k in dom (p - {x}) holds ( ( (p - {x}) . k = p . k implies k < x .. p ) & ( k < x .. p implies (p - {x}) . k = p . k ) & ( (p - {x}) . k = p . (k + 1) implies x .. p <= k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) ) set q = p - {x}; let k be Nat; ::_thesis: ( k in dom (p - {x}) implies ( ( (p - {x}) . k = p . k implies k < x .. p ) & ( k < x .. p implies (p - {x}) . k = p . k ) & ( (p - {x}) . k = p . (k + 1) implies x .. p <= k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) ) ) assume A3: k in dom (p - {x}) ; ::_thesis: ( ( (p - {x}) . k = p . k implies k < x .. p ) & ( k < x .. p implies (p - {x}) . k = p . k ) & ( (p - {x}) . k = p . (k + 1) implies x .. p <= k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) ) A4: p just_once_values x by A1, A2, Th8; then ( dom (p - {x}) = Seg (len (p - {x})) & len (p - {x}) = (len p) - 1 ) by Th30, FINSEQ_1:def_3; then k <= (len p) - 1 by A3, FINSEQ_1:1; then ( 1 <= k + 1 & k + 1 <= len p ) by NAT_1:12, XREAL_1:19; then k + 1 in Seg (len p) ; then A5: ( dom (p - {x}) c= dom p & k + 1 in dom p ) by FINSEQ_1:def_3, FINSEQ_3:63; thus ( (p - {x}) . k = p . k implies k < x .. p ) ::_thesis: ( ( k < x .. p implies (p - {x}) . k = p . k ) & ( (p - {x}) . k = p . (k + 1) implies x .. p <= k ) & ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) ) proof assume that A6: (p - {x}) . k = p . k and A7: not k < x .. p ; ::_thesis: contradiction (p - {x}) . k = p . (k + 1) by A4, A3, A7, Th31; then k + 0 = k + 1 by A1, A3, A5, A6, FUNCT_1:def_4; hence contradiction ; ::_thesis: verum end; thus ( k < x .. p implies (p - {x}) . k = p . k ) by A4, A3, Th31; ::_thesis: ( (p - {x}) . k = p . (k + 1) iff x .. p <= k ) thus ( (p - {x}) . k = p . (k + 1) implies x .. p <= k ) ::_thesis: ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) proof assume A8: (p - {x}) . k = p . (k + 1) ; ::_thesis: x .. p <= k assume not x .. p <= k ; ::_thesis: contradiction then p . (k + 1) = p . k by A4, A3, A8, Th31; then k + 0 = k + 1 by A1, A3, A5, FUNCT_1:def_4; hence contradiction ; ::_thesis: verum end; thus ( x .. p <= k implies (p - {x}) . k = p . (k + 1) ) by A4, A3, Th31; ::_thesis: verum end; definition let p be FinSequence; let x be set ; assume A1: x in rng p ; funcp -| x -> FinSequence means :Def5: :: FINSEQ_4:def 5 ex n being Nat st ( n = (x .. p) - 1 & it = p | (Seg n) ); existence ex b1 being FinSequence ex n being Nat st ( n = (x .. p) - 1 & b1 = p | (Seg n) ) proof reconsider n = (x .. p) - 1 as Element of NAT by A1, Th22; reconsider q = p | (Seg n) as FinSequence by FINSEQ_1:15; take q ; ::_thesis: ex n being Nat st ( n = (x .. p) - 1 & q = p | (Seg n) ) thus ex n being Nat st ( n = (x .. p) - 1 & q = p | (Seg n) ) ; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence st ex n being Nat st ( n = (x .. p) - 1 & b1 = p | (Seg n) ) & ex n being Nat st ( n = (x .. p) - 1 & b2 = p | (Seg n) ) holds b1 = b2 ; end; :: deftheorem Def5 defines -| FINSEQ_4:def_5_:_ for p being FinSequence for x being set st x in rng p holds for b3 being FinSequence holds ( b3 = p -| x iff ex n being Nat st ( n = (x .. p) - 1 & b3 = p | (Seg n) ) ); theorem Th33: :: FINSEQ_4:33 for p being FinSequence for x being set for n being Nat st x in rng p & n = (x .. p) - 1 holds p | (Seg n) = p -| x proof let p be FinSequence; ::_thesis: for x being set for n being Nat st x in rng p & n = (x .. p) - 1 holds p | (Seg n) = p -| x let x be set ; ::_thesis: for n being Nat st x in rng p & n = (x .. p) - 1 holds p | (Seg n) = p -| x let n be Nat; ::_thesis: ( x in rng p & n = (x .. p) - 1 implies p | (Seg n) = p -| x ) assume x in rng p ; ::_thesis: ( not n = (x .. p) - 1 or p | (Seg n) = p -| x ) then ex m being Nat st ( m = (x .. p) - 1 & p | (Seg m) = p -| x ) by Def5; hence ( not n = (x .. p) - 1 or p | (Seg n) = p -| x ) ; ::_thesis: verum end; theorem Th34: :: FINSEQ_4:34 for p being FinSequence for x being set st x in rng p holds len (p -| x) = (x .. p) - 1 proof let p be FinSequence; ::_thesis: for x being set st x in rng p holds len (p -| x) = (x .. p) - 1 let x be set ; ::_thesis: ( x in rng p implies len (p -| x) = (x .. p) - 1 ) assume A1: x in rng p ; ::_thesis: len (p -| x) = (x .. p) - 1 then consider n being Nat such that A2: n = (x .. p) - 1 and A3: p | (Seg n) = p -| x by Def5; A4: n <= n + 1 by NAT_1:12; n + 1 <= len p by A1, A2, Th21; then n <= len p by A4, XXREAL_0:2; hence len (p -| x) = (x .. p) - 1 by A2, A3, FINSEQ_1:17; ::_thesis: verum end; theorem Th35: :: FINSEQ_4:35 for p being FinSequence for x being set for n being Nat st x in rng p & n = (x .. p) - 1 holds dom (p -| x) = Seg n proof let p be FinSequence; ::_thesis: for x being set for n being Nat st x in rng p & n = (x .. p) - 1 holds dom (p -| x) = Seg n let x be set ; ::_thesis: for n being Nat st x in rng p & n = (x .. p) - 1 holds dom (p -| x) = Seg n let n be Nat; ::_thesis: ( x in rng p & n = (x .. p) - 1 implies dom (p -| x) = Seg n ) assume x in rng p ; ::_thesis: ( not n = (x .. p) - 1 or dom (p -| x) = Seg n ) then len (p -| x) = (x .. p) - 1 by Th34; hence ( not n = (x .. p) - 1 or dom (p -| x) = Seg n ) by FINSEQ_1:def_3; ::_thesis: verum end; theorem Th36: :: FINSEQ_4:36 for p being FinSequence for x being set for k being Nat st x in rng p & k in dom (p -| x) holds p . k = (p -| x) . k proof let p be FinSequence; ::_thesis: for x being set for k being Nat st x in rng p & k in dom (p -| x) holds p . k = (p -| x) . k let x be set ; ::_thesis: for k being Nat st x in rng p & k in dom (p -| x) holds p . k = (p -| x) . k let k be Nat; ::_thesis: ( x in rng p & k in dom (p -| x) implies p . k = (p -| x) . k ) assume that A1: x in rng p and A2: k in dom (p -| x) ; ::_thesis: p . k = (p -| x) . k ex n being Nat st ( n = (x .. p) - 1 & p | (Seg n) = p -| x ) by A1, Def5; hence p . k = (p -| x) . k by A2, FUNCT_1:47; ::_thesis: verum end; theorem Th37: :: FINSEQ_4:37 for p being FinSequence for x being set st x in rng p holds not x in rng (p -| x) proof let p be FinSequence; ::_thesis: for x being set st x in rng p holds not x in rng (p -| x) let x be set ; ::_thesis: ( x in rng p implies not x in rng (p -| x) ) assume that A1: x in rng p and A2: x in rng (p -| x) ; ::_thesis: contradiction reconsider n = (x .. p) - 1 as Element of NAT by A1, Th22; set r = p | (Seg n); A3: p | (Seg n) = p -| x by A1, Th33; then consider y being set such that A4: y in dom (p | (Seg n)) and A5: (p | (Seg n)) . y = x by A2, FUNCT_1:def_3; A6: dom (p | (Seg n)) = Seg n by A1, A3, Th35; then reconsider y = y as Element of NAT by A4; y <= n by A4, A6, FINSEQ_1:1; then A7: y + 1 <= x .. p by XREAL_1:19; y < y + 1 by XREAL_1:29; then ( dom (p | (Seg n)) c= dom p & y < x .. p ) by A7, RELAT_1:60, XXREAL_0:2; then p . y <> x by A4, Th24; hence contradiction by A4, A5, FUNCT_1:47; ::_thesis: verum end; theorem :: FINSEQ_4:38 for p being FinSequence for x being set st x in rng p holds rng (p -| x) misses {x} proof let p be FinSequence; ::_thesis: for x being set st x in rng p holds rng (p -| x) misses {x} let x be set ; ::_thesis: ( x in rng p implies rng (p -| x) misses {x} ) assume x in rng p ; ::_thesis: rng (p -| x) misses {x} then not x in rng (p -| x) by Th37; then for y being set st y in rng (p -| x) holds not y in {x} by TARSKI:def_1; hence rng (p -| x) misses {x} by XBOOLE_0:3; ::_thesis: verum end; theorem :: FINSEQ_4:39 for p being FinSequence for x being set st x in rng p holds rng (p -| x) c= rng p proof let p be FinSequence; ::_thesis: for x being set st x in rng p holds rng (p -| x) c= rng p let x be set ; ::_thesis: ( x in rng p implies rng (p -| x) c= rng p ) assume x in rng p ; ::_thesis: rng (p -| x) c= rng p then ex n being Nat st ( n = (x .. p) - 1 & p | (Seg n) = p -| x ) by Def5; hence rng (p -| x) c= rng p by RELAT_1:70; ::_thesis: verum end; theorem :: FINSEQ_4:40 for p being FinSequence for x being set st x in rng p holds ( x .. p = 1 iff p -| x = {} ) proof let p be FinSequence; ::_thesis: for x being set st x in rng p holds ( x .. p = 1 iff p -| x = {} ) let x be set ; ::_thesis: ( x in rng p implies ( x .. p = 1 iff p -| x = {} ) ) assume A1: x in rng p ; ::_thesis: ( x .. p = 1 iff p -| x = {} ) thus ( x .. p = 1 implies p -| x = {} ) ::_thesis: ( p -| x = {} implies x .. p = 1 ) proof assume A2: x .. p = 1 ; ::_thesis: p -| x = {} len (p -| x) = (x .. p) - 1 by A1, Th34 .= 0 by A2 ; hence p -| x = {} ; ::_thesis: verum end; assume p -| x = {} ; ::_thesis: x .. p = 1 then A3: len (p -| x) = 0 ; len (p -| x) = (x .. p) - 1 by A1, Th34; hence x .. p = 1 by A3; ::_thesis: verum end; theorem :: FINSEQ_4:41 for p being FinSequence for x being set for D being non empty set st x in rng p & p is FinSequence of D holds p -| x is FinSequence of D proof let p be FinSequence; ::_thesis: for x being set for D being non empty set st x in rng p & p is FinSequence of D holds p -| x is FinSequence of D let x be set ; ::_thesis: for D being non empty set st x in rng p & p is FinSequence of D holds p -| x is FinSequence of D let D be non empty set ; ::_thesis: ( x in rng p & p is FinSequence of D implies p -| x is FinSequence of D ) assume x in rng p ; ::_thesis: ( not p is FinSequence of D or p -| x is FinSequence of D ) then ex n being Nat st ( n = (x .. p) - 1 & p | (Seg n) = p -| x ) by Def5; hence ( not p is FinSequence of D or p -| x is FinSequence of D ) by FINSEQ_1:18; ::_thesis: verum end; definition let p be FinSequence; let x be set ; assume A1: x in rng p ; funcp |-- x -> FinSequence means :Def6: :: FINSEQ_4:def 6 ( len it = (len p) - (x .. p) & ( for k being Nat st k in dom it holds it . k = p . (k + (x .. p)) ) ); existence ex b1 being FinSequence st ( len b1 = (len p) - (x .. p) & ( for k being Nat st k in dom b1 holds b1 . k = p . (k + (x .. p)) ) ) proof deffunc H1( Nat) -> set = p . ($1 + (x .. p)); reconsider n = (len p) - (x .. p) as Element of NAT by A1, Th22; consider q being FinSequence such that A2: ( len q = n & ( for k being Nat st k in dom q holds q . k = H1(k) ) ) from FINSEQ_1:sch_2(); take q ; ::_thesis: ( len q = (len p) - (x .. p) & ( for k being Nat st k in dom q holds q . k = p . (k + (x .. p)) ) ) thus ( len q = (len p) - (x .. p) & ( for k being Nat st k in dom q holds q . k = p . (k + (x .. p)) ) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence st len b1 = (len p) - (x .. p) & ( for k being Nat st k in dom b1 holds b1 . k = p . (k + (x .. p)) ) & len b2 = (len p) - (x .. p) & ( for k being Nat st k in dom b2 holds b2 . k = p . (k + (x .. p)) ) holds b1 = b2 proof let q, r be FinSequence; ::_thesis: ( len q = (len p) - (x .. p) & ( for k being Nat st k in dom q holds q . k = p . (k + (x .. p)) ) & len r = (len p) - (x .. p) & ( for k being Nat st k in dom r holds r . k = p . (k + (x .. p)) ) implies q = r ) assume that A3: len q = (len p) - (x .. p) and A4: for k being Nat st k in dom q holds q . k = p . (k + (x .. p)) ; ::_thesis: ( not len r = (len p) - (x .. p) or ex k being Nat st ( k in dom r & not r . k = p . (k + (x .. p)) ) or q = r ) assume that A5: len r = (len p) - (x .. p) and A6: for k being Nat st k in dom r holds r . k = p . (k + (x .. p)) ; ::_thesis: q = r now__::_thesis:_for_k_being_Nat_st_k_in_dom_q_holds_ q_._k_=_r_._k let k be Nat; ::_thesis: ( k in dom q implies q . k = r . k ) A7: ( dom q = Seg (len q) & dom r = Seg (len r) ) by FINSEQ_1:def_3; assume A8: k in dom q ; ::_thesis: q . k = r . k then q . k = p . (k + (x .. p)) by A4; hence q . k = r . k by A3, A5, A6, A8, A7; ::_thesis: verum end; hence q = r by A3, A5, FINSEQ_2:9; ::_thesis: verum end; end; :: deftheorem Def6 defines |-- FINSEQ_4:def_6_:_ for p being FinSequence for x being set st x in rng p holds for b3 being FinSequence holds ( b3 = p |-- x iff ( len b3 = (len p) - (x .. p) & ( for k being Nat st k in dom b3 holds b3 . k = p . (k + (x .. p)) ) ) ); theorem Th42: :: FINSEQ_4:42 for p being FinSequence for x being set for n being Nat st x in rng p & n = (len p) - (x .. p) holds dom (p |-- x) = Seg n proof let p be FinSequence; ::_thesis: for x being set for n being Nat st x in rng p & n = (len p) - (x .. p) holds dom (p |-- x) = Seg n let x be set ; ::_thesis: for n being Nat st x in rng p & n = (len p) - (x .. p) holds dom (p |-- x) = Seg n let n be Nat; ::_thesis: ( x in rng p & n = (len p) - (x .. p) implies dom (p |-- x) = Seg n ) assume x in rng p ; ::_thesis: ( not n = (len p) - (x .. p) or dom (p |-- x) = Seg n ) then len (p |-- x) = (len p) - (x .. p) by Def6; hence ( not n = (len p) - (x .. p) or dom (p |-- x) = Seg n ) by FINSEQ_1:def_3; ::_thesis: verum end; theorem Th43: :: FINSEQ_4:43 for p being FinSequence for x being set for n being Nat st x in rng p & n in dom (p |-- x) holds n + (x .. p) in dom p proof let p be FinSequence; ::_thesis: for x being set for n being Nat st x in rng p & n in dom (p |-- x) holds n + (x .. p) in dom p let x be set ; ::_thesis: for n being Nat st x in rng p & n in dom (p |-- x) holds n + (x .. p) in dom p let n be Nat; ::_thesis: ( x in rng p & n in dom (p |-- x) implies n + (x .. p) in dom p ) assume that A1: x in rng p and A2: n in dom (p |-- x) ; ::_thesis: n + (x .. p) in dom p reconsider m = (len p) - (x .. p) as Element of NAT by A1, Th22; n in Seg m by A1, A2, Th42; then n <= (len p) - (x .. p) by FINSEQ_1:1; then A3: n + (x .. p) <= len p by XREAL_1:19; 1 <= n by A2, FINSEQ_3:25; then 1 <= n + (x .. p) by NAT_1:12; hence n + (x .. p) in dom p by A3, FINSEQ_3:25; ::_thesis: verum end; theorem :: FINSEQ_4:44 for p being FinSequence for x being set st x in rng p holds rng (p |-- x) c= rng p proof let p be FinSequence; ::_thesis: for x being set st x in rng p holds rng (p |-- x) c= rng p let x be set ; ::_thesis: ( x in rng p implies rng (p |-- x) c= rng p ) assume A1: x in rng p ; ::_thesis: rng (p |-- x) c= rng p let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (p |-- x) or y in rng p ) assume y in rng (p |-- x) ; ::_thesis: y in rng p then consider z being set such that A2: z in dom (p |-- x) and A3: (p |-- x) . z = y by FUNCT_1:def_3; reconsider z = z as Element of NAT by A2; ( y = p . (z + (x .. p)) & z + (x .. p) in dom p ) by A1, A2, A3, Def6, Th43; hence y in rng p by FUNCT_1:def_3; ::_thesis: verum end; theorem Th45: :: FINSEQ_4:45 for p being FinSequence for x being set holds ( p just_once_values x iff ( x in rng p & not x in rng (p |-- x) ) ) proof let p be FinSequence; ::_thesis: for x being set holds ( p just_once_values x iff ( x in rng p & not x in rng (p |-- x) ) ) let x be set ; ::_thesis: ( p just_once_values x iff ( x in rng p & not x in rng (p |-- x) ) ) thus ( p just_once_values x implies ( x in rng p & not x in rng (p |-- x) ) ) ::_thesis: ( x in rng p & not x in rng (p |-- x) implies p just_once_values x ) proof assume A1: p just_once_values x ; ::_thesis: ( x in rng p & not x in rng (p |-- x) ) hence A2: x in rng p by Th5; ::_thesis: not x in rng (p |-- x) assume x in rng (p |-- x) ; ::_thesis: contradiction then consider z being set such that A3: z in dom (p |-- x) and A4: (p |-- x) . z = x by FUNCT_1:def_3; reconsider z = z as Element of NAT by A3; ( (p |-- x) . z = p . (z + (x .. p)) & z + (x .. p) in dom p ) by A2, A3, Def6, Th43; then z + (x .. p) = 0 + (x .. p) by A1, A4, Th26; hence contradiction by A3, FINSEQ_3:24; ::_thesis: verum end; assume that A5: x in rng p and A6: not x in rng (p |-- x) ; ::_thesis: p just_once_values x now__::_thesis:_for_k_being_Nat_st_k_in_dom_p_&_k_<>_x_.._p_holds_ not_p_._k_=_x let k be Nat; ::_thesis: ( k in dom p & k <> x .. p implies not p . k = x ) assume that A7: k in dom p and A8: k <> x .. p and A9: p . k = x ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( k < x .. p or x .. p < k ) by A8, XXREAL_0:1; suppose k < x .. p ; ::_thesis: contradiction then k + 1 <= x .. p by NAT_1:13; then k <= (x .. p) - 1 by XREAL_1:19; then A10: k <= len (p -| x) by A5, Th34; 1 <= k by A7, FINSEQ_3:25; then A11: k in dom (p -| x) by A10, FINSEQ_3:25; then x = (p -| x) . k by A5, A9, Th36; then x in rng (p -| x) by A11, FUNCT_1:def_3; hence contradiction by A5, Th37; ::_thesis: verum end; supposeA12: x .. p < k ; ::_thesis: contradiction then consider m being Nat such that A13: k = (x .. p) + m by NAT_1:10; (x .. p) + 0 < (x .. p) + m by A12, A13; then 0 < m ; then A14: 0 + 1 <= m by NAT_1:13; m + (x .. p) <= len p by A7, A13, FINSEQ_3:25; then m <= (len p) - (x .. p) by XREAL_1:19; then m <= len (p |-- x) by A5, Def6; then A15: m in dom (p |-- x) by A14, FINSEQ_3:25; then (p |-- x) . m = p . k by A5, A13, Def6; hence contradiction by A6, A9, A15, FUNCT_1:def_3; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; hence p just_once_values x by A5, Th27; ::_thesis: verum end; theorem Th46: :: FINSEQ_4:46 for p being FinSequence for x being set st x in rng p & p is one-to-one holds not x in rng (p |-- x) proof let p be FinSequence; ::_thesis: for x being set st x in rng p & p is one-to-one holds not x in rng (p |-- x) let x be set ; ::_thesis: ( x in rng p & p is one-to-one implies not x in rng (p |-- x) ) assume that A1: x in rng p and A2: p is one-to-one and A3: x in rng (p |-- x) ; ::_thesis: contradiction A4: len (p |-- x) = (len p) - (x .. p) by A1, Def6; consider y being set such that A5: y in dom (p |-- x) and A6: (p |-- x) . y = x by A3, FUNCT_1:def_3; reconsider y = y as Element of NAT by A5; A7: 1 <= y + (x .. p) by A1, Th21, NAT_1:12; A8: y in Seg (len (p |-- x)) by A5, FINSEQ_1:def_3; then y <= len (p |-- x) by FINSEQ_1:1; then y + (x .. p) <= len p by A4, XREAL_1:19; then y + (x .. p) in Seg (len p) by A7; then A9: y + (x .. p) in dom p by FINSEQ_1:def_3; A10: ( x .. p in dom p & p . (x .. p) = x ) by A1, Th19, Th20; (p |-- x) . y = p . (y + (x .. p)) by A1, A5, Def6; then 0 + (x .. p) = y + (x .. p) by A2, A6, A10, A9, FUNCT_1:def_4; hence contradiction by A8, FINSEQ_1:1; ::_thesis: verum end; theorem :: FINSEQ_4:47 for p being FinSequence for x being set holds ( p just_once_values x iff ( x in rng p & rng (p |-- x) misses {x} ) ) proof let p be FinSequence; ::_thesis: for x being set holds ( p just_once_values x iff ( x in rng p & rng (p |-- x) misses {x} ) ) let x be set ; ::_thesis: ( p just_once_values x iff ( x in rng p & rng (p |-- x) misses {x} ) ) thus ( p just_once_values x implies ( x in rng p & rng (p |-- x) misses {x} ) ) ::_thesis: ( x in rng p & rng (p |-- x) misses {x} implies p just_once_values x ) proof assume A1: p just_once_values x ; ::_thesis: ( x in rng p & rng (p |-- x) misses {x} ) hence x in rng p by Th45; ::_thesis: rng (p |-- x) misses {x} assume not rng (p |-- x) misses {x} ; ::_thesis: contradiction then A2: ex y being set st ( y in rng (p |-- x) & y in {x} ) by XBOOLE_0:3; not x in rng (p |-- x) by A1, Th45; hence contradiction by A2, TARSKI:def_1; ::_thesis: verum end; assume that A3: x in rng p and A4: rng (p |-- x) misses {x} ; ::_thesis: p just_once_values x now__::_thesis:_not_x_in_rng_(p_|--_x) A5: x in {x} by TARSKI:def_1; assume x in rng (p |-- x) ; ::_thesis: contradiction hence contradiction by A4, A5, XBOOLE_0:3; ::_thesis: verum end; hence p just_once_values x by A3, Th45; ::_thesis: verum end; theorem :: FINSEQ_4:48 for p being FinSequence for x being set st x in rng p & p is one-to-one holds rng (p |-- x) misses {x} proof let p be FinSequence; ::_thesis: for x being set st x in rng p & p is one-to-one holds rng (p |-- x) misses {x} let x be set ; ::_thesis: ( x in rng p & p is one-to-one implies rng (p |-- x) misses {x} ) assume ( x in rng p & p is one-to-one ) ; ::_thesis: rng (p |-- x) misses {x} then not x in rng (p |-- x) by Th46; then for y being set st y in rng (p |-- x) holds not y in {x} by TARSKI:def_1; hence rng (p |-- x) misses {x} by XBOOLE_0:3; ::_thesis: verum end; theorem :: FINSEQ_4:49 for p being FinSequence for x being set st x in rng p holds ( x .. p = len p iff p |-- x = {} ) proof let p be FinSequence; ::_thesis: for x being set st x in rng p holds ( x .. p = len p iff p |-- x = {} ) let x be set ; ::_thesis: ( x in rng p implies ( x .. p = len p iff p |-- x = {} ) ) assume A1: x in rng p ; ::_thesis: ( x .. p = len p iff p |-- x = {} ) thus ( x .. p = len p implies p |-- x = {} ) ::_thesis: ( p |-- x = {} implies x .. p = len p ) proof assume A2: x .. p = len p ; ::_thesis: p |-- x = {} len (p |-- x) = (len p) - (x .. p) by A1, Def6 .= 0 by A2 ; hence p |-- x = {} ; ::_thesis: verum end; assume p |-- x = {} ; ::_thesis: x .. p = len p then A3: len (p |-- x) = 0 ; len (p |-- x) = (len p) - (x .. p) by A1, Def6; hence x .. p = len p by A3; ::_thesis: verum end; theorem :: FINSEQ_4:50 for p being FinSequence for x being set for D being non empty set st x in rng p & p is FinSequence of D holds p |-- x is FinSequence of D proof let p be FinSequence; ::_thesis: for x being set for D being non empty set st x in rng p & p is FinSequence of D holds p |-- x is FinSequence of D let x be set ; ::_thesis: for D being non empty set st x in rng p & p is FinSequence of D holds p |-- x is FinSequence of D let D be non empty set ; ::_thesis: ( x in rng p & p is FinSequence of D implies p |-- x is FinSequence of D ) assume that A1: x in rng p and A2: p is FinSequence of D ; ::_thesis: p |-- x is FinSequence of D rng (p |-- x) c= D proof A3: len (p |-- x) = (len p) - (x .. p) by A1, Def6; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (p |-- x) or y in D ) assume y in rng (p |-- x) ; ::_thesis: y in D then consider z being set such that A4: z in dom (p |-- x) and A5: (p |-- x) . z = y by FUNCT_1:def_3; reconsider z = z as Element of NAT by A4; dom (p |-- x) = Seg (len (p |-- x)) by FINSEQ_1:def_3; then z <= len (p |-- x) by A4, FINSEQ_1:1; then A6: z + (x .. p) <= len p by A3, XREAL_1:19; 1 <= z + (x .. p) by A1, Th21, NAT_1:12; then z + (x .. p) in Seg (len p) by A6; then A7: z + (x .. p) in dom p by FINSEQ_1:def_3; y = p . (z + (x .. p)) by A1, A4, A5, Def6; then A8: y in rng p by A7, FUNCT_1:def_3; rng p c= D by A2, FINSEQ_1:def_4; hence y in D by A8; ::_thesis: verum end; hence p |-- x is FinSequence of D by FINSEQ_1:def_4; ::_thesis: verum end; theorem Th51: :: FINSEQ_4:51 for p being FinSequence for x being set st x in rng p holds p = ((p -| x) ^ <*x*>) ^ (p |-- x) proof let p be FinSequence; ::_thesis: for x being set st x in rng p holds p = ((p -| x) ^ <*x*>) ^ (p |-- x) let x be set ; ::_thesis: ( x in rng p implies p = ((p -| x) ^ <*x*>) ^ (p |-- x) ) set q1 = p -| x; set q2 = p |-- x; set r = (p -| x) ^ <*x*>; assume A1: x in rng p ; ::_thesis: p = ((p -| x) ^ <*x*>) ^ (p |-- x) A2: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_(p_|--_x)_holds_ p_._((len_((p_-|_x)_^_<*x*>))_+_k)_=_(p_|--_x)_._k let k be Element of NAT ; ::_thesis: ( k in dom (p |-- x) implies p . ((len ((p -| x) ^ <*x*>)) + k) = (p |-- x) . k ) assume k in dom (p |-- x) ; ::_thesis: p . ((len ((p -| x) ^ <*x*>)) + k) = (p |-- x) . k then (p |-- x) . k = p . ((((x .. p) - 1) + 1) + k) by A1, Def6 .= p . (((len (p -| x)) + 1) + k) by A1, Th34 .= p . (((len (p -| x)) + (len <*x*>)) + k) by FINSEQ_1:40 .= p . ((len ((p -| x) ^ <*x*>)) + k) by FINSEQ_1:22 ; hence p . ((len ((p -| x) ^ <*x*>)) + k) = (p |-- x) . k ; ::_thesis: verum end; A3: now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_((p_-|_x)_^_<*x*>)_holds_ p_._k_=_((p_-|_x)_^_<*x*>)_._k let k be Element of NAT ; ::_thesis: ( k in dom ((p -| x) ^ <*x*>) implies p . k = ((p -| x) ^ <*x*>) . k ) assume A4: k in dom ((p -| x) ^ <*x*>) ; ::_thesis: p . k = ((p -| x) ^ <*x*>) . k now__::_thesis:_((p_-|_x)_^_<*x*>)_._k_=_p_._k percases ( k in dom (p -| x) or ex n being Nat st ( n in dom <*x*> & k = (len (p -| x)) + n ) ) by A4, FINSEQ_1:25; supposeA5: k in dom (p -| x) ; ::_thesis: ((p -| x) ^ <*x*>) . k = p . k hence ((p -| x) ^ <*x*>) . k = (p -| x) . k by FINSEQ_1:def_7 .= p . k by A1, A5, Th36 ; ::_thesis: verum end; suppose ex n being Nat st ( n in dom <*x*> & k = (len (p -| x)) + n ) ; ::_thesis: ((p -| x) ^ <*x*>) . k = p . k then consider n being Nat such that A6: n in dom <*x*> and A7: k = (len (p -| x)) + n ; n in {1} by A6, FINSEQ_1:2, FINSEQ_1:def_8; then A8: n = 1 by TARSKI:def_1; hence ((p -| x) ^ <*x*>) . k = <*x*> . 1 by A6, A7, FINSEQ_1:def_7 .= x by FINSEQ_1:def_8 .= p . (((x .. p) - 1) + 1) by A1, Th19 .= p . k by A1, A7, A8, Th34 ; ::_thesis: verum end; end; end; hence p . k = ((p -| x) ^ <*x*>) . k ; ::_thesis: verum end; len p = ((len p) - (x .. p)) + (x .. p) .= (((x .. p) - 1) + 1) + (len (p |-- x)) by A1, Def6 .= ((len (p -| x)) + 1) + (len (p |-- x)) by A1, Th34 .= ((len (p -| x)) + (len <*x*>)) + (len (p |-- x)) by FINSEQ_1:40 .= (len ((p -| x) ^ <*x*>)) + (len (p |-- x)) by FINSEQ_1:22 ; hence p = ((p -| x) ^ <*x*>) ^ (p |-- x) by A3, A2, FINSEQ_3:38; ::_thesis: verum end; theorem :: FINSEQ_4:52 for p being FinSequence for x being set st x in rng p & p is one-to-one holds p -| x is one-to-one proof let p be FinSequence; ::_thesis: for x being set st x in rng p & p is one-to-one holds p -| x is one-to-one let x be set ; ::_thesis: ( x in rng p & p is one-to-one implies p -| x is one-to-one ) assume x in rng p ; ::_thesis: ( not p is one-to-one or p -| x is one-to-one ) then p = ((p -| x) ^ <*x*>) ^ (p |-- x) by Th51 .= (p -| x) ^ (<*x*> ^ (p |-- x)) by FINSEQ_1:32 ; hence ( not p is one-to-one or p -| x is one-to-one ) by FINSEQ_3:91; ::_thesis: verum end; theorem :: FINSEQ_4:53 for p being FinSequence for x being set st x in rng p & p is one-to-one holds p |-- x is one-to-one proof let p be FinSequence; ::_thesis: for x being set st x in rng p & p is one-to-one holds p |-- x is one-to-one let x be set ; ::_thesis: ( x in rng p & p is one-to-one implies p |-- x is one-to-one ) assume x in rng p ; ::_thesis: ( not p is one-to-one or p |-- x is one-to-one ) then p = ((p -| x) ^ <*x*>) ^ (p |-- x) by Th51; hence ( not p is one-to-one or p |-- x is one-to-one ) by FINSEQ_3:91; ::_thesis: verum end; theorem Th54: :: FINSEQ_4:54 for p being FinSequence for x being set holds ( p just_once_values x iff ( x in rng p & p - {x} = (p -| x) ^ (p |-- x) ) ) proof let p be FinSequence; ::_thesis: for x being set holds ( p just_once_values x iff ( x in rng p & p - {x} = (p -| x) ^ (p |-- x) ) ) let x be set ; ::_thesis: ( p just_once_values x iff ( x in rng p & p - {x} = (p -| x) ^ (p |-- x) ) ) set q = p - {x}; set r = p -| x; set s = p |-- x; thus ( p just_once_values x implies ( x in rng p & p - {x} = (p -| x) ^ (p |-- x) ) ) ::_thesis: ( x in rng p & p - {x} = (p -| x) ^ (p |-- x) implies p just_once_values x ) proof assume A1: p just_once_values x ; ::_thesis: ( x in rng p & p - {x} = (p -| x) ^ (p |-- x) ) hence A2: x in rng p by Th5; ::_thesis: p - {x} = (p -| x) ^ (p |-- x) A3: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(p_-|_x)_holds_ (p_-_{x})_._k_=_(p_-|_x)_._k x .. p <= len p by A2, Th21; then (x .. p) - 1 <= (len p) - 1 by XREAL_1:9; then len (p -| x) <= (len p) - 1 by A2, Th34; then len (p -| x) <= len (p - {x}) by A1, Th30; then A4: Seg (len (p -| x)) c= Seg (len (p - {x})) by FINSEQ_1:5; let k be Nat; ::_thesis: ( k in dom (p -| x) implies (p - {x}) . k = (p -| x) . k ) A5: ( Seg (len (p -| x)) = dom (p -| x) & Seg (len (p - {x})) = dom (p - {x}) ) by FINSEQ_1:def_3; assume A6: k in dom (p -| x) ; ::_thesis: (p - {x}) . k = (p -| x) . k then k in Seg (len (p -| x)) by FINSEQ_1:def_3; then k <= len (p -| x) by FINSEQ_1:1; then k <= (x .. p) - 1 by A2, Th34; then A7: k + 1 <= x .. p by XREAL_1:19; k < k + 1 by XREAL_1:29; then A8: k < x .. p by A7, XXREAL_0:2; (p -| x) . k = p . k by A2, A6, Th36; hence (p - {x}) . k = (p -| x) . k by A1, A6, A4, A5, A8, Th31; ::_thesis: verum end; A9: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(p_|--_x)_holds_ (p_-_{x})_._((len_(p_-|_x))_+_k)_=_(p_|--_x)_._k reconsider m = (x .. p) - 1 as Element of NAT by A2, Th22; let k be Nat; ::_thesis: ( k in dom (p |-- x) implies (p - {x}) . ((len (p -| x)) + k) = (p |-- x) . k ) set z = k + m; assume A10: k in dom (p |-- x) ; ::_thesis: (p - {x}) . ((len (p -| x)) + k) = (p |-- x) . k then A11: (p |-- x) . k = p . (k + (x .. p)) by A2, Def6; A12: dom (p |-- x) = Seg (len (p |-- x)) by FINSEQ_1:def_3; then A13: 1 <= k by A10, FINSEQ_1:1; then (x .. p) + 1 <= k + (x .. p) by XREAL_1:7; then A14: x .. p <= (k + (x .. p)) - 1 by XREAL_1:19; k <= len (p |-- x) by A10, A12, FINSEQ_1:1; then k <= (len p) - (x .. p) by A2, Def6; then k + (x .. p) <= len p by XREAL_1:19; then (k + (x .. p)) - 1 <= (len p) - 1 by XREAL_1:9; then A15: (k + (x .. p)) - 1 <= len (p - {x}) by A1, Th30; 1 <= x .. p by A2, Th21; then 1 + 1 <= k + (x .. p) by A13, XREAL_1:7; then A16: 1 <= (k + (x .. p)) - 1 by XREAL_1:19; dom (p - {x}) = Seg (len (p - {x})) by FINSEQ_1:def_3; then k + m in dom (p - {x}) by A16, A15; then (p - {x}) . (k + m) = p . ((k + m) + 1) by A1, A14, Th31 .= p . (k + (x .. p)) ; hence (p - {x}) . ((len (p -| x)) + k) = (p |-- x) . k by A2, A11, Th34; ::_thesis: verum end; (len (p -| x)) + (len (p |-- x)) = ((x .. p) - 1) + (len (p |-- x)) by A2, Th34 .= ((x .. p) - 1) + ((len p) - (x .. p)) by A2, Def6 .= (len p) - 1 .= len (p - {x}) by A1, Th30 ; then dom (p - {x}) = Seg ((len (p -| x)) + (len (p |-- x))) by FINSEQ_1:def_3; hence p - {x} = (p -| x) ^ (p |-- x) by A3, A9, FINSEQ_1:def_7; ::_thesis: verum end; assume A17: x in rng p ; ::_thesis: ( not p - {x} = (p -| x) ^ (p |-- x) or p just_once_values x ) assume A18: p - {x} = (p -| x) ^ (p |-- x) ; ::_thesis: p just_once_values x now__::_thesis:_for_k_being_Nat_st_k_in_dom_p_&_k_<>_x_.._p_holds_ not_p_._k_=_x let k be Nat; ::_thesis: ( k in dom p & k <> x .. p implies not p . k = x ) assume that A19: k in dom p and A20: k <> x .. p and A21: p . k = x ; ::_thesis: contradiction {(x .. p),k} c= p " {x} proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {(x .. p),k} or y in p " {x} ) assume A22: y in {(x .. p),k} ; ::_thesis: y in p " {x} A23: x in {x} by TARSKI:def_1; ( x .. p in dom p & p . (x .. p) = x ) by A17, Th19, Th20; then A24: x .. p in p " {x} by A23, FUNCT_1:def_7; k in p " {x} by A19, A21, A23, FUNCT_1:def_7; hence y in p " {x} by A22, A24, TARSKI:def_2; ::_thesis: verum end; then card {(x .. p),k} <= card (p " {x}) by NAT_1:43; then A25: 2 <= card (p " {x}) by A20, CARD_2:57; A26: len (p - {x}) = (len p) - (card (p " {x})) by FINSEQ_3:59 .= (len p) + (- (card (p " {x}))) ; len (p - {x}) = (len (p -| x)) + (len (p |-- x)) by A18, FINSEQ_1:22 .= ((x .. p) - 1) + (len (p |-- x)) by A17, Th34 .= ((x .. p) - 1) + ((len p) - (x .. p)) by A17, Def6 .= (len p) + (- 1) ; hence contradiction by A26, A25; ::_thesis: verum end; hence p just_once_values x by A17, Th27; ::_thesis: verum end; theorem :: FINSEQ_4:55 for p being FinSequence for x being set st x in rng p & p is one-to-one holds p - {x} = (p -| x) ^ (p |-- x) proof let p be FinSequence; ::_thesis: for x being set st x in rng p & p is one-to-one holds p - {x} = (p -| x) ^ (p |-- x) let x be set ; ::_thesis: ( x in rng p & p is one-to-one implies p - {x} = (p -| x) ^ (p |-- x) ) assume ( x in rng p & p is one-to-one ) ; ::_thesis: p - {x} = (p -| x) ^ (p |-- x) then p just_once_values x by Th8; hence p - {x} = (p -| x) ^ (p |-- x) by Th54; ::_thesis: verum end; theorem Th56: :: FINSEQ_4:56 for p being FinSequence for x being set st x in rng p & p - {x} is one-to-one & p - {x} = (p -| x) ^ (p |-- x) holds p is one-to-one proof let p be FinSequence; ::_thesis: for x being set st x in rng p & p - {x} is one-to-one & p - {x} = (p -| x) ^ (p |-- x) holds p is one-to-one let x be set ; ::_thesis: ( x in rng p & p - {x} is one-to-one & p - {x} = (p -| x) ^ (p |-- x) implies p is one-to-one ) assume that A1: x in rng p and A2: p - {x} is one-to-one and A3: p - {x} = (p -| x) ^ (p |-- x) ; ::_thesis: p is one-to-one set q = p - {x}; let x1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x1 in dom p or not b1 in dom p or not p . x1 = p . b1 or x1 = b1 ) let x2 be set ; ::_thesis: ( not x1 in dom p or not x2 in dom p or not p . x1 = p . x2 or x1 = x2 ) assume that A4: x1 in dom p and A5: x2 in dom p and A6: p . x1 = p . x2 ; ::_thesis: x1 = x2 reconsider k1 = x1, k2 = x2 as Element of NAT by A4, A5; A7: p just_once_values x by A1, A3, Th54; now__::_thesis:_x1_=_x2 percases ( ( x1 = x .. p & x2 = x .. p ) or ( x1 = x .. p & x .. p < k2 ) or ( x1 = x .. p & k2 < x .. p ) or ( k1 < x .. p & x .. p = x2 ) or ( k1 < x .. p & x .. p < k2 ) or ( k1 < x .. p & k2 < x .. p ) or ( x .. p < k1 & x .. p < k2 ) or ( x .. p < k1 & x .. p = x2 ) or ( x .. p < k1 & k2 < x .. p ) ) by XXREAL_0:1; suppose ( x1 = x .. p & x2 = x .. p ) ; ::_thesis: x1 = x2 hence x1 = x2 ; ::_thesis: verum end; suppose ( x1 = x .. p & x .. p < k2 ) ; ::_thesis: x1 = x2 hence x1 = x2 by A1, A5, A6, A7, Th19, Th26; ::_thesis: verum end; suppose ( x1 = x .. p & k2 < x .. p ) ; ::_thesis: x1 = x2 hence x1 = x2 by A1, A5, A6, A7, Th19, Th26; ::_thesis: verum end; suppose ( k1 < x .. p & x .. p = x2 ) ; ::_thesis: x1 = x2 hence x1 = x2 by A1, A4, A6, A7, Th19, Th26; ::_thesis: verum end; supposeA8: ( k1 < x .. p & x .. p < k2 ) ; ::_thesis: x1 = x2 x .. p <= len p by A1, Th21; then k1 < len p by A8, XXREAL_0:2; then k1 + 1 <= len p by NAT_1:13; then k1 <= (len p) - 1 by XREAL_1:19; then A9: k1 <= len (p - {x}) by A7, Th30; k1 in Seg (len p) by A4, FINSEQ_1:def_3; then 1 <= k1 by FINSEQ_1:1; then k1 in Seg (len (p - {x})) by A9; then A10: k1 in dom (p - {x}) by FINSEQ_1:def_3; then A11: (p - {x}) . k1 = p . k1 by A7, A8, Th31; consider m2 being Nat such that A12: k2 = m2 + 1 by A8, NAT_1:6; reconsider m2 = m2 as Element of NAT by ORDINAL1:def_12; A13: x .. p <= m2 by A8, A12, NAT_1:13; k2 in Seg (len p) by A5, FINSEQ_1:def_3; then k2 <= len p by FINSEQ_1:1; then m2 <= (len p) - 1 by A12, XREAL_1:19; then A14: m2 <= len (p - {x}) by A7, Th30; 1 <= x .. p by A1, Th21; then 1 <= m2 by A13, XXREAL_0:2; then m2 in Seg (len (p - {x})) by A14; then A15: m2 in dom (p - {x}) by FINSEQ_1:def_3; then (p - {x}) . m2 = p . k2 by A7, A12, A13, Th31; hence x1 = x2 by A2, A6, A8, A10, A13, A15, A11, FUNCT_1:def_4; ::_thesis: verum end; supposeA16: ( k1 < x .. p & k2 < x .. p ) ; ::_thesis: x1 = x2 A17: x .. p <= len p by A1, Th21; then k2 < len p by A16, XXREAL_0:2; then k2 + 1 <= len p by NAT_1:13; then k2 <= (len p) - 1 by XREAL_1:19; then A18: k2 <= len (p - {x}) by A7, Th30; k2 in Seg (len p) by A5, FINSEQ_1:def_3; then 1 <= k2 by FINSEQ_1:1; then k2 in Seg (len (p - {x})) by A18; then A19: k2 in dom (p - {x}) by FINSEQ_1:def_3; then A20: p . k2 = (p - {x}) . k2 by A7, A16, Th31; k1 < len p by A16, A17, XXREAL_0:2; then k1 + 1 <= len p by NAT_1:13; then k1 <= (len p) - 1 by XREAL_1:19; then A21: k1 <= len (p - {x}) by A7, Th30; k1 in Seg (len p) by A4, FINSEQ_1:def_3; then 1 <= k1 by FINSEQ_1:1; then k1 in Seg (len (p - {x})) by A21; then A22: k1 in dom (p - {x}) by FINSEQ_1:def_3; then p . k1 = (p - {x}) . k1 by A7, A16, Th31; hence x1 = x2 by A2, A6, A22, A19, A20, FUNCT_1:def_4; ::_thesis: verum end; supposeA23: ( x .. p < k1 & x .. p < k2 ) ; ::_thesis: x1 = x2 then consider m2 being Nat such that A24: k2 = m2 + 1 by NAT_1:6; consider m1 being Nat such that A25: k1 = m1 + 1 by A23, NAT_1:6; reconsider m1 = m1, m2 = m2 as Element of NAT by ORDINAL1:def_12; k2 in Seg (len p) by A5, FINSEQ_1:def_3; then k2 <= len p by FINSEQ_1:1; then m2 <= (len p) - 1 by A24, XREAL_1:19; then A26: m2 <= len (p - {x}) by A7, Th30; A27: 1 <= x .. p by A1, Th21; A28: x .. p <= m2 by A23, A24, NAT_1:13; then 1 <= m2 by A27, XXREAL_0:2; then m2 in Seg (len (p - {x})) by A26; then A29: m2 in dom (p - {x}) by FINSEQ_1:def_3; then A30: p . k2 = (p - {x}) . m2 by A7, A24, A28, Th31; k1 in Seg (len p) by A4, FINSEQ_1:def_3; then k1 <= len p by FINSEQ_1:1; then m1 <= (len p) - 1 by A25, XREAL_1:19; then A31: m1 <= len (p - {x}) by A7, Th30; A32: x .. p <= m1 by A23, A25, NAT_1:13; then 1 <= m1 by A27, XXREAL_0:2; then m1 in Seg (len (p - {x})) by A31; then A33: m1 in dom (p - {x}) by FINSEQ_1:def_3; then p . k1 = (p - {x}) . m1 by A7, A25, A32, Th31; hence x1 = x2 by A2, A6, A25, A24, A33, A29, A30, FUNCT_1:def_4; ::_thesis: verum end; suppose ( x .. p < k1 & x .. p = x2 ) ; ::_thesis: x1 = x2 hence x1 = x2 by A1, A4, A6, A7, Th19, Th26; ::_thesis: verum end; supposeA34: ( x .. p < k1 & k2 < x .. p ) ; ::_thesis: x1 = x2 x .. p <= len p by A1, Th21; then k2 < len p by A34, XXREAL_0:2; then k2 + 1 <= len p by NAT_1:13; then k2 <= (len p) - 1 by XREAL_1:19; then A35: k2 <= len (p - {x}) by A7, Th30; k2 in Seg (len p) by A5, FINSEQ_1:def_3; then 1 <= k2 by FINSEQ_1:1; then k2 in Seg (len (p - {x})) by A35; then A36: k2 in dom (p - {x}) by FINSEQ_1:def_3; then A37: (p - {x}) . k2 = p . k2 by A7, A34, Th31; consider m2 being Nat such that A38: k1 = m2 + 1 by A34, NAT_1:6; reconsider m2 = m2 as Element of NAT by ORDINAL1:def_12; A39: x .. p <= m2 by A34, A38, NAT_1:13; k1 in Seg (len p) by A4, FINSEQ_1:def_3; then k1 <= len p by FINSEQ_1:1; then m2 <= (len p) - 1 by A38, XREAL_1:19; then A40: m2 <= len (p - {x}) by A7, Th30; 1 <= x .. p by A1, Th21; then 1 <= m2 by A39, XXREAL_0:2; then m2 in Seg (len (p - {x})) by A40; then A41: m2 in dom (p - {x}) by FINSEQ_1:def_3; then (p - {x}) . m2 = p . k1 by A7, A38, A39, Th31; hence x1 = x2 by A2, A6, A34, A36, A39, A41, A37, FUNCT_1:def_4; ::_thesis: verum end; end; end; hence x1 = x2 ; ::_thesis: verum end; theorem :: FINSEQ_4:57 for p being FinSequence for x being set st x in rng p & p is one-to-one holds rng (p -| x) misses rng (p |-- x) proof let p be FinSequence; ::_thesis: for x being set st x in rng p & p is one-to-one holds rng (p -| x) misses rng (p |-- x) let x be set ; ::_thesis: ( x in rng p & p is one-to-one implies rng (p -| x) misses rng (p |-- x) ) assume that A1: x in rng p and A2: p is one-to-one ; ::_thesis: rng (p -| x) misses rng (p |-- x) p = ((p -| x) ^ <*x*>) ^ (p |-- x) by A1, Th51; then rng (p |-- x) misses rng ((p -| x) ^ <*x*>) by A2, FINSEQ_3:91; hence rng (p -| x) misses rng (p |-- x) by FINSEQ_1:29, XBOOLE_1:63; ::_thesis: verum end; theorem Th58: :: FINSEQ_4:58 for A being set st A is finite holds ex p being FinSequence st ( rng p = A & p is one-to-one ) proof let A be set ; ::_thesis: ( A is finite implies ex p being FinSequence st ( rng p = A & p is one-to-one ) ) defpred S1[ set ] means ex p being FinSequence st ( rng p = $1 & p is one-to-one ); rng {} = {} ; then A1: S1[ {} ] ; now__::_thesis:_for_B,_C_being_set_st_B_in_A_&_C_c=_A_&_ex_p_being_FinSequence_st_ (_rng_p_=_C_&_p_is_one-to-one_)_holds_ ex_p_being_FinSequence_st_ (_rng_p_=_C_\/_{B}_&_p_is_one-to-one_) let B, C be set ; ::_thesis: ( B in A & C c= A & ex p being FinSequence st ( rng p = C & p is one-to-one ) implies ex p being FinSequence st ( rng p = C \/ {B} & p is one-to-one ) ) assume that B in A and C c= A ; ::_thesis: ( ex p being FinSequence st ( rng p = C & p is one-to-one ) implies ex p being FinSequence st ( rng p = C \/ {B} & p is one-to-one ) ) given p being FinSequence such that A2: rng p = C and A3: p is one-to-one ; ::_thesis: ex p being FinSequence st ( rng p = C \/ {B} & p is one-to-one ) A4: now__::_thesis:_(_not_B_in_C_implies_ex_q_being_set_st_ (_rng_q_=_C_\/_{B}_&_q_is_one-to-one_)_) assume A5: not B in C ; ::_thesis: ex q being set st ( rng q = C \/ {B} & q is one-to-one ) take q = p ^ <*B*>; ::_thesis: ( rng q = C \/ {B} & q is one-to-one ) thus rng q = (rng p) \/ (rng <*B*>) by FINSEQ_1:31 .= C \/ {B} by A2, FINSEQ_1:38 ; ::_thesis: q is one-to-one thus q is one-to-one ::_thesis: verum proof let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom q or not b1 in dom q or not q . x = q . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom q or not y in dom q or not q . x = q . y or x = y ) assume that A6: ( x in dom q & y in dom q ) and A7: q . x = q . y ; ::_thesis: x = y reconsider k = x, l = y as Element of NAT by A6; A8: now__::_thesis:_(_k_in_dom_p_&_ex_n_being_Nat_st_ (_n_in_dom_<*B*>_&_l_=_(len_p)_+_n_)_implies_x_=_y_) assume A9: k in dom p ; ::_thesis: ( ex n being Nat st ( n in dom <*B*> & l = (len p) + n ) implies x = y ) given n being Nat such that A10: n in dom <*B*> and A11: l = (len p) + n ; ::_thesis: x = y n in {1} by A10, FINSEQ_1:2, FINSEQ_1:38; then A12: n = 1 by TARSKI:def_1; <*B*> . n = q . k by A7, A10, A11, FINSEQ_1:def_7 .= p . k by A9, FINSEQ_1:def_7 ; then B = p . k by A12, FINSEQ_1:def_8; hence x = y by A2, A5, A9, FUNCT_1:def_3; ::_thesis: verum end; A13: now__::_thesis:_(_l_in_dom_p_&_ex_n_being_Nat_st_ (_n_in_dom_<*B*>_&_k_=_(len_p)_+_n_)_implies_x_=_y_) assume A14: l in dom p ; ::_thesis: ( ex n being Nat st ( n in dom <*B*> & k = (len p) + n ) implies x = y ) given n being Nat such that A15: n in dom <*B*> and A16: k = (len p) + n ; ::_thesis: x = y n in {1} by A15, FINSEQ_1:2, FINSEQ_1:38; then A17: n = 1 by TARSKI:def_1; <*B*> . n = q . l by A7, A15, A16, FINSEQ_1:def_7 .= p . l by A14, FINSEQ_1:def_7 ; then B = p . l by A17, FINSEQ_1:def_8; hence x = y by A2, A5, A14, FUNCT_1:def_3; ::_thesis: verum end; A18: now__::_thesis:_(_ex_m1_being_Nat_st_ (_m1_in_dom_<*B*>_&_k_=_(len_p)_+_m1_)_&_ex_m2_being_Nat_st_ (_m2_in_dom_<*B*>_&_l_=_(len_p)_+_m2_)_implies_x_=_y_) given m1 being Nat such that A19: m1 in dom <*B*> and A20: k = (len p) + m1 ; ::_thesis: ( ex m2 being Nat st ( m2 in dom <*B*> & l = (len p) + m2 ) implies x = y ) m1 in {1} by A19, FINSEQ_1:2, FINSEQ_1:def_8; then A21: m1 = 1 by TARSKI:def_1; given m2 being Nat such that A22: m2 in dom <*B*> and A23: l = (len p) + m2 ; ::_thesis: x = y m2 in {1} by A22, FINSEQ_1:2, FINSEQ_1:def_8; hence x = y by A20, A23, A21, TARSKI:def_1; ::_thesis: verum end; now__::_thesis:_(_k_in_dom_p_&_l_in_dom_p_implies_x_=_y_) assume A24: ( k in dom p & l in dom p ) ; ::_thesis: x = y then ( q . k = p . k & q . l = p . l ) by FINSEQ_1:def_7; hence x = y by A3, A7, A24, FUNCT_1:def_4; ::_thesis: verum end; hence x = y by A6, A8, A13, A18, FINSEQ_1:25; ::_thesis: verum end; end; now__::_thesis:_(_B_in_C_implies_ex_q_being_FinSequence_st_ (_rng_q_=_C_\/_{B}_&_q_is_one-to-one_)_) assume A25: B in C ; ::_thesis: ex q being FinSequence st ( rng q = C \/ {B} & q is one-to-one ) take q = p; ::_thesis: ( rng q = C \/ {B} & q is one-to-one ) thus ( rng q = C \/ {B} & q is one-to-one ) by A2, A3, A25, ZFMISC_1:40; ::_thesis: verum end; hence ex p being FinSequence st ( rng p = C \/ {B} & p is one-to-one ) by A4; ::_thesis: verum end; then A26: for B, C being set st B in A & C c= A & S1[C] holds S1[C \/ {B}] ; assume A27: A is finite ; ::_thesis: ex p being FinSequence st ( rng p = A & p is one-to-one ) thus S1[A] from FINSET_1:sch_2(A27, A1, A26); ::_thesis: verum end; theorem Th59: :: FINSEQ_4:59 for p being FinSequence st rng p c= dom p & p is one-to-one holds rng p = dom p proof let p be FinSequence; ::_thesis: ( rng p c= dom p & p is one-to-one implies rng p = dom p ) defpred S1[ Nat] means for q being FinSequence st len q = $1 & rng q c= dom q & q is one-to-one holds rng q = dom q; A1: len p = len p ; now__::_thesis:_for_k_being_Nat_st_(_for_q_being_FinSequence_st_len_q_=_k_&_rng_q_c=_dom_q_&_q_is_one-to-one_holds_ rng_q_=_dom_q_)_holds_ for_q_being_FinSequence_st_len_q_=_k_+_1_&_rng_q_c=_dom_q_&_q_is_one-to-one_holds_ rng_q_=_dom_q let k be Nat; ::_thesis: ( ( for q being FinSequence st len q = k & rng q c= dom q & q is one-to-one holds rng q = dom q ) implies for q being FinSequence st len q = k + 1 & rng q c= dom q & q is one-to-one holds rng q = dom q ) assume A2: for q being FinSequence st len q = k & rng q c= dom q & q is one-to-one holds rng q = dom q ; ::_thesis: for q being FinSequence st len q = k + 1 & rng q c= dom q & q is one-to-one holds rng q = dom q let q be FinSequence; ::_thesis: ( len q = k + 1 & rng q c= dom q & q is one-to-one implies rng q = dom q ) assume that A3: len q = k + 1 and A4: rng q c= dom q and A5: q is one-to-one ; ::_thesis: rng q = dom q A6: dom q = Seg (k + 1) by A3, FINSEQ_1:def_3; dom q c= rng q proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom q or x in rng q ) assume A7: x in dom q ; ::_thesis: x in rng q then reconsider n = x as Element of NAT ; percases ( k + 1 in rng q or not k + 1 in rng q ) ; supposeA8: k + 1 in rng q ; ::_thesis: x in rng q now__::_thesis:_x_in_rng_q percases ( n = k + 1 or n <> k + 1 ) ; suppose n = k + 1 ; ::_thesis: x in rng q hence x in rng q by A8; ::_thesis: verum end; suppose n <> k + 1 ; ::_thesis: x in rng q then not x in {(k + 1)} by TARSKI:def_1; then x in (Seg (k + 1)) \ {(k + 1)} by A6, A7, XBOOLE_0:def_5; then A9: x in Seg k by FINSEQ_1:10; set r = q - {(k + 1)}; A10: len (q - {(k + 1)}) = (k + 1) - 1 by A3, A5, A8, FINSEQ_3:90; then A11: dom (q - {(k + 1)}) = Seg k by FINSEQ_1:def_3; A12: rng (q - {(k + 1)}) = (rng q) \ {(k + 1)} by FINSEQ_3:65; then rng (q - {(k + 1)}) c= (Seg (k + 1)) \ {(k + 1)} by A4, A6, XBOOLE_1:33; then rng (q - {(k + 1)}) c= dom (q - {(k + 1)}) by A11, FINSEQ_1:10; then rng (q - {(k + 1)}) = dom (q - {(k + 1)}) by A2, A5, A10, FINSEQ_3:87; hence x in rng q by A12, A11, A9; ::_thesis: verum end; end; end; hence x in rng q ; ::_thesis: verum end; supposeA13: not k + 1 in rng q ; ::_thesis: x in rng q A14: rng q c= Seg k proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng q or x in Seg k ) assume A15: x in rng q ; ::_thesis: x in Seg k then not x in {(k + 1)} by A13, TARSKI:def_1; then x in (Seg (k + 1)) \ {(k + 1)} by A4, A6, A15, XBOOLE_0:def_5; hence x in Seg k by FINSEQ_1:10; ::_thesis: verum end; A16: k + 1 in Seg (k + 1) by FINSEQ_1:4; then A17: q . (k + 1) in rng q by A6, FUNCT_1:def_3; reconsider r = q | (Seg k) as FinSequence by FINSEQ_1:15; A18: ( dom r c= dom q & k < k + 1 ) by RELAT_1:60, XREAL_1:29; A19: len r = k by A3, FINSEQ_3:53; then A20: dom r = Seg k by FINSEQ_1:def_3; ( rng r c= rng q & r is one-to-one ) by A5, FUNCT_1:52, RELAT_1:70; then rng r = dom r by A2, A19, A20, A14, XBOOLE_1:1; then consider x being set such that A21: x in dom r and A22: r . x = q . (k + 1) by A20, A14, A17, FUNCT_1:def_3; reconsider n = x as Element of NAT by A21; ( r . x = q . x & n <= k ) by A20, A21, FINSEQ_1:1, FUNCT_1:49; hence x in rng q by A5, A6, A16, A21, A22, A18, FUNCT_1:def_4; ::_thesis: verum end; end; end; hence rng q = dom q by A4, XBOOLE_0:def_10; ::_thesis: verum end; then A23: for k being Nat st S1[k] holds S1[k + 1] ; now__::_thesis:_for_q_being_FinSequence_st_len_q_=_0_&_rng_q_c=_dom_q_&_q_is_one-to-one_holds_ rng_q_=_dom_q let q be FinSequence; ::_thesis: ( len q = 0 & rng q c= dom q & q is one-to-one implies rng q = dom q ) assume A24: len q = 0 ; ::_thesis: ( rng q c= dom q & q is one-to-one implies rng q = dom q ) assume that rng q c= dom q and q is one-to-one ; ::_thesis: rng q = dom q q = {} by A24; hence rng q = dom q by RELAT_1:38; ::_thesis: verum end; then A25: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A25, A23); hence ( rng p c= dom p & p is one-to-one implies rng p = dom p ) by A1; ::_thesis: verum end; theorem Th60: :: FINSEQ_4:60 for p being FinSequence st rng p = dom p holds p is one-to-one proof let p be FinSequence; ::_thesis: ( rng p = dom p implies p is one-to-one ) defpred S1[ Nat] means for p being FinSequence st len p = $1 & rng p = dom p holds p is one-to-one ; A1: len p = len p ; A2: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_ S1[k_+_1] let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof set x = k + 1; let p be FinSequence; ::_thesis: ( len p = k + 1 & rng p = dom p implies p is one-to-one ) set q = p - {(k + 1)}; assume that A4: len p = k + 1 and A5: rng p = dom p ; ::_thesis: p is one-to-one A6: dom p = Seg (k + 1) by A4, FINSEQ_1:def_3; then A7: k + 1 in rng p by A5, FINSEQ_1:4; now__::_thesis:_for_l_being_Nat_st_l_in_dom_p_&_l_<>_(k_+_1)_.._p_holds_ not_p_._l_=_k_+_1 rng (p - {(k + 1)}) = (Seg (k + 1)) \ {(k + 1)} by A5, A6, FINSEQ_3:65 .= Seg k by FINSEQ_1:10 ; then card (rng (p - {(k + 1)})) = k by FINSEQ_1:57; then A8: card k = card (rng (p - {(k + 1)})) ; p . ((k + 1) .. p) = k + 1 by A5, A6, Th19, FINSEQ_1:4; then A9: p . ((k + 1) .. p) in {(k + 1)} by TARSKI:def_1; let l be Nat; ::_thesis: ( l in dom p & l <> (k + 1) .. p implies not p . l = k + 1 ) assume that A10: l in dom p and A11: l <> (k + 1) .. p and A12: p . l = k + 1 ; ::_thesis: contradiction A13: card {((k + 1) .. p),l} = 2 by A11, CARD_2:57; p . l in {(k + 1)} by A12, TARSKI:def_1; then A14: l in p " {(k + 1)} by A10, FUNCT_1:def_7; (k + 1) .. p in dom p by A5, A6, Th20, FINSEQ_1:4; then (k + 1) .. p in p " {(k + 1)} by A9, FUNCT_1:def_7; then {((k + 1) .. p),l} c= p " {(k + 1)} by A14, ZFMISC_1:32; then A15: 2 <= card (p " {(k + 1)}) by A13, NAT_1:43; len (p - {(k + 1)}) = (k + 1) - (card (p " {(k + 1)})) by A4, FINSEQ_3:59; then 2 + (len (p - {(k + 1)})) <= (card (p " {(k + 1)})) + ((k + 1) - (card (p " {(k + 1)}))) by A15, XREAL_1:6; then ((len (p - {(k + 1)})) + 1) + 1 <= k + 1 ; then (len (p - {(k + 1)})) + 1 <= k by XREAL_1:6; then A16: len (p - {(k + 1)}) <= k - 1 by XREAL_1:19; dom (p - {(k + 1)}) = Seg (len (p - {(k + 1)})) by FINSEQ_1:def_3; then ( card (rng (p - {(k + 1)})) c= card (dom (p - {(k + 1)})) & card (len (p - {(k + 1)})) = card (dom (p - {(k + 1)})) ) by CARD_1:12, FINSEQ_1:57; then k <= len (p - {(k + 1)}) by A8, NAT_1:40; then k <= k - 1 by A16, XXREAL_0:2; then k + 1 <= k + 0 by XREAL_1:19; hence contradiction by XREAL_1:6; ::_thesis: verum end; then A17: p just_once_values k + 1 by A7, Th27; then A18: len (p - {(k + 1)}) = (k + 1) - 1 by A4, Th30 .= k ; A19: p - {(k + 1)} = (p -| (k + 1)) ^ (p |-- (k + 1)) by A17, Th54; rng (p - {(k + 1)}) = (Seg (k + 1)) \ {(k + 1)} by A5, A6, FINSEQ_3:65 .= Seg k by FINSEQ_1:10 ; then dom (p - {(k + 1)}) = rng (p - {(k + 1)}) by A18, FINSEQ_1:def_3; hence p is one-to-one by A3, A7, A18, A19, Th56; ::_thesis: verum end; end; A20: S1[ 0 ] proof let p be FinSequence; ::_thesis: ( len p = 0 & rng p = dom p implies p is one-to-one ) assume len p = 0 ; ::_thesis: ( not rng p = dom p or p is one-to-one ) then p = {} ; hence ( not rng p = dom p or p is one-to-one ) ; ::_thesis: verum end; for k being Nat holds S1[k] from NAT_1:sch_2(A20, A2); hence ( rng p = dom p implies p is one-to-one ) by A1; ::_thesis: verum end; theorem :: FINSEQ_4:61 for p, q being FinSequence st rng p = rng q & len p = len q & q is one-to-one holds p is one-to-one proof let p, q be FinSequence; ::_thesis: ( rng p = rng q & len p = len q & q is one-to-one implies p is one-to-one ) assume that A1: rng p = rng q and A2: len p = len q and A3: q is one-to-one ; ::_thesis: p is one-to-one A4: rng p = dom (q ") by A1, A3, FUNCT_1:33; then A5: dom ((q ") * p) = dom p by RELAT_1:27 .= Seg (len p) by FINSEQ_1:def_3 ; then reconsider r = (q ") * p as FinSequence by FINSEQ_1:def_2; rng r = rng (q ") by A4, RELAT_1:28 .= dom q by A3, FUNCT_1:33 .= Seg (len q) by FINSEQ_1:def_3 ; then r is one-to-one by A2, A5, Th60; hence p is one-to-one by A4, FUNCT_1:26; ::_thesis: verum end; Lm1: for A, B being finite set for f being Function of A,B st card A = card B & rng f = B holds f is one-to-one proof let A, B be finite set ; ::_thesis: for f being Function of A,B st card A = card B & rng f = B holds f is one-to-one let f be Function of A,B; ::_thesis: ( card A = card B & rng f = B implies f is one-to-one ) assume that A1: card A = card B and A2: rng f = B ; ::_thesis: f is one-to-one A3: A,B are_equipotent by A1, CARD_1:5; consider p being FinSequence such that A4: rng p = A and A5: p is one-to-one by Th58; dom p,p .: (dom p) are_equipotent by A5, CARD_1:33; then dom p,A are_equipotent by A4, RELAT_1:113; then A6: dom p,B are_equipotent by A3, WELLORD2:15; reconsider X = dom p as finite set ; consider q being FinSequence such that A7: rng q = B and A8: q is one-to-one by Th58; A9: dom q = Seg (len q) by FINSEQ_1:def_3; dom q,q .: (dom q) are_equipotent by A8, CARD_1:33; then dom q,B are_equipotent by A7, RELAT_1:113; then dom p, dom q are_equipotent by A6, WELLORD2:15; then card X = card (Seg (len q)) by A9, CARD_1:5 .= len q by FINSEQ_1:57 ; then A10: len q = card (Seg (len p)) by FINSEQ_1:def_3 .= len p by FINSEQ_1:57 ; now__::_thesis:_f_is_one-to-one percases ( B = {} or B <> {} ) ; suppose B = {} ; ::_thesis: f is one-to-one hence f is one-to-one ; ::_thesis: verum end; supposeA11: B <> {} ; ::_thesis: f is one-to-one then rng p = dom f by A4, FUNCT_2:def_1; then A12: rng (f * p) = B by A2, RELAT_1:28 .= dom (q ") by A7, A8, FUNCT_1:33 ; dom (q ") = rng q by A8, FUNCT_1:33; then rng f c= dom (q ") by A7, RELAT_1:def_19; then dom ((q ") * f) = dom f by RELAT_1:27; then rng p = dom ((q ") * f) by A4, A11, FUNCT_2:def_1; then A13: dom (((q ") * f) * p) = dom p by RELAT_1:27 .= Seg (len p) by FINSEQ_1:def_3 ; then reconsider g = ((q ") * f) * p as FinSequence by FINSEQ_1:def_2; g = (q ") * (f * p) by RELAT_1:36; then rng g = rng (q ") by A12, RELAT_1:28 .= dom q by A8, FUNCT_1:33 .= Seg (len q) by FINSEQ_1:def_3 ; then A14: g is one-to-one by A10, A13, Th60; q * g = q * ((q ") * (f * p)) by RELAT_1:36 .= (q * (q ")) * (f * p) by RELAT_1:36 .= (id (rng q)) * (f * p) by A8, FUNCT_1:39 .= ((id (rng q)) * f) * p by RELAT_1:36 .= f * p by A2, A7, RELAT_1:54 ; then (q * g) * (p ") = f * (p * (p ")) by RELAT_1:36 .= f * (id (rng p)) by A5, FUNCT_1:39 .= f * (id (dom f)) by A4, A11, FUNCT_2:def_1 .= f by RELAT_1:52 ; hence f is one-to-one by A5, A8, A14; ::_thesis: verum end; end; end; hence f is one-to-one ; ::_thesis: verum end; theorem Th62: :: FINSEQ_4:62 for p being FinSequence holds ( p is one-to-one iff card (rng p) = len p ) proof let p be FinSequence; ::_thesis: ( p is one-to-one iff card (rng p) = len p ) thus ( p is one-to-one implies card (rng p) = len p ) ::_thesis: ( card (rng p) = len p implies p is one-to-one ) proof assume p is one-to-one ; ::_thesis: card (rng p) = len p then dom p,p .: (dom p) are_equipotent by CARD_1:33; then dom p, rng p are_equipotent by RELAT_1:113; then Seg (len p), rng p are_equipotent by FINSEQ_1:def_3; then card (Seg (len p)) = card (rng p) by CARD_1:5; hence card (rng p) = len p by FINSEQ_1:57; ::_thesis: verum end; reconsider f = p as Function of (dom p),(rng p) by FUNCT_2:1; reconsider B = dom p as finite set ; assume card (rng p) = len p ; ::_thesis: p is one-to-one then card (rng p) = card (Seg (len p)) by FINSEQ_1:57; then A1: card (rng p) = card B by FINSEQ_1:def_3; dom f is finite ; hence p is one-to-one by A1, Lm1; ::_thesis: verum end; theorem :: FINSEQ_4:63 for A, B being finite set for f being Function of A,B st card A = card B & f is one-to-one holds rng f = B proof let A, B be finite set ; ::_thesis: for f being Function of A,B st card A = card B & f is one-to-one holds rng f = B let f be Function of A,B; ::_thesis: ( card A = card B & f is one-to-one implies rng f = B ) assume that A1: card A = card B and A2: f is one-to-one ; ::_thesis: rng f = B A3: A,B are_equipotent by A1, CARD_1:5; consider p being FinSequence such that A4: rng p = A and A5: p is one-to-one by Th58; dom p,p .: (dom p) are_equipotent by A5, CARD_1:33; then dom p,A are_equipotent by A4, RELAT_1:113; then A6: dom p,B are_equipotent by A3, WELLORD2:15; consider q being FinSequence such that A7: rng q = B and A8: q is one-to-one by Th58; A9: dom q = Seg (len q) by FINSEQ_1:def_3; dom q,q .: (dom q) are_equipotent by A8, CARD_1:33; then dom q,B are_equipotent by A7, RELAT_1:113; then dom p, dom q are_equipotent by A6, WELLORD2:15; then card (dom p) = card (Seg (len q)) by A9, CARD_1:5 .= len q by FINSEQ_1:57 ; then A10: len q = card (Seg (len p)) by FINSEQ_1:def_3 .= len p by FINSEQ_1:57 ; percases ( B = {} or B <> {} ) ; suppose B = {} ; ::_thesis: rng f = B hence rng f = B ; ::_thesis: verum end; supposeA11: B <> {} ; ::_thesis: rng f = B dom (q ") = rng q by A8, FUNCT_1:33; then rng f c= dom (q ") by A7, RELAT_1:def_19; then dom ((q ") * f) = dom f by RELAT_1:27; then rng p = dom ((q ") * f) by A4, A11, FUNCT_2:def_1; then A12: dom (((q ") * f) * p) = dom p by RELAT_1:27 .= Seg (len p) by FINSEQ_1:def_3 ; then reconsider g = ((q ") * f) * p as FinSequence by FINSEQ_1:def_2; g = (q ") * (f * p) by RELAT_1:36; then rng g c= rng (q ") by RELAT_1:26; then rng g c= dom q by A8, FUNCT_1:33; then rng g c= dom g by A10, A12, FINSEQ_1:def_3; then rng g = dom g by A2, A5, A8, Th59; then rng g = dom q by A10, A12, FINSEQ_1:def_3; then A13: rng (q * g) = B by A7, RELAT_1:28; A14: rng f c= rng q by A7, RELAT_1:def_19; A15: rng p = dom f by A4, A11, FUNCT_2:def_1; q * g = q * ((q ") * (f * p)) by RELAT_1:36 .= (q * (q ")) * (f * p) by RELAT_1:36 .= (id (rng q)) * (f * p) by A8, FUNCT_1:39 .= ((id (rng q)) * f) * p by RELAT_1:36 .= f * p by A14, RELAT_1:53 ; hence rng f = B by A13, A15, RELAT_1:28; ::_thesis: verum end; end; end; theorem :: FINSEQ_4:64 for A, B being finite set for f being Function of A,B st card A = card B & rng f = B holds f is one-to-one by Lm1; theorem :: FINSEQ_4:65 for B, A being set for f being Function of A,B st card B in card A & B <> {} holds ex x, y being set st ( x in A & y in A & x <> y & f . x = f . y ) proof let B, A be set ; ::_thesis: for f being Function of A,B st card B in card A & B <> {} holds ex x, y being set st ( x in A & y in A & x <> y & f . x = f . y ) let f be Function of A,B; ::_thesis: ( card B in card A & B <> {} implies ex x, y being set st ( x in A & y in A & x <> y & f . x = f . y ) ) assume that A1: card B in card A and A2: B <> {} and A3: for x, y being set st x in A & y in A & x <> y holds f . x <> f . y ; ::_thesis: contradiction A4: dom f = A by A2, FUNCT_2:def_1; then for x, y being set st x in dom f & y in dom f & f . x = f . y holds x = y by A3; then f is one-to-one by FUNCT_1:def_4; then dom f,f .: (dom f) are_equipotent by CARD_1:33; then dom f, rng f are_equipotent by RELAT_1:113; then A5: card A = card (rng f) by A4, CARD_1:5; rng f c= B by RELAT_1:def_19; then card A c= card B by A5, CARD_1:11; hence contradiction by A1, CARD_1:4; ::_thesis: verum end; theorem Th66: :: FINSEQ_4:66 for A, B being set for f being Function of A,B st card A in card B holds ex x being set st ( x in B & ( for y being set st y in A holds f . y <> x ) ) proof let A, B be set ; ::_thesis: for f being Function of A,B st card A in card B holds ex x being set st ( x in B & ( for y being set st y in A holds f . y <> x ) ) let f be Function of A,B; ::_thesis: ( card A in card B implies ex x being set st ( x in B & ( for y being set st y in A holds f . y <> x ) ) ) assume that A1: card A in card B and A2: for x being set st x in B holds ex y being set st ( y in A & f . y = x ) ; ::_thesis: contradiction A3: dom f = A by A1, CARD_1:27, FUNCT_2:def_1; rng f = B proof thus rng f c= B by RELAT_1:def_19; :: according to XBOOLE_0:def_10 ::_thesis: B c= rng f let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in rng f ) assume x in B ; ::_thesis: x in rng f then ex y being set st ( y in A & f . y = x ) by A2; hence x in rng f by A3, FUNCT_1:def_3; ::_thesis: verum end; then card B c= card A by A3, CARD_1:12; hence contradiction by A1, CARD_1:4; ::_thesis: verum end; begin theorem :: FINSEQ_4:67 for D being non empty set for f being FinSequence of D for p being Element of D holds (f ^ <*p*>) /. ((len f) + 1) = p proof let D be non empty set ; ::_thesis: for f being FinSequence of D for p being Element of D holds (f ^ <*p*>) /. ((len f) + 1) = p let f be FinSequence of D; ::_thesis: for p being Element of D holds (f ^ <*p*>) /. ((len f) + 1) = p let p be Element of D; ::_thesis: (f ^ <*p*>) /. ((len f) + 1) = p len (f ^ <*p*>) = (len f) + (len <*p*>) by FINSEQ_1:22; then ( 1 <= (len f) + 1 & (len f) + 1 <= len (f ^ <*p*>) ) by FINSEQ_1:39, NAT_1:11; then (len f) + 1 in dom (f ^ <*p*>) by FINSEQ_3:25; hence (f ^ <*p*>) /. ((len f) + 1) = (f ^ <*p*>) . ((len f) + 1) by PARTFUN1:def_6 .= p by FINSEQ_1:42 ; ::_thesis: verum end; theorem :: FINSEQ_4:68 for k being Nat for E being non empty set for p, q being FinSequence of E st k in dom p holds (p ^ q) /. k = p /. k proof let k be Nat; ::_thesis: for E being non empty set for p, q being FinSequence of E st k in dom p holds (p ^ q) /. k = p /. k let E be non empty set ; ::_thesis: for p, q being FinSequence of E st k in dom p holds (p ^ q) /. k = p /. k let p, q be FinSequence of E; ::_thesis: ( k in dom p implies (p ^ q) /. k = p /. k ) assume A1: k in dom p ; ::_thesis: (p ^ q) /. k = p /. k then k in dom (p ^ q) by FINSEQ_3:22; hence (p ^ q) /. k = (p ^ q) . k by PARTFUN1:def_6 .= p . k by A1, FINSEQ_1:def_7 .= p /. k by A1, PARTFUN1:def_6 ; ::_thesis: verum end; theorem :: FINSEQ_4:69 for k being Nat for E being non empty set for p, q being FinSequence of E st k in dom q holds (p ^ q) /. ((len p) + k) = q /. k proof let k be Nat; ::_thesis: for E being non empty set for p, q being FinSequence of E st k in dom q holds (p ^ q) /. ((len p) + k) = q /. k let E be non empty set ; ::_thesis: for p, q being FinSequence of E st k in dom q holds (p ^ q) /. ((len p) + k) = q /. k let p, q be FinSequence of E; ::_thesis: ( k in dom q implies (p ^ q) /. ((len p) + k) = q /. k ) assume A1: k in dom q ; ::_thesis: (p ^ q) /. ((len p) + k) = q /. k then (len p) + k in dom (p ^ q) by FINSEQ_1:28; hence (p ^ q) /. ((len p) + k) = (p ^ q) . ((len p) + k) by PARTFUN1:def_6 .= q . k by A1, FINSEQ_1:def_7 .= q /. k by A1, PARTFUN1:def_6 ; ::_thesis: verum end; theorem :: FINSEQ_4:70 for a, m being Nat for D being set for p being FinSequence of D st a in dom (p | m) holds (p | m) /. a = p /. a proof let a, m be Nat; ::_thesis: for D being set for p being FinSequence of D st a in dom (p | m) holds (p | m) /. a = p /. a let D be set ; ::_thesis: for p being FinSequence of D st a in dom (p | m) holds (p | m) /. a = p /. a let p be FinSequence of D; ::_thesis: ( a in dom (p | m) implies (p | m) /. a = p /. a ) assume A1: a in dom (p | m) ; ::_thesis: (p | m) /. a = p /. a then a in (dom p) /\ (Seg m) by RELAT_1:61; then A2: a in dom p by XBOOLE_0:def_4; thus (p | m) /. a = (p | (Seg m)) . a by A1, PARTFUN1:def_6 .= p . a by A1, FUNCT_1:47 .= p /. a by A2, PARTFUN1:def_6 ; ::_thesis: verum end; theorem :: FINSEQ_4:71 for D being set for f being FinSequence of D for n, m being Nat st n in dom f & m in Seg n holds ( m in dom f & (f | n) /. m = f /. m ) proof let D be set ; ::_thesis: for f being FinSequence of D for n, m being Nat st n in dom f & m in Seg n holds ( m in dom f & (f | n) /. m = f /. m ) let f be FinSequence of D; ::_thesis: for n, m being Nat st n in dom f & m in Seg n holds ( m in dom f & (f | n) /. m = f /. m ) let n, m be Nat; ::_thesis: ( n in dom f & m in Seg n implies ( m in dom f & (f | n) /. m = f /. m ) ) assume that A1: n in dom f and A2: m in Seg n ; ::_thesis: ( m in dom f & (f | n) /. m = f /. m ) ( dom f = Seg (len f) & n <= len f ) by A1, FINSEQ_1:def_3, FINSEQ_3:25; then A3: Seg n c= dom f by FINSEQ_1:5; hence m in dom f by A2; ::_thesis: (f | n) /. m = f /. m A4: Seg n = (dom f) /\ (Seg n) by A3, XBOOLE_1:28 .= dom (f | n) by RELAT_1:61 ; hence (f | n) /. m = (f | n) . m by A2, PARTFUN1:def_6 .= f . m by A2, A4, FUNCT_1:47 .= f /. m by A2, A3, PARTFUN1:def_6 ; ::_thesis: verum end; theorem :: FINSEQ_4:72 for n being Nat for X being finite set st n <= card X holds ex A being finite Subset of X st card A = n proof let n be Nat; ::_thesis: for X being finite set st n <= card X holds ex A being finite Subset of X st card A = n let X be finite set ; ::_thesis: ( n <= card X implies ex A being finite Subset of X st card A = n ) assume A1: n <= card X ; ::_thesis: ex A being finite Subset of X st card A = n consider p being FinSequence such that A2: rng p = X and A3: p is one-to-one by Th58; reconsider q = p | (Seg n) as FinSequence by FINSEQ_1:15; n <= len p by A1, A2, A3, Th62; then A4: len q = n by FINSEQ_1:17; reconsider A = rng q as Subset of X by A2, RELAT_1:70; q is one-to-one by A3, FUNCT_1:52; then card A = n by A4, Th62; hence ex A being finite Subset of X st card A = n ; ::_thesis: verum end; theorem :: FINSEQ_4:73 for x being set for f being Function st f is one-to-one & x in rng f holds card (Coim (f,x)) = 1 proof let x be set ; ::_thesis: for f being Function st f is one-to-one & x in rng f holds card (Coim (f,x)) = 1 let f be Function; ::_thesis: ( f is one-to-one & x in rng f implies card (Coim (f,x)) = 1 ) assume ( f is one-to-one & x in rng f ) ; ::_thesis: card (Coim (f,x)) = 1 then f just_once_values x by Th8; hence card (Coim (f,x)) = 1 by Def2; ::_thesis: verum end; definition let x1, x2, x3, x4 be set ; func<*x1,x2,x3,x4*> -> set equals :: FINSEQ_4:def 7 <*x1,x2,x3*> ^ <*x4*>; correctness coherence <*x1,x2,x3*> ^ <*x4*> is set ; ; let x5 be set ; func<*x1,x2,x3,x4,x5*> -> set equals :: FINSEQ_4:def 8 <*x1,x2,x3*> ^ <*x4,x5*>; correctness coherence <*x1,x2,x3*> ^ <*x4,x5*> is set ; ; end; :: deftheorem defines <* FINSEQ_4:def_7_:_ for x1, x2, x3, x4 being set holds <*x1,x2,x3,x4*> = <*x1,x2,x3*> ^ <*x4*>; :: deftheorem defines <* FINSEQ_4:def_8_:_ for x1, x2, x3, x4, x5 being set holds <*x1,x2,x3,x4,x5*> = <*x1,x2,x3*> ^ <*x4,x5*>; registration let x1, x2, x3, x4 be set ; cluster<*x1,x2,x3,x4*> -> Relation-like Function-like non empty ; coherence ( not <*x1,x2,x3,x4*> is empty & <*x1,x2,x3,x4*> is Function-like & <*x1,x2,x3,x4*> is Relation-like ) ; let x5 be set ; cluster<*x1,x2,x3,x4,x5*> -> Relation-like Function-like non empty ; coherence ( not <*x1,x2,x3,x4,x5*> is empty & <*x1,x2,x3,x4,x5*> is Function-like & <*x1,x2,x3,x4,x5*> is Relation-like ) ; end; registration let x1, x2, x3, x4 be set ; cluster<*x1,x2,x3,x4*> -> FinSequence-like ; coherence <*x1,x2,x3,x4*> is FinSequence-like ; let x5 be set ; cluster<*x1,x2,x3,x4,x5*> -> FinSequence-like ; coherence <*x1,x2,x3,x4,x5*> is FinSequence-like ; end; definition let D be non empty set ; let x1, x2, x3, x4 be Element of D; :: original: <* redefine func<*x1,x2,x3,x4*> -> FinSequence of D; coherence <*x1,x2,x3,x4*> is FinSequence of D proof <*x1,x2,x3,x4*> = <*x1,x2,x3*> ^ <*x4*> ; hence <*x1,x2,x3,x4*> is FinSequence of D ; ::_thesis: verum end; end; definition let D be non empty set ; let x1, x2, x3, x4, x5 be Element of D; :: original: <* redefine func<*x1,x2,x3,x4,x5*> -> FinSequence of D; coherence <*x1,x2,x3,x4,x5*> is FinSequence of D proof <*x1,x2,x3,x4,x5*> = <*x1,x2,x3*> ^ <*x4,x5*> ; hence <*x1,x2,x3,x4,x5*> is FinSequence of D ; ::_thesis: verum end; end; theorem Th74: :: FINSEQ_4:74 for x1, x2, x3, x4 being set holds ( <*x1,x2,x3,x4*> = <*x1,x2,x3*> ^ <*x4*> & <*x1,x2,x3,x4*> = <*x1,x2*> ^ <*x3,x4*> & <*x1,x2,x3,x4*> = <*x1*> ^ <*x2,x3,x4*> & <*x1,x2,x3,x4*> = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> ) proof let x1, x2, x3, x4 be set ; ::_thesis: ( <*x1,x2,x3,x4*> = <*x1,x2,x3*> ^ <*x4*> & <*x1,x2,x3,x4*> = <*x1,x2*> ^ <*x3,x4*> & <*x1,x2,x3,x4*> = <*x1*> ^ <*x2,x3,x4*> & <*x1,x2,x3,x4*> = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> ) thus <*x1,x2,x3,x4*> = <*x1,x2,x3*> ^ <*x4*> ; ::_thesis: ( <*x1,x2,x3,x4*> = <*x1,x2*> ^ <*x3,x4*> & <*x1,x2,x3,x4*> = <*x1*> ^ <*x2,x3,x4*> & <*x1,x2,x3,x4*> = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> ) thus <*x1,x2,x3,x4*> = <*x1,x2*> ^ <*x3,x4*> by FINSEQ_1:32; ::_thesis: ( <*x1,x2,x3,x4*> = <*x1*> ^ <*x2,x3,x4*> & <*x1,x2,x3,x4*> = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> ) hence <*x1,x2,x3,x4*> = <*x1*> ^ (<*x2*> ^ <*x3,x4*>) by FINSEQ_1:32 .= <*x1*> ^ <*x2,x3,x4*> by FINSEQ_1:43 ; ::_thesis: <*x1,x2,x3,x4*> = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> thus <*x1,x2,x3,x4*> = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> ; ::_thesis: verum end; theorem Th75: :: FINSEQ_4:75 for x1, x2, x3, x4, x5 being set holds ( <*x1,x2,x3,x4,x5*> = <*x1,x2,x3*> ^ <*x4,x5*> & <*x1,x2,x3,x4,x5*> = <*x1,x2,x3,x4*> ^ <*x5*> & <*x1,x2,x3,x4,x5*> = (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*> & <*x1,x2,x3,x4,x5*> = <*x1,x2*> ^ <*x3,x4,x5*> & <*x1,x2,x3,x4,x5*> = <*x1*> ^ <*x2,x3,x4,x5*> ) proof let x1, x2, x3, x4, x5 be set ; ::_thesis: ( <*x1,x2,x3,x4,x5*> = <*x1,x2,x3*> ^ <*x4,x5*> & <*x1,x2,x3,x4,x5*> = <*x1,x2,x3,x4*> ^ <*x5*> & <*x1,x2,x3,x4,x5*> = (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*> & <*x1,x2,x3,x4,x5*> = <*x1,x2*> ^ <*x3,x4,x5*> & <*x1,x2,x3,x4,x5*> = <*x1*> ^ <*x2,x3,x4,x5*> ) thus <*x1,x2,x3,x4,x5*> = <*x1,x2,x3*> ^ <*x4,x5*> ; ::_thesis: ( <*x1,x2,x3,x4,x5*> = <*x1,x2,x3,x4*> ^ <*x5*> & <*x1,x2,x3,x4,x5*> = (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*> & <*x1,x2,x3,x4,x5*> = <*x1,x2*> ^ <*x3,x4,x5*> & <*x1,x2,x3,x4,x5*> = <*x1*> ^ <*x2,x3,x4,x5*> ) thus A1: <*x1,x2,x3,x4,x5*> = <*x1,x2,x3,x4*> ^ <*x5*> by FINSEQ_1:32; ::_thesis: ( <*x1,x2,x3,x4,x5*> = (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*> & <*x1,x2,x3,x4,x5*> = <*x1,x2*> ^ <*x3,x4,x5*> & <*x1,x2,x3,x4,x5*> = <*x1*> ^ <*x2,x3,x4,x5*> ) thus <*x1,x2,x3,x4,x5*> = (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*> by FINSEQ_1:32; ::_thesis: ( <*x1,x2,x3,x4,x5*> = <*x1,x2*> ^ <*x3,x4,x5*> & <*x1,x2,x3,x4,x5*> = <*x1*> ^ <*x2,x3,x4,x5*> ) thus <*x1,x2,x3,x4,x5*> = (<*x1,x2*> ^ (<*x3*> ^ <*x4*>)) ^ <*x5*> by A1, FINSEQ_1:32 .= <*x1,x2*> ^ <*x3,x4,x5*> by FINSEQ_1:32 ; ::_thesis: <*x1,x2,x3,x4,x5*> = <*x1*> ^ <*x2,x3,x4,x5*> hence <*x1,x2,x3,x4,x5*> = <*x1*> ^ (<*x2*> ^ <*x3,x4,x5*>) by FINSEQ_1:32 .= <*x1*> ^ <*x2,x3,x4,x5*> by Th74 ; ::_thesis: verum end; theorem Th76: :: FINSEQ_4:76 for x1, x2, x3, x4 being set for p being FinSequence holds ( p = <*x1,x2,x3,x4*> iff ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) ) proof let x1, x2, x3, x4 be set ; ::_thesis: for p being FinSequence holds ( p = <*x1,x2,x3,x4*> iff ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) ) let p be FinSequence; ::_thesis: ( p = <*x1,x2,x3,x4*> iff ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) ) thus ( p = <*x1,x2,x3,x4*> implies ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) ) ::_thesis: ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 implies p = <*x1,x2,x3,x4*> ) proof set p3 = <*x1,x2,x3*>; assume A1: p = <*x1,x2,x3,x4*> ; ::_thesis: ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) hence len p = (len <*x1,x2,x3*>) + (len <*x4*>) by FINSEQ_1:22 .= 3 + (len <*x4*>) by FINSEQ_1:45 .= 3 + 1 by FINSEQ_1:40 .= 4 ; ::_thesis: ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) A2: dom <*x1,x2,x3*> = {1,2,3} by FINSEQ_3:1, FINSEQ_1:89; then 1 in dom <*x1,x2,x3*> by ENUMSET1:def_1; hence p . 1 = <*x1,x2,x3*> . 1 by A1, FINSEQ_1:def_7 .= x1 by FINSEQ_1:45 ; ::_thesis: ( p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) 2 in dom <*x1,x2,x3*> by A2, ENUMSET1:def_1; hence p . 2 = <*x1,x2,x3*> . 2 by A1, FINSEQ_1:def_7 .= x2 by FINSEQ_1:45 ; ::_thesis: ( p . 3 = x3 & p . 4 = x4 ) 3 in dom <*x1,x2,x3*> by A2, ENUMSET1:def_1; hence p . 3 = <*x1,x2,x3*> . 3 by A1, FINSEQ_1:def_7 .= x3 by FINSEQ_1:45 ; ::_thesis: p . 4 = x4 1 in {1} by TARSKI:def_1; then A3: 1 in dom <*x4*> by FINSEQ_1:2, FINSEQ_1:def_8; thus p . 4 = (<*x1,x2,x3*> ^ <*x4*>) . (3 + 1) by A1 .= (<*x1,x2,x3*> ^ <*x4*>) . ((len <*x1,x2,x3*>) + 1) by FINSEQ_1:45 .= <*x4*> . 1 by A3, FINSEQ_1:def_7 .= x4 by FINSEQ_1:def_8 ; ::_thesis: verum end; assume that A4: len p = 4 and A5: p . 1 = x1 and A6: p . 2 = x2 and A7: p . 3 = x3 and A8: p . 4 = x4 ; ::_thesis: p = <*x1,x2,x3,x4*> A9: for k being Nat st k in dom <*x1,x2,x3*> holds p . k = <*x1,x2,x3*> . k proof A10: len <*x1,x2,x3*> = 3 by FINSEQ_1:45; let k be Nat; ::_thesis: ( k in dom <*x1,x2,x3*> implies p . k = <*x1,x2,x3*> . k ) assume k in dom <*x1,x2,x3*> ; ::_thesis: p . k = <*x1,x2,x3*> . k then A11: k in {1,2,3} by A10, FINSEQ_1:def_3, FINSEQ_3:1; percases ( k = 1 or k = 2 or k = 3 ) by A11, ENUMSET1:def_1; suppose k = 1 ; ::_thesis: p . k = <*x1,x2,x3*> . k hence p . k = <*x1,x2,x3*> . k by A5, FINSEQ_1:45; ::_thesis: verum end; suppose k = 2 ; ::_thesis: p . k = <*x1,x2,x3*> . k hence p . k = <*x1,x2,x3*> . k by A6, FINSEQ_1:45; ::_thesis: verum end; suppose k = 3 ; ::_thesis: p . k = <*x1,x2,x3*> . k hence p . k = <*x1,x2,x3*> . k by A7, FINSEQ_1:45; ::_thesis: verum end; end; end; A12: for k being Nat st k in dom <*x4*> holds p . ((len <*x1,x2,x3*>) + k) = <*x4*> . k proof let k be Nat; ::_thesis: ( k in dom <*x4*> implies p . ((len <*x1,x2,x3*>) + k) = <*x4*> . k ) assume k in dom <*x4*> ; ::_thesis: p . ((len <*x1,x2,x3*>) + k) = <*x4*> . k then k in {1} by FINSEQ_1:2, FINSEQ_1:def_8; then A13: k = 1 by TARSKI:def_1; hence p . ((len <*x1,x2,x3*>) + k) = p . (3 + 1) by FINSEQ_1:45 .= <*x4*> . k by A8, A13, FINSEQ_1:def_8 ; ::_thesis: verum end; dom p = Seg (3 + 1) by A4, FINSEQ_1:def_3 .= Seg ((len <*x1,x2,x3*>) + 1) by FINSEQ_1:45 .= Seg ((len <*x1,x2,x3*>) + (len <*x4*>)) by FINSEQ_1:39 ; hence p = <*x1,x2,x3,x4*> by A9, A12, FINSEQ_1:def_7; ::_thesis: verum end; theorem :: FINSEQ_4:77 canceled; theorem Th78: :: FINSEQ_4:78 for x1, x2, x3, x4, x5 being set for p being FinSequence holds ( p = <*x1,x2,x3,x4,x5*> iff ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) ) proof let x1, x2, x3, x4, x5 be set ; ::_thesis: for p being FinSequence holds ( p = <*x1,x2,x3,x4,x5*> iff ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) ) let p be FinSequence; ::_thesis: ( p = <*x1,x2,x3,x4,x5*> iff ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) ) set p4 = <*x1,x2,x3,x4*>; thus ( p = <*x1,x2,x3,x4,x5*> implies ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) ) ::_thesis: ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 implies p = <*x1,x2,x3,x4,x5*> ) proof set p4 = <*x1,x2,x3,x4*>; 1 in {1} by TARSKI:def_1; then A1: 1 in dom <*x5*> by FINSEQ_1:2, FINSEQ_1:def_8; assume A2: p = <*x1,x2,x3,x4,x5*> ; ::_thesis: ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) then A3: p = <*x1,x2,x3,x4*> ^ <*x5*> by Th75; thus len p = len (<*x1,x2,x3,x4*> ^ <*x5*>) by A2, Th75 .= (len <*x1,x2,x3,x4*>) + (len <*x5*>) by FINSEQ_1:22 .= 4 + (len <*x5*>) by Th76 .= 4 + 1 by FINSEQ_1:40 .= 5 ; ::_thesis: ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) A4: dom <*x1,x2,x3,x4*> = {1,2,3,4} by FINSEQ_1:89, FINSEQ_3:2; then 1 in dom <*x1,x2,x3,x4*> by ENUMSET1:def_2; hence p . 1 = <*x1,x2,x3,x4*> . 1 by A3, FINSEQ_1:def_7 .= x1 by Th76 ; ::_thesis: ( p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) 2 in dom <*x1,x2,x3,x4*> by A4, ENUMSET1:def_2; hence p . 2 = <*x1,x2,x3,x4*> . 2 by A3, FINSEQ_1:def_7 .= x2 by Th76 ; ::_thesis: ( p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) 3 in dom <*x1,x2,x3,x4*> by A4, ENUMSET1:def_2; hence p . 3 = <*x1,x2,x3,x4*> . 3 by A3, FINSEQ_1:def_7 .= x3 by Th76 ; ::_thesis: ( p . 4 = x4 & p . 5 = x5 ) 4 in dom <*x1,x2,x3,x4*> by A4, ENUMSET1:def_2; hence p . 4 = <*x1,x2,x3,x4*> . 4 by A3, FINSEQ_1:def_7 .= x4 by Th76 ; ::_thesis: p . 5 = x5 thus p . 5 = (<*x1,x2,x3,x4*> ^ <*x5*>) . (4 + 1) by A2, Th75 .= (<*x1,x2,x3,x4*> ^ <*x5*>) . ((len <*x1,x2,x3,x4*>) + 1) by Th76 .= <*x5*> . 1 by A1, FINSEQ_1:def_7 .= x5 by FINSEQ_1:def_8 ; ::_thesis: verum end; assume that A5: len p = 5 and A6: p . 1 = x1 and A7: p . 2 = x2 and A8: p . 3 = x3 and A9: p . 4 = x4 and A10: p . 5 = x5 ; ::_thesis: p = <*x1,x2,x3,x4,x5*> A11: for k being Nat st k in dom <*x1,x2,x3,x4*> holds p . k = <*x1,x2,x3,x4*> . k proof A12: len <*x1,x2,x3,x4*> = 4 by Th76; let k be Nat; ::_thesis: ( k in dom <*x1,x2,x3,x4*> implies p . k = <*x1,x2,x3,x4*> . k ) assume k in dom <*x1,x2,x3,x4*> ; ::_thesis: p . k = <*x1,x2,x3,x4*> . k then A13: k in {1,2,3,4} by A12, FINSEQ_1:def_3, FINSEQ_3:2; percases ( k = 1 or k = 2 or k = 3 or k = 4 ) by A13, ENUMSET1:def_2; suppose k = 1 ; ::_thesis: p . k = <*x1,x2,x3,x4*> . k hence p . k = <*x1,x2,x3,x4*> . k by A6, Th76; ::_thesis: verum end; suppose k = 2 ; ::_thesis: p . k = <*x1,x2,x3,x4*> . k hence p . k = <*x1,x2,x3,x4*> . k by A7, Th76; ::_thesis: verum end; suppose k = 3 ; ::_thesis: p . k = <*x1,x2,x3,x4*> . k hence p . k = <*x1,x2,x3,x4*> . k by A8, Th76; ::_thesis: verum end; suppose k = 4 ; ::_thesis: p . k = <*x1,x2,x3,x4*> . k hence p . k = <*x1,x2,x3,x4*> . k by A9, Th76; ::_thesis: verum end; end; end; A14: for k being Nat st k in dom <*x5*> holds p . ((len <*x1,x2,x3,x4*>) + k) = <*x5*> . k proof let k be Nat; ::_thesis: ( k in dom <*x5*> implies p . ((len <*x1,x2,x3,x4*>) + k) = <*x5*> . k ) assume k in dom <*x5*> ; ::_thesis: p . ((len <*x1,x2,x3,x4*>) + k) = <*x5*> . k then k in {1} by FINSEQ_1:2, FINSEQ_1:def_8; then A15: k = 1 by TARSKI:def_1; hence p . ((len <*x1,x2,x3,x4*>) + k) = p . (4 + 1) by Th76 .= <*x5*> . k by A10, A15, FINSEQ_1:def_8 ; ::_thesis: verum end; dom p = Seg (4 + 1) by A5, FINSEQ_1:def_3 .= Seg ((len <*x1,x2,x3,x4*>) + 1) by Th76 .= Seg ((len <*x1,x2,x3,x4*>) + (len <*x5*>)) by FINSEQ_1:39 ; hence p = <*x1,x2,x3,x4*> ^ <*x5*> by A11, A14, FINSEQ_1:def_7 .= <*x1,x2,x3,x4,x5*> by Th75 ; ::_thesis: verum end; theorem :: FINSEQ_4:79 canceled; theorem :: FINSEQ_4:80 for ND being non empty set for y1, y2, y3, y4 being Element of ND holds ( <*y1,y2,y3,y4*> /. 1 = y1 & <*y1,y2,y3,y4*> /. 2 = y2 & <*y1,y2,y3,y4*> /. 3 = y3 & <*y1,y2,y3,y4*> /. 4 = y4 ) proof let ND be non empty set ; ::_thesis: for y1, y2, y3, y4 being Element of ND holds ( <*y1,y2,y3,y4*> /. 1 = y1 & <*y1,y2,y3,y4*> /. 2 = y2 & <*y1,y2,y3,y4*> /. 3 = y3 & <*y1,y2,y3,y4*> /. 4 = y4 ) let y1, y2, y3, y4 be Element of ND; ::_thesis: ( <*y1,y2,y3,y4*> /. 1 = y1 & <*y1,y2,y3,y4*> /. 2 = y2 & <*y1,y2,y3,y4*> /. 3 = y3 & <*y1,y2,y3,y4*> /. 4 = y4 ) set s = <*y1,y2,y3,y4*>; A1: ( 2 in {1,2,3,4} & 3 in {1,2,3,4} ) by FINSEQ_3:2; A2: ( <*y1,y2,y3,y4*> . 2 = y2 & <*y1,y2,y3,y4*> . 3 = y3 ) by Th76; A3: 4 in {1,2,3,4} by FINSEQ_3:2; A4: ( <*y1,y2,y3,y4*> . 4 = y4 & 1 in {1,2,3,4} ) by Th76, FINSEQ_3:2; ( dom <*y1,y2,y3,y4*> = {1,2,3,4} & <*y1,y2,y3,y4*> . 1 = y1 ) by Th76, FINSEQ_1:89, FINSEQ_3:2; hence ( <*y1,y2,y3,y4*> /. 1 = y1 & <*y1,y2,y3,y4*> /. 2 = y2 & <*y1,y2,y3,y4*> /. 3 = y3 & <*y1,y2,y3,y4*> /. 4 = y4 ) by A2, A4, A1, A3, PARTFUN1:def_6; ::_thesis: verum end; theorem :: FINSEQ_4:81 for ND being non empty set for y1, y2, y3, y4, y5 being Element of ND holds ( <*y1,y2,y3,y4,y5*> /. 1 = y1 & <*y1,y2,y3,y4,y5*> /. 2 = y2 & <*y1,y2,y3,y4,y5*> /. 3 = y3 & <*y1,y2,y3,y4,y5*> /. 4 = y4 & <*y1,y2,y3,y4,y5*> /. 5 = y5 ) proof let ND be non empty set ; ::_thesis: for y1, y2, y3, y4, y5 being Element of ND holds ( <*y1,y2,y3,y4,y5*> /. 1 = y1 & <*y1,y2,y3,y4,y5*> /. 2 = y2 & <*y1,y2,y3,y4,y5*> /. 3 = y3 & <*y1,y2,y3,y4,y5*> /. 4 = y4 & <*y1,y2,y3,y4,y5*> /. 5 = y5 ) let y1, y2, y3, y4, y5 be Element of ND; ::_thesis: ( <*y1,y2,y3,y4,y5*> /. 1 = y1 & <*y1,y2,y3,y4,y5*> /. 2 = y2 & <*y1,y2,y3,y4,y5*> /. 3 = y3 & <*y1,y2,y3,y4,y5*> /. 4 = y4 & <*y1,y2,y3,y4,y5*> /. 5 = y5 ) set s = <*y1,y2,y3,y4,y5*>; set i5 = {1,2,3,4,5}; A1: ( 1 in {1,2,3,4,5} & 2 in {1,2,3,4,5} ) by FINSEQ_3:3; A2: ( 3 in {1,2,3,4,5} & 4 in {1,2,3,4,5} ) by FINSEQ_3:3; A3: ( <*y1,y2,y3,y4,y5*> . 4 = y4 & <*y1,y2,y3,y4,y5*> . 5 = y5 ) by Th78; A4: ( <*y1,y2,y3,y4,y5*> . 2 = y2 & <*y1,y2,y3,y4,y5*> . 3 = y3 ) by Th78; A5: 5 in {1,2,3,4,5} by FINSEQ_3:3; ( dom <*y1,y2,y3,y4,y5*> = {1,2,3,4,5} & <*y1,y2,y3,y4,y5*> . 1 = y1 ) by Th78, FINSEQ_1:89, FINSEQ_3:3; hence ( <*y1,y2,y3,y4,y5*> /. 1 = y1 & <*y1,y2,y3,y4,y5*> /. 2 = y2 & <*y1,y2,y3,y4,y5*> /. 3 = y3 & <*y1,y2,y3,y4,y5*> /. 4 = y4 & <*y1,y2,y3,y4,y5*> /. 5 = y5 ) by A4, A3, A1, A2, A5, PARTFUN1:def_6; ::_thesis: verum end; scheme :: FINSEQ_4:sch 1 Sch1{ F1() -> non empty set , F2() -> Nat, P1[ set , set ] } : ex f being FinSequence of F1() st ( len f = F2() & ( for n being Nat st n in Seg F2() holds P1[n,f /. n] ) ) provided A1: for n being Nat st n in Seg F2() holds ex d being Element of F1() st P1[n,d] proof defpred S1[ set , set ] means ( P1[$1,$2] & $2 in F1() ); reconsider X = F1() as set ; A2: now__::_thesis:_for_x_being_set_st_x_in_Seg_F2()_holds_ ex_y_being_set_st_ (_y_in_X_&_S1[x,y]_) let x be set ; ::_thesis: ( x in Seg F2() implies ex y being set st ( y in X & S1[x,y] ) ) assume A3: x in Seg F2() ; ::_thesis: ex y being set st ( y in X & S1[x,y] ) then reconsider x9 = x as Element of NAT ; consider d being Element of F1() such that A4: P1[x9,d] by A1, A3; reconsider y = d as set ; take y = y; ::_thesis: ( y in X & S1[x,y] ) thus ( y in X & S1[x,y] ) by A4; ::_thesis: verum end; consider f being Function such that A5: ( dom f = Seg F2() & rng f c= X & ( for x being set st x in Seg F2() holds S1[x,f . x] ) ) from FUNCT_1:sch_5(A2); reconsider f = f as FinSequence by A5, FINSEQ_1:def_2; reconsider f = f as FinSequence of F1() by A5, FINSEQ_1:def_4; take f ; ::_thesis: ( len f = F2() & ( for n being Nat st n in Seg F2() holds P1[n,f /. n] ) ) F2() in NAT by ORDINAL1:def_12; hence len f = F2() by A5, FINSEQ_1:def_3; ::_thesis: for n being Nat st n in Seg F2() holds P1[n,f /. n] let n be Nat; ::_thesis: ( n in Seg F2() implies P1[n,f /. n] ) assume A6: n in Seg F2() ; ::_thesis: P1[n,f /. n] then P1[n,f . n] by A5; hence P1[n,f /. n] by A5, A6, PARTFUN1:def_6; ::_thesis: verum end; theorem Th82: :: FINSEQ_4:82 for D being non empty set for p, q being FinSequence of D st p c= q holds ex p9 being FinSequence of D st p ^ p9 = q proof let D be non empty set ; ::_thesis: for p, q being FinSequence of D st p c= q holds ex p9 being FinSequence of D st p ^ p9 = q let p, q be FinSequence of D; ::_thesis: ( p c= q implies ex p9 being FinSequence of D st p ^ p9 = q ) assume A1: p c= q ; ::_thesis: ex p9 being FinSequence of D st p ^ p9 = q ( dom p = Seg (len p) & dom q = Seg (len q) ) by FINSEQ_1:def_3; then Seg (len p) c= Seg (len q) by A1, GRFUNC_1:2; then len p <= len q by FINSEQ_1:5; then reconsider N = (len q) - (len p) as Element of NAT by INT_1:3, XREAL_1:48; defpred S1[ Nat, set ] means q /. ((len p) + $1) = $2; A2: for n being Nat st n in Seg N holds ex d being Element of D st S1[n,d] ; consider f being FinSequence of D such that A3: len f = N and A4: for n being Nat st n in Seg N holds S1[n,f /. n] from FINSEQ_4:sch_1(A2); take f ; ::_thesis: p ^ f = q A5: len (p ^ f) = (len p) + N by A3, FINSEQ_1:22 .= len q ; now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_(p_^_f)_holds_ (p_^_f)_._k_=_q_._k let k be Nat; ::_thesis: ( 1 <= k & k <= len (p ^ f) implies (p ^ f) . b1 = q . b1 ) assume that A6: 1 <= k and A7: k <= len (p ^ f) ; ::_thesis: (p ^ f) . b1 = q . b1 A8: k in NAT by ORDINAL1:def_12; then k in Seg (len q) by A5, A6, A7; then A9: k in dom q by FINSEQ_1:def_3; percases ( k <= len p or len p < k ) ; suppose k <= len p ; ::_thesis: (p ^ f) . b1 = q . b1 then k in Seg (len p) by A6, A8; then A10: k in dom p by FINSEQ_1:def_3; hence (p ^ f) . k = p . k by FINSEQ_1:def_7 .= q . k by A1, A10, GRFUNC_1:2 ; ::_thesis: verum end; supposeA11: len p < k ; ::_thesis: (p ^ f) . b1 = q . b1 then k - (len p) > 0 by XREAL_1:50; then reconsider kk = k - (len p) as Element of NAT by INT_1:3; k <= (len p) + (len f) by A7, FINSEQ_1:22; then A12: kk <= ((len p) + (len f)) - (len p) by XREAL_1:9; k - (len p) >= 0 + 1 by A11, INT_1:7, XREAL_1:50; then A13: kk in Seg (len f) by A12; then A14: kk in dom f by FINSEQ_1:def_3; thus (p ^ f) . k = f . kk by A7, A11, FINSEQ_1:24 .= f /. kk by A14, PARTFUN1:def_6 .= q /. ((len p) + kk) by A3, A4, A13 .= q . k by A9, PARTFUN1:def_6 ; ::_thesis: verum end; end; end; hence p ^ f = q by A5, FINSEQ_1:14; ::_thesis: verum end; theorem :: FINSEQ_4:83 for D being non empty set for p, q being FinSequence of D for i being Element of NAT st p c= q & 1 <= i & i <= len p holds q . i = p . i proof let D be non empty set ; ::_thesis: for p, q being FinSequence of D for i being Element of NAT st p c= q & 1 <= i & i <= len p holds q . i = p . i let p, q be FinSequence of D; ::_thesis: for i being Element of NAT st p c= q & 1 <= i & i <= len p holds q . i = p . i let i be Element of NAT ; ::_thesis: ( p c= q & 1 <= i & i <= len p implies q . i = p . i ) assume p c= q ; ::_thesis: ( not 1 <= i or not i <= len p or q . i = p . i ) then A1: ex p9 being FinSequence of D st p ^ p9 = q by Th82; assume ( 1 <= i & i <= len p ) ; ::_thesis: q . i = p . i hence q . i = p . i by A1, FINSEQ_1:64; ::_thesis: verum end; scheme :: FINSEQ_4:sch 2 PiLambdaD{ F1() -> non empty set , F2() -> Nat, F3( set ) -> Element of F1() } : ex g being FinSequence of F1() st ( len g = F2() & ( for n being Nat st n in dom g holds g /. n = F3(n) ) ) proof consider g being FinSequence of F1() such that A1: ( len g = F2() & ( for n being Nat st n in dom g holds g . n = F3(n) ) ) from FINSEQ_2:sch_1(); take g ; ::_thesis: ( len g = F2() & ( for n being Nat st n in dom g holds g /. n = F3(n) ) ) thus len g = F2() by A1; ::_thesis: for n being Nat st n in dom g holds g /. n = F3(n) let n be Nat; ::_thesis: ( n in dom g implies g /. n = F3(n) ) assume A2: n in dom g ; ::_thesis: g /. n = F3(n) then g . n = F3(n) by A1; hence g /. n = F3(n) by A2, PARTFUN1:def_6; ::_thesis: verum end; registration let x1, x2, x3, x4 be set ; cluster<*x1,x2,x3,x4*> -> 4 -element ; coherence <*x1,x2,x3,x4*> is 4 -element ; let x5 be set ; cluster<*x1,x2,x3,x4,x5*> -> 5 -element ; coherence <*x1,x2,x3,x4,x5*> is 5 -element ; end; begin theorem :: FINSEQ_4:84 for m, n being Nat st m < n holds ex p being Element of NAT st ( n = m + p & 1 <= p ) proof let m, n be Nat; ::_thesis: ( m < n implies ex p being Element of NAT st ( n = m + p & 1 <= p ) ) assume A1: m < n ; ::_thesis: ex p being Element of NAT st ( n = m + p & 1 <= p ) then consider p being Nat such that A2: n = m + p by NAT_1:10; reconsider p = p as Element of NAT by ORDINAL1:def_12; take p ; ::_thesis: ( n = m + p & 1 <= p ) thus n = m + p by A2; ::_thesis: 1 <= p assume p < 1 ; ::_thesis: contradiction then p < 0 + 1 ; then p = 0 by NAT_1:13; hence contradiction by A1, A2; ::_thesis: verum end; theorem :: FINSEQ_4:85 for S being set for D1, D2 being non empty set for f1 being Function of S,D1 for f2 being Function of D1,D2 st f1 is bijective & f2 is bijective holds f2 * f1 is bijective proof let S be set ; ::_thesis: for D1, D2 being non empty set for f1 being Function of S,D1 for f2 being Function of D1,D2 st f1 is bijective & f2 is bijective holds f2 * f1 is bijective let D1, D2 be non empty set ; ::_thesis: for f1 being Function of S,D1 for f2 being Function of D1,D2 st f1 is bijective & f2 is bijective holds f2 * f1 is bijective let f1 be Function of S,D1; ::_thesis: for f2 being Function of D1,D2 st f1 is bijective & f2 is bijective holds f2 * f1 is bijective let f2 be Function of D1,D2; ::_thesis: ( f1 is bijective & f2 is bijective implies f2 * f1 is bijective ) set f3 = f2 * f1; A1: dom f2 = D1 by FUNCT_2:def_1; assume A2: ( f1 is bijective & f2 is bijective ) ; ::_thesis: f2 * f1 is bijective then ( rng f2 = D2 & rng f1 = D1 ) by FUNCT_2:def_3; then rng (f2 * f1) = D2 by A1, RELAT_1:28; then ( f2 * f1 is one-to-one & f2 * f1 is onto ) by A2, FUNCT_2:def_3; hence f2 * f1 is bijective ; ::_thesis: verum end; theorem :: FINSEQ_4:86 for Y being set for E1, E2 being Equivalence_Relation of Y st Class E1 = Class E2 holds E1 = E2 proof let Y be set ; ::_thesis: for E1, E2 being Equivalence_Relation of Y st Class E1 = Class E2 holds E1 = E2 let E1, E2 be Equivalence_Relation of Y; ::_thesis: ( Class E1 = Class E2 implies E1 = E2 ) assume A1: Class E1 = Class E2 ; ::_thesis: E1 = E2 now__::_thesis:_for_x_being_set_holds_ (_(_x_in_E1_implies_x_in_E2_)_&_(_x_in_E2_implies_x_in_E1_)_) let x be set ; ::_thesis: ( ( x in E1 implies x in E2 ) & ( x in E2 implies x in E1 ) ) hereby ::_thesis: ( x in E2 implies x in E1 ) assume A2: x in E1 ; ::_thesis: x in E2 then consider a, b being set such that A3: x = [a,b] and A4: a in Y and A5: b in Y by RELSET_1:2; reconsider a = a, b = b as Element of Y by A4, A5; Class (E1,b) in Class E2 by A1, A4, EQREL_1:def_3; then consider c being set such that c in Y and A6: Class (E1,b) = Class (E2,c) by EQREL_1:def_3; b in Class (E1,b) by A4, EQREL_1:20; then [b,c] in E2 by A6, EQREL_1:19; then A7: [c,b] in E2 by EQREL_1:6; a in Class (E1,b) by A2, A3, EQREL_1:19; then [a,c] in E2 by A6, EQREL_1:19; hence x in E2 by A3, A7, EQREL_1:7; ::_thesis: verum end; assume A8: x in E2 ; ::_thesis: x in E1 then consider a, b being set such that A9: x = [a,b] and A10: a in Y and A11: b in Y by RELSET_1:2; reconsider a = a, b = b as Element of Y by A10, A11; Class (E2,b) in Class E1 by A1, A10, EQREL_1:def_3; then consider c being set such that c in Y and A12: Class (E2,b) = Class (E1,c) by EQREL_1:def_3; b in Class (E2,b) by A10, EQREL_1:20; then [b,c] in E1 by A12, EQREL_1:19; then A13: [c,b] in E1 by EQREL_1:6; a in Class (E2,b) by A8, A9, EQREL_1:19; then [a,c] in E1 by A12, EQREL_1:19; hence x in E1 by A9, A13, EQREL_1:7; ::_thesis: verum end; hence E1 = E2 by TARSKI:1; ::_thesis: verum end; registration let Z be finite set ; cluster -> finite for a_partition of Z; coherence for b1 being a_partition of Z holds b1 is finite ; end; registration let X be non empty finite set ; cluster non empty finite V38() with_non-empty_elements for a_partition of X; existence ex b1 being a_partition of X st ( not b1 is empty & b1 is finite ) proof set p = the a_partition of X; take the a_partition of X ; ::_thesis: ( not the a_partition of X is empty & the a_partition of X is finite ) thus ( not the a_partition of X is empty & the a_partition of X is finite ) ; ::_thesis: verum end; end; theorem Th87: :: FINSEQ_4:87 for X being non empty set for PX being a_partition of X for Pi being set st Pi in PX holds ex x being Element of X st x in Pi proof let X be non empty set ; ::_thesis: for PX being a_partition of X for Pi being set st Pi in PX holds ex x being Element of X st x in Pi let PX be a_partition of X; ::_thesis: for Pi being set st Pi in PX holds ex x being Element of X st x in Pi let Pi be set ; ::_thesis: ( Pi in PX implies ex x being Element of X st x in Pi ) assume Pi in PX ; ::_thesis: ex x being Element of X st x in Pi then reconsider Pi = Pi as Element of PX ; set q = the Element of Pi; A1: Pi <> {} by EQREL_1:def_4; then the Element of Pi in Pi ; then reconsider q = the Element of Pi as Element of X ; take q ; ::_thesis: q in Pi thus q in Pi by A1; ::_thesis: verum end; theorem :: FINSEQ_4:88 for X being non empty finite set for PX being a_partition of X holds card PX <= card X proof let X be non empty finite set ; ::_thesis: for PX being a_partition of X holds card PX <= card X let PX be a_partition of X; ::_thesis: card PX <= card X assume card PX > card X ; ::_thesis: contradiction then card (card X) in card (card PX) by NAT_1:41; then consider Pi being set such that A1: Pi in PX and A2: for x being set st x in X holds (proj PX) . x <> Pi by Th66; reconsider Pi = Pi as Element of PX by A1; consider q being Element of X such that A3: q in Pi by Th87; reconsider Pq = (proj PX) . q as Element of PX ; A4: ( Pq = Pi or Pq misses Pi ) by EQREL_1:def_4; q in Pq by EQREL_1:def_9; hence contradiction by A2, A3, A4, XBOOLE_0:3; ::_thesis: verum end; theorem :: FINSEQ_4:89 for A being non empty finite set for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 holds card PA2 <= card PA1 proof let A be non empty finite set ; ::_thesis: for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 holds card PA2 <= card PA1 let PA1, PA2 be a_partition of A; ::_thesis: ( PA1 is_finer_than PA2 implies card PA2 <= card PA1 ) defpred S1[ set , set ] means $1 c= $2; assume PA1 is_finer_than PA2 ; ::_thesis: card PA2 <= card PA1 then A1: for e being set st e in PA1 holds ex u being set st ( u in PA2 & S1[e,u] ) by SETFAM_1:def_2; consider f being Function of PA1,PA2 such that A2: for e being set st e in PA1 holds S1[e,f . e] from FUNCT_2:sch_1(A1); assume card PA1 < card PA2 ; ::_thesis: contradiction then card (card PA1) in card (card PA2) by NAT_1:41; then consider p2i being set such that A3: p2i in PA2 and A4: for x being set st x in PA1 holds f . x <> p2i by Th66; reconsider p2i = p2i as Element of PA2 by A3; consider q being Element of A such that A5: q in p2i by Th87; reconsider p2q = f . ((proj PA1) . q) as Element of PA2 ; A6: ( p2q = p2i or p2q misses p2i ) by EQREL_1:def_4; ( q in (proj PA1) . q & (proj PA1) . q c= p2q ) by A2, EQREL_1:def_9; hence contradiction by A4, A5, A6, XBOOLE_0:3; ::_thesis: verum end; theorem Th90: :: FINSEQ_4:90 for A being non empty finite set for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 holds for p2 being Element of PA2 ex p1 being Element of PA1 st p1 c= p2 proof let A be non empty finite set ; ::_thesis: for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 holds for p2 being Element of PA2 ex p1 being Element of PA1 st p1 c= p2 let PA1, PA2 be a_partition of A; ::_thesis: ( PA1 is_finer_than PA2 implies for p2 being Element of PA2 ex p1 being Element of PA1 st p1 c= p2 ) assume A1: PA1 is_finer_than PA2 ; ::_thesis: for p2 being Element of PA2 ex p1 being Element of PA1 st p1 c= p2 let p2 be Element of PA2; ::_thesis: ex p1 being Element of PA1 st p1 c= p2 consider E1 being Equivalence_Relation of A such that A2: PA1 = Class E1 by EQREL_1:34; reconsider p29 = p2 as Subset of A ; consider E2 being Equivalence_Relation of A such that A3: PA2 = Class E2 by EQREL_1:34; consider a being set such that A4: a in A and A5: p29 = Class (E2,a) by A3, EQREL_1:def_3; A6: a in Class (E1,a) by A4, EQREL_1:20; reconsider E1a = Class (E1,a) as Element of PA1 by A2, A4, EQREL_1:def_3; consider p22 being set such that A7: p22 in PA2 and A8: E1a c= p22 by A1, SETFAM_1:def_2; reconsider p229 = p22 as Subset of A by A7; take E1a ; ::_thesis: E1a c= p2 ex b being set st ( b in A & p229 = Class (E2,b) ) by A3, A7, EQREL_1:def_3; hence E1a c= p2 by A5, A8, A6, EQREL_1:23; ::_thesis: verum end; theorem :: FINSEQ_4:91 for A being non empty finite set for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 & card PA1 = card PA2 holds PA1 = PA2 proof let A be non empty finite set ; ::_thesis: for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 & card PA1 = card PA2 holds PA1 = PA2 let PA1, PA2 be a_partition of A; ::_thesis: ( PA1 is_finer_than PA2 & card PA1 = card PA2 implies PA1 = PA2 ) defpred S1[ set , set ] means $1 c= $2; assume that A1: PA1 is_finer_than PA2 and A2: card PA1 = card PA2 ; ::_thesis: PA1 = PA2 A3: for e being set st e in PA1 holds ex u being set st ( u in PA2 & S1[e,u] ) by A1, SETFAM_1:def_2; consider f being Function of PA1,PA2 such that A4: for e being set st e in PA1 holds S1[e,f . e] from FUNCT_2:sch_1(A3); A5: dom f = PA1 by FUNCT_2:def_1; A6: PA2 c= rng f proof let p2 be set ; :: according to TARSKI:def_3 ::_thesis: ( not p2 in PA2 or p2 in rng f ) assume p2 in PA2 ; ::_thesis: p2 in rng f then reconsider p29 = p2 as Element of PA2 ; consider p1 being Element of PA1 such that A7: p1 c= p29 by A1, Th90; reconsider fp1 = f . p1 as Subset of A by TARSKI:def_3; A8: p1 c= f . p1 by A4; p29 meets f . p1 proof ex x being Element of A st x in p1 by Th87; hence p29 meets f . p1 by A7, A8, XBOOLE_0:3; ::_thesis: verum end; then p29 = fp1 by EQREL_1:def_4; hence p2 in rng f by A5, FUNCT_1:def_3; ::_thesis: verum end; rng f c= PA2 by RELAT_1:def_19; then rng f = PA2 by A6, XBOOLE_0:def_10; then A9: f is one-to-one by A2, Lm1; A10: for x being Element of PA1 holds x = f . x proof let x be Element of PA1; ::_thesis: x = f . x reconsider fx = f . x as Subset of A by TARSKI:def_3; consider E1 being Equivalence_Relation of A such that A11: PA1 = Class E1 by EQREL_1:34; assume x <> f . x ; ::_thesis: contradiction then consider a being set such that A12: ( ( a in x & not a in f . x ) or ( a in f . x & not a in x ) ) by TARSKI:1; A13: fx c= A ; then A14: a in Class (E1,a) by A12, EQREL_1:20; reconsider CE1a = Class (E1,a) as Element of PA1 by A13, A12, A11, EQREL_1:def_3; reconsider fCE1a = f . CE1a as Subset of A by TARSKI:def_3; A15: x c= f . x by A4; CE1a c= f . CE1a by A4; then fx meets fCE1a by A15, A12, A14, XBOOLE_0:3; then fx = fCE1a by EQREL_1:def_4; hence contradiction by A5, A9, A15, A12, A14, FUNCT_1:def_4; ::_thesis: verum end; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_PA1_implies_x_in_PA2_)_&_(_x_in_PA2_implies_x_in_PA1_)_) let x be set ; ::_thesis: ( ( x in PA1 implies x in PA2 ) & ( x in PA2 implies x in PA1 ) ) hereby ::_thesis: ( x in PA2 implies x in PA1 ) assume x in PA1 ; ::_thesis: x in PA2 then reconsider x9 = x as Element of PA1 ; set fx = f . x9; f . x9 in PA2 ; hence x in PA2 by A10; ::_thesis: verum end; assume x in PA2 ; ::_thesis: x in PA1 then consider y being set such that A16: y in dom f and A17: x = f . y by A6, FUNCT_1:def_3; reconsider y9 = y as Element of PA1 by A16, FUNCT_2:def_1; y9 = f . y9 by A10; hence x in PA1 by A17; ::_thesis: verum end; hence PA1 = PA2 by TARSKI:1; ::_thesis: verum end; registration let D be set ; let M be FinSequence of D * ; let k be Nat; clusterM /. k -> Relation-like Function-like ; coherence ( M /. k is Function-like & M /. k is Relation-like ) ; end; registration let D be set ; let M be FinSequence of D * ; let k be Nat; clusterM /. k -> D -valued FinSequence-like for Function; coherence for b1 being Function st b1 = M /. k holds ( b1 is FinSequence-like & b1 is D -valued ) by FINSEQ_1:def_11; end;