:: 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;