:: FINTOPO6 semantic presentation
begin
registration
let FT be non empty RelStr ;
cluster empty -> connected for Element of K32( the carrier of FT);
coherence
for b1 being Subset of FT st b1 is empty holds
b1 is connected
proof
let S be Subset of FT; ::_thesis: ( S is empty implies S is connected )
assume A1: S is empty ; ::_thesis: S is connected
let B, C be Subset of FT; :: according to FIN_TOPO:def_16 ::_thesis: ( not S = B \/ C or B = {} or C = {} or not B misses C or not B ^b misses C )
assume that
A2: ( S = B \/ C & B <> {} ) and
C <> {} and
B misses C ; ::_thesis: not B ^b misses C
thus not B ^b misses C by A1, A2; ::_thesis: verum
end;
end;
theorem Th1: :: FINTOPO6:1
for FT being non empty RelStr
for A, B being Subset of FT holds (A \/ B) ^b = (A ^b) \/ (B ^b)
proof
let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT holds (A \/ B) ^b = (A ^b) \/ (B ^b)
let A, B be Subset of FT; ::_thesis: (A \/ B) ^b = (A ^b) \/ (B ^b)
A1: (A \/ B) ^b c= (A ^b) \/ (B ^b)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A \/ B) ^b or x in (A ^b) \/ (B ^b) )
assume x in (A \/ B) ^b ; ::_thesis: x in (A ^b) \/ (B ^b)
then consider y being Element of FT such that
A2: x = y and
A3: U_FT y meets A \/ B ;
( U_FT y meets A or U_FT y meets B ) by A3, XBOOLE_1:70;
then ( x in { u where u is Element of FT : U_FT u meets A } or x in B ^b ) by A2;
hence x in (A ^b) \/ (B ^b) by XBOOLE_0:def_3; ::_thesis: verum
end;
( A ^b c= (A \/ B) ^b & B ^b c= (A \/ B) ^b ) by FIN_TOPO:14, XBOOLE_1:7;
then (A ^b) \/ (B ^b) c= (A \/ B) ^b by XBOOLE_1:8;
hence (A \/ B) ^b = (A ^b) \/ (B ^b) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th2: :: FINTOPO6:2
for FT being non empty RelStr holds ({} FT) ^b = {}
proof
let FT be non empty RelStr ; ::_thesis: ({} FT) ^b = {}
assume not ({} FT) ^b = {} ; ::_thesis: contradiction
then consider x being set such that
A1: x in ({} FT) ^b by XBOOLE_0:def_1;
ex y being Element of FT st
( x = y & U_FT y meets {} FT ) by A1;
hence contradiction by XBOOLE_1:65; ::_thesis: verum
end;
registration
let FT be non empty RelStr ;
cluster({} FT) ^b -> empty ;
coherence
({} FT) ^b is empty by Th2;
end;
theorem Th3: :: FINTOPO6:3
for FT being non empty RelStr
for A being Subset of FT st ( for B, C being Subset of FT st A = B \/ C & B <> {} & C <> {} & B misses C holds
( B ^b meets C & B meets C ^b ) ) holds
A is connected
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st ( for B, C being Subset of FT st A = B \/ C & B <> {} & C <> {} & B misses C holds
( B ^b meets C & B meets C ^b ) ) holds
A is connected
let A be Subset of FT; ::_thesis: ( ( for B, C being Subset of FT st A = B \/ C & B <> {} & C <> {} & B misses C holds
( B ^b meets C & B meets C ^b ) ) implies A is connected )
assume for B, C being Subset of FT st A = B \/ C & B <> {} & C <> {} & B misses C holds
( B ^b meets C & B meets C ^b ) ; ::_thesis: A is connected
then for B, C being Subset of FT st A = B \/ C & B <> {} & C <> {} & B misses C holds
B ^b meets C ;
hence A is connected by FIN_TOPO:def_16; ::_thesis: verum
end;
definition
let FT be non empty RelStr ;
attrFT is connected means :Def1: :: FINTOPO6:def 1
[#] FT is connected ;
end;
:: deftheorem Def1 defines connected FINTOPO6:def_1_:_
for FT being non empty RelStr holds
( FT is connected iff [#] FT is connected );
theorem Th4: :: FINTOPO6:4
for FT being non empty RelStr
for A being Subset of FT st A is connected holds
for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds
B2 = {} FT
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st A is connected holds
for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds
B2 = {} FT
let A be Subset of FT; ::_thesis: ( A is connected implies for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds
B2 = {} FT )
assume A1: A is connected ; ::_thesis: for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds
B2 = {} FT
let A2, B2 be Subset of FT; ::_thesis: ( A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT implies B2 = {} FT )
assume that
A2: ( A = A2 \/ B2 & A2 misses B2 ) and
A3: A2,B2 are_separated ; ::_thesis: ( A2 = {} FT or B2 = {} FT )
A2 ^b misses B2 by A3, FINTOPO4:def_1;
hence ( A2 = {} FT or B2 = {} FT ) by A1, A2, FIN_TOPO:def_16; ::_thesis: verum
end;
theorem Th5: :: FINTOPO6:5
for FT being non empty RelStr st FT is connected holds
for A, B being Subset of FT st [#] FT = A \/ B & A misses B & A,B are_separated & not A = {} FT holds
B = {} FT
proof
let FT be non empty RelStr ; ::_thesis: ( FT is connected implies for A, B being Subset of FT st [#] FT = A \/ B & A misses B & A,B are_separated & not A = {} FT holds
B = {} FT )
assume FT is connected ; ::_thesis: for A, B being Subset of FT st [#] FT = A \/ B & A misses B & A,B are_separated & not A = {} FT holds
B = {} FT
then A1: [#] FT is connected by Def1;
let A, B be Subset of FT; ::_thesis: ( [#] FT = A \/ B & A misses B & A,B are_separated & not A = {} FT implies B = {} FT )
assume that
A2: ( [#] FT = A \/ B & A misses B ) and
A3: A,B are_separated ; ::_thesis: ( A = {} FT or B = {} FT )
A ^b misses B by A3, FINTOPO4:def_1;
hence ( A = {} FT or B = {} FT ) by A1, A2, FIN_TOPO:def_16; ::_thesis: verum
end;
theorem Th6: :: FINTOPO6:6
for FT being non empty RelStr
for A, B being Subset of FT st FT is symmetric & A ^b misses B holds
A misses B ^b
proof
let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT st FT is symmetric & A ^b misses B holds
A misses B ^b
let A, B be Subset of FT; ::_thesis: ( FT is symmetric & A ^b misses B implies A misses B ^b )
assume that
A1: FT is symmetric and
A2: A ^b misses B ; ::_thesis: A misses B ^b
assume A meets B ^b ; ::_thesis: contradiction
then consider x being set such that
A3: x in A and
A4: x in B ^b by XBOOLE_0:3;
consider y being Element of FT such that
A5: x = y and
A6: U_FT y meets B by A4;
consider z being set such that
A7: z in U_FT y and
A8: z in B by A6, XBOOLE_0:3;
reconsider z2 = z as Element of FT by A7;
y in U_FT z2 by A1, A7, FIN_TOPO:def_13;
then U_FT z2 meets A by A3, A5, XBOOLE_0:3;
then A9: z in A ^b ;
(A ^b) /\ B = {} by A2, XBOOLE_0:def_7;
hence contradiction by A8, A9, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th7: :: FINTOPO6:7
for FT being non empty RelStr
for A being Subset of FT st FT is symmetric & ( for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds
B2 = {} FT ) holds
A is connected
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st FT is symmetric & ( for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds
B2 = {} FT ) holds
A is connected
let A be Subset of FT; ::_thesis: ( FT is symmetric & ( for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds
B2 = {} FT ) implies A is connected )
assume A1: FT is symmetric ; ::_thesis: ( ex A2, B2 being Subset of FT st
( A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT & not B2 = {} FT ) or A is connected )
assume A2: for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds
B2 = {} FT ; ::_thesis: A is connected
for B, C being Subset of FT st A = B \/ C & B <> {} & C <> {} & B misses C holds
( B ^b meets C & B meets C ^b )
proof
let B, C be Subset of FT; ::_thesis: ( A = B \/ C & B <> {} & C <> {} & B misses C implies ( B ^b meets C & B meets C ^b ) )
assume ( A = B \/ C & B <> {} & C <> {} & B misses C ) ; ::_thesis: ( B ^b meets C & B meets C ^b )
then not B,C are_separated by A2;
then ( not B ^b misses C or not B misses C ^b ) by FINTOPO4:def_1;
hence ( B ^b meets C & B meets C ^b ) by A1, Th6; ::_thesis: verum
end;
hence A is connected by Th3; ::_thesis: verum
end;
definition
let T be RelStr ;
mode SubSpace of T -> RelStr means :Def2: :: FINTOPO6:def 2
( the carrier of it c= the carrier of T & ( for x being Element of it st x in the carrier of it holds
U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of it ) );
existence
ex b1 being RelStr st
( the carrier of b1 c= the carrier of T & ( for x being Element of b1 st x in the carrier of b1 holds
U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of b1 ) )
proof
for x being Element of T st x in the carrier of T holds
U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of T by XBOOLE_1:28;
hence ex b1 being RelStr st
( the carrier of b1 c= the carrier of T & ( for x being Element of b1 st x in the carrier of b1 holds
U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of b1 ) ) ; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines SubSpace FINTOPO6:def_2_:_
for T, b2 being RelStr holds
( b2 is SubSpace of T iff ( the carrier of b2 c= the carrier of T & ( for x being Element of b2 st x in the carrier of b2 holds
U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of b2 ) ) );
Lm1: for T being RelStr holds RelStr(# the carrier of T, the InternalRel of T #) is SubSpace of T
proof
let T be RelStr ; ::_thesis: RelStr(# the carrier of T, the InternalRel of T #) is SubSpace of T
set S = RelStr(# the carrier of T, the InternalRel of T #);
for x being Element of RelStr(# the carrier of T, the InternalRel of T #) st x in the carrier of RelStr(# the carrier of T, the InternalRel of T #) holds
U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of T by XBOOLE_1:28;
hence RelStr(# the carrier of T, the InternalRel of T #) is SubSpace of T by Def2; ::_thesis: verum
end;
registration
let T be RelStr ;
cluster strict for SubSpace of T;
existence
ex b1 being SubSpace of T st b1 is strict
proof
RelStr(# the carrier of T, the InternalRel of T #) is SubSpace of T by Lm1;
hence ex b1 being SubSpace of T st b1 is strict ; ::_thesis: verum
end;
end;
registration
let T be non empty RelStr ;
cluster non empty strict for SubSpace of T;
existence
ex b1 being SubSpace of T st
( b1 is strict & not b1 is empty )
proof
( RelStr(# the carrier of T, the InternalRel of T #) is SubSpace of T & not RelStr(# the carrier of T, the InternalRel of T #) is empty ) by Lm1;
hence ex b1 being SubSpace of T st
( b1 is strict & not b1 is empty ) ; ::_thesis: verum
end;
end;
definition
let T be non empty RelStr ;
let P be non empty Subset of T;
funcT | P -> non empty strict SubSpace of T means :Def3: :: FINTOPO6:def 3
[#] it = P;
existence
ex b1 being non empty strict SubSpace of T st [#] b1 = P
proof
deffunc H1( set ) -> Element of K32( the carrier of T) = (Im ( the InternalRel of T,$1)) /\ P;
A1: for x being Element of T st x in P holds
H1(x) c= P by XBOOLE_1:17;
consider G being Relation of P such that
A2: for y being Element of T st y in P holds
Im (G,y) = H1(y) from RELSET_1:sch_3(A1);
set FS = RelStr(# P,G #);
for x being Element of RelStr(# P,G #) st x in the carrier of RelStr(# P,G #) holds
U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of RelStr(# P,G #) by A2;
then ( [#] RelStr(# P,G #) = the carrier of RelStr(# P,G #) & RelStr(# P,G #) is non empty strict SubSpace of T ) by Def2;
hence ex b1 being non empty strict SubSpace of T st [#] b1 = P ; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty strict SubSpace of T st [#] b1 = P & [#] b2 = P holds
b1 = b2
proof
let Z1, Z2 be non empty strict SubSpace of T; ::_thesis: ( [#] Z1 = P & [#] Z2 = P implies Z1 = Z2 )
assume that
A3: [#] Z1 = P and
A4: [#] Z2 = P ; ::_thesis: Z1 = Z2
reconsider R1 = the InternalRel of Z1, R2 = the InternalRel of Z2 as Relation of P by A3, A4;
for z being set st z in P holds
Im (R1,z) = Im (R2,z)
proof
let z be set ; ::_thesis: ( z in P implies Im (R1,z) = Im (R2,z) )
assume A5: z in P ; ::_thesis: Im (R1,z) = Im (R2,z)
then reconsider z1 = z as Element of Z1 by A3;
reconsider z2 = z as Element of Z2 by A4, A5;
thus Im (R1,z) = U_FT z1
.= (Im ( the InternalRel of T,z1)) /\ the carrier of Z1 by Def2
.= U_FT z2 by A3, A4, Def2
.= Im (R2,z) ; ::_thesis: verum
end;
hence Z1 = Z2 by A3, A4, RELSET_1:31; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines | FINTOPO6:def_3_:_
for T being non empty RelStr
for P being non empty Subset of T
for b3 being non empty strict SubSpace of T holds
( b3 = T | P iff [#] b3 = P );
theorem Th8: :: FINTOPO6:8
for FT being non empty RelStr
for X being non empty SubSpace of FT st FT is filled holds
X is filled
proof
let FT be non empty RelStr ; ::_thesis: for X being non empty SubSpace of FT st FT is filled holds
X is filled
let X be non empty SubSpace of FT; ::_thesis: ( FT is filled implies X is filled )
assume A1: FT is filled ; ::_thesis: X is filled
let x be Element of X; :: according to FIN_TOPO:def_4 ::_thesis: x in U_FT x
the carrier of X c= the carrier of FT by Def2;
then reconsider x2 = x as Element of FT by TARSKI:def_3;
A2: U_FT x = (U_FT x2) /\ ([#] X) by Def2;
x2 in U_FT x2 by A1, FIN_TOPO:def_4;
hence x in U_FT x by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
registration
let FT be non empty filled RelStr ;
cluster non empty -> non empty filled for SubSpace of FT;
coherence
for b1 being non empty SubSpace of FT holds b1 is filled by Th8;
end;
theorem :: FINTOPO6:9
for FT being non empty RelStr
for X being non empty SubSpace of FT st FT is symmetric holds
X is symmetric
proof
let FT be non empty RelStr ; ::_thesis: for X being non empty SubSpace of FT st FT is symmetric holds
X is symmetric
let X be non empty SubSpace of FT; ::_thesis: ( FT is symmetric implies X is symmetric )
assume A1: FT is symmetric ; ::_thesis: X is symmetric
for x, y being Element of X st y in U_FT x holds
x in U_FT y
proof
let x, y be Element of X; ::_thesis: ( y in U_FT x implies x in U_FT y )
assume A2: y in U_FT x ; ::_thesis: x in U_FT y
the carrier of X c= the carrier of FT by Def2;
then reconsider x2 = x, y2 = y as Element of FT by TARSKI:def_3;
A3: ( U_FT x = (U_FT x2) /\ ([#] X) & U_FT y = (U_FT y2) /\ ([#] X) ) by Def2;
( y2 in U_FT x2 implies x2 in U_FT y2 ) by A1, FIN_TOPO:def_13;
hence x in U_FT y by A2, A3, XBOOLE_0:def_4; ::_thesis: verum
end;
hence X is symmetric by FIN_TOPO:def_13; ::_thesis: verum
end;
theorem Th10: :: FINTOPO6:10
for FT being non empty RelStr
for X9 being SubSpace of FT
for A being Subset of X9 holds A is Subset of FT
proof
let FT be non empty RelStr ; ::_thesis: for X9 being SubSpace of FT
for A being Subset of X9 holds A is Subset of FT
let X9 be SubSpace of FT; ::_thesis: for A being Subset of X9 holds A is Subset of FT
let A be Subset of X9; ::_thesis: A is Subset of FT
the carrier of X9 c= the carrier of FT by Def2;
hence A is Subset of FT by XBOOLE_1:1; ::_thesis: verum
end;
theorem :: FINTOPO6:11
for FT being non empty RelStr
for P being Subset of FT holds
( P is closed iff P ` is open )
proof
let FT be non empty RelStr ; ::_thesis: for P being Subset of FT holds
( P is closed iff P ` is open )
let P be Subset of FT; ::_thesis: ( P is closed iff P ` is open )
( P ` is open implies (P `) ` is closed ) by FIN_TOPO:23;
hence ( P is closed iff P ` is open ) by FIN_TOPO:24; ::_thesis: verum
end;
theorem :: FINTOPO6:12
for FT being non empty RelStr
for A being Subset of FT holds
( A is open iff ( ( for z being Element of FT st U_FT z c= A holds
z in A ) & ( for x being Element of FT st x in A holds
U_FT x c= A ) ) )
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds
( A is open iff ( ( for z being Element of FT st U_FT z c= A holds
z in A ) & ( for x being Element of FT st x in A holds
U_FT x c= A ) ) )
let A be Subset of FT; ::_thesis: ( A is open iff ( ( for z being Element of FT st U_FT z c= A holds
z in A ) & ( for x being Element of FT st x in A holds
U_FT x c= A ) ) )
hereby ::_thesis: ( ( for z being Element of FT st U_FT z c= A holds
z in A ) & ( for x being Element of FT st x in A holds
U_FT x c= A ) implies A is open )
assume A is open ; ::_thesis: ( ( for z being Element of FT st U_FT z c= A holds
z in A ) & ( for x being Element of FT st x in A holds
U_FT x c= A ) )
then A1: A = A ^i by FIN_TOPO:def_14;
hence for z being Element of FT st U_FT z c= A holds
z in A ; ::_thesis: for x being Element of FT st x in A holds
U_FT x c= A
for x being Element of FT st x in A holds
U_FT x c= A
proof
let x be Element of FT; ::_thesis: ( x in A implies U_FT x c= A )
assume x in A ; ::_thesis: U_FT x c= A
then ex y being Element of FT st
( x = y & U_FT y c= A ) by A1;
hence U_FT x c= A ; ::_thesis: verum
end;
hence for x being Element of FT st x in A holds
U_FT x c= A ; ::_thesis: verum
end;
assume that
A2: for z being Element of FT st U_FT z c= A holds
z in A and
A3: for x being Element of FT st x in A holds
U_FT x c= A ; ::_thesis: A is open
A4: A c= { y where y is Element of FT : U_FT y c= A }
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in A or u in { y where y is Element of FT : U_FT y c= A } )
assume A5: u in A ; ::_thesis: u in { y where y is Element of FT : U_FT y c= A }
then reconsider y2 = u as Element of FT ;
U_FT y2 c= A by A3, A5;
hence u in { y where y is Element of FT : U_FT y c= A } ; ::_thesis: verum
end;
{ y where y is Element of FT : U_FT y c= A } c= A
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { y where y is Element of FT : U_FT y c= A } or u in A )
assume u in { y where y is Element of FT : U_FT y c= A } ; ::_thesis: u in A
then ex y being Element of FT st
( y = u & U_FT y c= A ) ;
hence u in A by A2; ::_thesis: verum
end;
then A = A ^i by A4, XBOOLE_0:def_10;
hence A is open by FIN_TOPO:def_14; ::_thesis: verum
end;
theorem Th13: :: FINTOPO6:13
for FT being non empty RelStr
for X9 being non empty SubSpace of FT
for A being Subset of FT
for A1 being Subset of X9 st A = A1 holds
A1 ^b = (A ^b) /\ ([#] X9)
proof
let FT be non empty RelStr ; ::_thesis: for X9 being non empty SubSpace of FT
for A being Subset of FT
for A1 being Subset of X9 st A = A1 holds
A1 ^b = (A ^b) /\ ([#] X9)
let X9 be non empty SubSpace of FT; ::_thesis: for A being Subset of FT
for A1 being Subset of X9 st A = A1 holds
A1 ^b = (A ^b) /\ ([#] X9)
let A be Subset of FT; ::_thesis: for A1 being Subset of X9 st A = A1 holds
A1 ^b = (A ^b) /\ ([#] X9)
let A1 be Subset of X9; ::_thesis: ( A = A1 implies A1 ^b = (A ^b) /\ ([#] X9) )
assume A1: A = A1 ; ::_thesis: A1 ^b = (A ^b) /\ ([#] X9)
A2: (A ^b) /\ ([#] X9) c= A1 ^b
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in (A ^b) /\ ([#] X9) or u in A1 ^b )
assume A3: u in (A ^b) /\ ([#] X9) ; ::_thesis: u in A1 ^b
then u in A ^b by XBOOLE_0:def_4;
then consider y2 being Element of FT such that
A4: u = y2 and
A5: U_FT y2 meets A ;
reconsider y3 = y2 as Element of X9 by A3, A4;
consider z being set such that
A6: z in U_FT y2 and
A7: z in A by A5, XBOOLE_0:3;
U_FT y3 = (U_FT y2) /\ ([#] X9) by Def2;
then z in U_FT y3 by A1, A6, A7, XBOOLE_0:def_4;
then U_FT y3 meets A1 by A1, A7, XBOOLE_0:3;
hence u in A1 ^b by A4; ::_thesis: verum
end;
A1 ^b c= (A ^b) /\ ([#] X9)
proof
reconsider Y = X9 as non empty RelStr ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A1 ^b or x in (A ^b) /\ ([#] X9) )
assume x in A1 ^b ; ::_thesis: x in (A ^b) /\ ([#] X9)
then consider y being Element of Y such that
A8: y = x and
A9: U_FT y meets A1 ;
( y in the carrier of X9 & the carrier of Y c= the carrier of FT ) by Def2;
then reconsider z = y as Element of FT ;
U_FT y = (Im ( the InternalRel of FT,y)) /\ the carrier of X9 by Def2;
then U_FT z meets A by A1, A9, XBOOLE_1:74;
then z in { u where u is Element of FT : U_FT u meets A } ;
hence x in (A ^b) /\ ([#] X9) by A8, XBOOLE_0:def_4; ::_thesis: verum
end;
hence A1 ^b = (A ^b) /\ ([#] X9) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: FINTOPO6:14
for FT being non empty RelStr
for X9 being non empty SubSpace of FT
for P1, Q1 being Subset of FT
for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds
P1,Q1 are_separated
proof
let FT be non empty RelStr ; ::_thesis: for X9 being non empty SubSpace of FT
for P1, Q1 being Subset of FT
for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds
P1,Q1 are_separated
let X9 be non empty SubSpace of FT; ::_thesis: for P1, Q1 being Subset of FT
for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds
P1,Q1 are_separated
let P1, Q1 be Subset of FT; ::_thesis: for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds
P1,Q1 are_separated
let P, Q be Subset of X9; ::_thesis: ( P = P1 & Q = Q1 & P,Q are_separated implies P1,Q1 are_separated )
assume A1: ( P = P1 & Q = Q1 ) ; ::_thesis: ( not P,Q are_separated or P1,Q1 are_separated )
reconsider P2 = P, Q2 = Q as Subset of FT by Th10;
assume A2: P,Q are_separated ; ::_thesis: P1,Q1 are_separated
then P ^b misses Q by FINTOPO4:def_1;
then A3: (P ^b) /\ Q = {} by XBOOLE_0:def_7;
P misses Q ^b by A2, FINTOPO4:def_1;
then A4: P /\ (Q ^b) = {} by XBOOLE_0:def_7;
P /\ (Q ^b) = P /\ (([#] X9) /\ (Q2 ^b)) by Th13
.= (P /\ ([#] X9)) /\ (Q2 ^b) by XBOOLE_1:16
.= P2 /\ (Q2 ^b) by XBOOLE_1:28 ;
then A5: P2 misses Q2 ^b by A4, XBOOLE_0:def_7;
(P ^b) /\ Q = ((P2 ^b) /\ ([#] X9)) /\ Q by Th13
.= (P2 ^b) /\ (Q /\ ([#] X9)) by XBOOLE_1:16
.= (P2 ^b) /\ Q2 by XBOOLE_1:28 ;
then P2 ^b misses Q2 by A3, XBOOLE_0:def_7;
hence P1,Q1 are_separated by A1, A5, FINTOPO4:def_1; ::_thesis: verum
end;
theorem :: FINTOPO6:15
for FT being non empty RelStr
for X9 being non empty SubSpace of FT
for P, Q being Subset of FT
for P1, Q1 being Subset of X9 st P = P1 & Q = Q1 & P \/ Q c= [#] X9 & P,Q are_separated holds
P1,Q1 are_separated
proof
let FT be non empty RelStr ; ::_thesis: for X9 being non empty SubSpace of FT
for P, Q being Subset of FT
for P1, Q1 being Subset of X9 st P = P1 & Q = Q1 & P \/ Q c= [#] X9 & P,Q are_separated holds
P1,Q1 are_separated
let X9 be non empty SubSpace of FT; ::_thesis: for P, Q being Subset of FT
for P1, Q1 being Subset of X9 st P = P1 & Q = Q1 & P \/ Q c= [#] X9 & P,Q are_separated holds
P1,Q1 are_separated
let P, Q be Subset of FT; ::_thesis: for P1, Q1 being Subset of X9 st P = P1 & Q = Q1 & P \/ Q c= [#] X9 & P,Q are_separated holds
P1,Q1 are_separated
let P1, Q1 be Subset of X9; ::_thesis: ( P = P1 & Q = Q1 & P \/ Q c= [#] X9 & P,Q are_separated implies P1,Q1 are_separated )
assume that
A1: ( P = P1 & Q = Q1 ) and
A2: P \/ Q c= [#] X9 ; ::_thesis: ( not P,Q are_separated or P1,Q1 are_separated )
( P c= P \/ Q & Q c= P \/ Q ) by XBOOLE_1:7;
then reconsider P2 = P, Q2 = Q as Subset of X9 by A2, XBOOLE_1:1;
assume A3: P,Q are_separated ; ::_thesis: P1,Q1 are_separated
then P misses Q ^b by FINTOPO4:def_1;
then A4: P /\ (Q ^b) = {} by XBOOLE_0:def_7;
P2 /\ (Q2 ^b) = P2 /\ (([#] X9) /\ (Q ^b)) by Th13
.= (P2 /\ ([#] X9)) /\ (Q ^b) by XBOOLE_1:16
.= P /\ (Q ^b) by XBOOLE_1:28 ;
then A5: P2 misses Q2 ^b by A4, XBOOLE_0:def_7;
P2 ^b = (P ^b) /\ ([#] X9) by Th13;
then A6: (P2 ^b) /\ Q2 = (P ^b) /\ (Q2 /\ ([#] X9)) by XBOOLE_1:16
.= (P ^b) /\ Q by XBOOLE_1:28 ;
P ^b misses Q by A3, FINTOPO4:def_1;
then (P ^b) /\ Q = {} by XBOOLE_0:def_7;
then P2 ^b misses Q2 by A6, XBOOLE_0:def_7;
hence P1,Q1 are_separated by A1, A5, FINTOPO4:def_1; ::_thesis: verum
end;
theorem Th16: :: FINTOPO6:16
for FT being non empty RelStr
for A being non empty Subset of FT holds
( A is connected iff FT | A is connected )
proof
let FT be non empty RelStr ; ::_thesis: for A being non empty Subset of FT holds
( A is connected iff FT | A is connected )
let A be non empty Subset of FT; ::_thesis: ( A is connected iff FT | A is connected )
A1: [#] (FT | A) = A by Def3;
thus ( A is connected implies FT | A is connected ) ::_thesis: ( FT | A is connected implies A is connected )
proof
assume A2: A is connected ; ::_thesis: FT | A is connected
for B2, C2 being Subset of (FT | A) st [#] (FT | A) = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2 holds
B2 ^b meets C2
proof
let B2, C2 be Subset of (FT | A); ::_thesis: ( [#] (FT | A) = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2 implies B2 ^b meets C2 )
A3: ([#] (FT | A)) /\ C2 = C2 by XBOOLE_1:28;
the carrier of (FT | A) = [#] (FT | A)
.= A by Def3 ;
then reconsider B3 = B2, C3 = C2 as Subset of FT by XBOOLE_1:1;
assume ( [#] (FT | A) = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2 ) ; ::_thesis: B2 ^b meets C2
then A4: B3 ^b meets C3 by A1, A2, FIN_TOPO:def_16;
(B2 ^b) /\ C2 = ((B3 ^b) /\ ([#] (FT | A))) /\ C2 by Th13
.= (B3 ^b) /\ C3 by A3, XBOOLE_1:16 ;
then (B2 ^b) /\ C2 <> {} by A4, XBOOLE_0:def_7;
hence B2 ^b meets C2 by XBOOLE_0:def_7; ::_thesis: verum
end;
then [#] (FT | A) is connected by FIN_TOPO:def_16;
hence FT | A is connected by Def1; ::_thesis: verum
end;
assume FT | A is connected ; ::_thesis: A is connected
then A5: [#] (FT | A) is connected by Def1;
let B, C be Subset of FT; :: according to FIN_TOPO:def_16 ::_thesis: ( not A = B \/ C or B = {} or C = {} or not B misses C or not B ^b misses C )
assume that
A6: A = B \/ C and
A7: ( B <> {} & C <> {} & B misses C ) ; ::_thesis: not B ^b misses C
A8: [#] (FT | A) = A by Def3;
then reconsider B2 = B as Subset of (FT | A) by A6, XBOOLE_1:7;
reconsider C2 = C as Subset of (FT | A) by A6, A8, XBOOLE_1:7;
( ([#] (FT | A)) /\ C2 = C2 & B2 ^b = (B ^b) /\ ([#] (FT | A)) ) by Th13, XBOOLE_1:28;
then A9: (B ^b) /\ C = (B2 ^b) /\ C2 by XBOOLE_1:16;
B2 ^b meets C2 by A5, A6, A7, A8, FIN_TOPO:def_16;
hence (B ^b) /\ C <> {} by A9, XBOOLE_0:def_7; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
theorem :: FINTOPO6:17
for FT being non empty filled RelStr
for A being non empty Subset of FT st FT is symmetric holds
( A is connected iff for P, Q being Subset of FT st A = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT holds
Q = {} FT )
proof
let FT be non empty filled RelStr ; ::_thesis: for A being non empty Subset of FT st FT is symmetric holds
( A is connected iff for P, Q being Subset of FT st A = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT holds
Q = {} FT )
let A be non empty Subset of FT; ::_thesis: ( FT is symmetric implies ( A is connected iff for P, Q being Subset of FT st A = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT holds
Q = {} FT ) )
assume A1: FT is symmetric ; ::_thesis: ( A is connected iff for P, Q being Subset of FT st A = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT holds
Q = {} FT )
now__::_thesis:_(_not_A_is_connected_implies_ex_P1,_Q1_being_Subset_of_FT_st_
(_A_=_P1_\/_Q1_&_P1_misses_Q1_&_P1,Q1_are_separated_&_P1_<>_{}_FT_&_Q1_<>_{}_FT_)_)
assume not A is connected ; ::_thesis: ex P1, Q1 being Subset of FT st
( A = P1 \/ Q1 & P1 misses Q1 & P1,Q1 are_separated & P1 <> {} FT & Q1 <> {} FT )
then not FT | A is connected by Th16;
then not [#] (FT | A) is connected by Def1;
then consider P, Q being Subset of (FT | A) such that
A2: [#] (FT | A) = P \/ Q and
A3: ( P <> {} & Q <> {} ) and
A4: P misses Q and
A5: P ^b misses Q by FIN_TOPO:def_16;
reconsider P1 = P, Q1 = Q as Subset of FT by Th10;
take P1 = P1; ::_thesis: ex Q1 being Subset of FT st
( A = P1 \/ Q1 & P1 misses Q1 & P1,Q1 are_separated & P1 <> {} FT & Q1 <> {} FT )
take Q1 = Q1; ::_thesis: ( A = P1 \/ Q1 & P1 misses Q1 & P1,Q1 are_separated & P1 <> {} FT & Q1 <> {} FT )
thus ( A = P1 \/ Q1 & P1 misses Q1 ) by A2, A4, Def3; ::_thesis: ( P1,Q1 are_separated & P1 <> {} FT & Q1 <> {} FT )
A6: P ^b = (P1 ^b) /\ ([#] (FT | A)) by Th13;
([#] (FT | A)) /\ Q1 = Q1 by XBOOLE_1:28;
then (P1 ^b) /\ Q1 = ((P1 ^b) /\ ([#] (FT | A))) /\ Q by XBOOLE_1:16
.= {} by A5, A6, XBOOLE_0:def_7 ;
then P1 ^b misses Q1 by XBOOLE_0:def_7;
hence ( P1,Q1 are_separated & P1 <> {} FT & Q1 <> {} FT ) by A1, A3, FINTOPO4:10; ::_thesis: verum
end;
hence ( A is connected iff for P, Q being Subset of FT st A = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT holds
Q = {} FT ) by Th4; ::_thesis: verum
end;
theorem :: FINTOPO6:18
for FT being non empty RelStr
for A being Subset of FT st FT is filled & FT is connected & A <> {} & A ` <> {} holds
A ^delta <> {}
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st FT is filled & FT is connected & A <> {} & A ` <> {} holds
A ^delta <> {}
let A be Subset of FT; ::_thesis: ( FT is filled & FT is connected & A <> {} & A ` <> {} implies A ^delta <> {} )
assume that
A1: ( FT is filled & FT is connected ) and
A2: ( A <> {} & A ` <> {} ) ; ::_thesis: A ^delta <> {}
A3: now__::_thesis:_(_A_^b_meets_A_`_implies_ex_z_being_Element_of_FT_st_
(_U_FT_z_meets_A_&_U_FT_z_meets_A_`_)_)
assume A ^b meets A ` ; ::_thesis: ex z being Element of FT st
( U_FT z meets A & U_FT z meets A ` )
then consider x being set such that
A4: x in A ^b and
A5: x in A ` by XBOOLE_0:3;
reconsider x = x as Element of FT by A4;
x in U_FT x by A1, FIN_TOPO:def_4;
then A6: U_FT x meets A ` by A5, XBOOLE_0:3;
U_FT x meets A by A4, FIN_TOPO:8;
hence ex z being Element of FT st
( U_FT z meets A & U_FT z meets A ` ) by A6; ::_thesis: verum
end;
A7: now__::_thesis:_(_A_meets_(A_`)_^b_implies_ex_z_being_Element_of_FT_st_
(_U_FT_z_meets_A_&_U_FT_z_meets_A_`_)_)
assume A meets (A `) ^b ; ::_thesis: ex z being Element of FT st
( U_FT z meets A & U_FT z meets A ` )
then consider x being set such that
A8: x in (A `) ^b and
A9: x in A by XBOOLE_0:3;
reconsider x = x as Element of FT by A8;
x in U_FT x by A1, FIN_TOPO:def_4;
then A10: U_FT x meets A by A9, XBOOLE_0:3;
U_FT x meets A ` by A8, FIN_TOPO:8;
hence ex z being Element of FT st
( U_FT z meets A & U_FT z meets A ` ) by A10; ::_thesis: verum
end;
( {} = {} FT & A \/ (A `) = [#] FT ) by XBOOLE_1:45;
then not A,A ` are_separated by A1, A2, Th5, XBOOLE_1:79;
hence A ^delta <> {} by A3, A7, FINTOPO4:def_1, FIN_TOPO:5; ::_thesis: verum
end;
theorem :: FINTOPO6:19
for FT being non empty RelStr
for A being Subset of FT st FT is filled & FT is symmetric & FT is connected & A <> {} & A ` <> {} holds
A ^deltai <> {}
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st FT is filled & FT is symmetric & FT is connected & A <> {} & A ` <> {} holds
A ^deltai <> {}
let A be Subset of FT; ::_thesis: ( FT is filled & FT is symmetric & FT is connected & A <> {} & A ` <> {} implies A ^deltai <> {} )
assume that
A1: ( FT is filled & FT is symmetric ) and
A2: ( FT is connected & A <> {} & A ` <> {} ) ; ::_thesis: A ^deltai <> {}
A3: now__::_thesis:_(_A_^b_meets_A_`_implies_A_^deltai_<>_{}_)
assume A ^b meets A ` ; ::_thesis: A ^deltai <> {}
then consider x being set such that
A4: x in A ^b and
A5: x in A ` by XBOOLE_0:3;
reconsider x = x as Element of FT by A4;
U_FT x meets A by A4, FIN_TOPO:8;
then consider y being set such that
A6: y in U_FT x and
A7: y in A by XBOOLE_0:3;
reconsider y = y as Element of FT by A6;
y in U_FT y by A1, FIN_TOPO:def_4;
then A8: U_FT y meets A by A7, XBOOLE_0:3;
x in U_FT y by A1, A6, FIN_TOPO:def_13;
then U_FT y meets A ` by A5, XBOOLE_0:3;
then y in A ^delta by A8;
hence A ^deltai <> {} by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
A9: now__::_thesis:_(_A_meets_(A_`)_^b_implies_A_^deltai_<>_{}_)
assume A meets (A `) ^b ; ::_thesis: A ^deltai <> {}
then consider x being set such that
A10: x in (A `) ^b and
A11: x in A by XBOOLE_0:3;
reconsider x = x as Element of FT by A10;
x in U_FT x by A1, FIN_TOPO:def_4;
then A12: U_FT x meets A by A11, XBOOLE_0:3;
U_FT x meets A ` by A10, FIN_TOPO:8;
then x in A ^delta by A12;
hence A ^deltai <> {} by A11, XBOOLE_0:def_4; ::_thesis: verum
end;
( {} = {} FT & A \/ (A `) = [#] FT ) by XBOOLE_1:45;
then not A,A ` are_separated by A2, Th5, XBOOLE_1:79;
hence A ^deltai <> {} by A3, A9, FINTOPO4:def_1; ::_thesis: verum
end;
theorem :: FINTOPO6:20
for FT being non empty RelStr
for A being Subset of FT st FT is filled & FT is symmetric & FT is connected & A <> {} & A ` <> {} holds
A ^deltao <> {}
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st FT is filled & FT is symmetric & FT is connected & A <> {} & A ` <> {} holds
A ^deltao <> {}
let A be Subset of FT; ::_thesis: ( FT is filled & FT is symmetric & FT is connected & A <> {} & A ` <> {} implies A ^deltao <> {} )
assume that
A1: ( FT is filled & FT is symmetric ) and
A2: ( FT is connected & A <> {} & A ` <> {} ) ; ::_thesis: A ^deltao <> {}
A3: now__::_thesis:_(_A_meets_(A_`)_^b_implies_A_^deltao_<>_{}_)
assume A meets (A `) ^b ; ::_thesis: A ^deltao <> {}
then consider x being set such that
A4: x in (A `) ^b and
A5: x in A by XBOOLE_0:3;
reconsider x = x as Element of FT by A4;
U_FT x meets A ` by A4, FIN_TOPO:8;
then consider y being set such that
A6: y in U_FT x and
A7: y in A ` by XBOOLE_0:3;
reconsider y = y as Element of FT by A6;
y in U_FT y by A1, FIN_TOPO:def_4;
then A8: U_FT y meets A ` by A7, XBOOLE_0:3;
x in U_FT y by A1, A6, FIN_TOPO:def_13;
then U_FT y meets A by A5, XBOOLE_0:3;
then y in A ^delta by A8;
hence A ^deltao <> {} by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
A9: now__::_thesis:_(_A_^b_meets_A_`_implies_A_^deltao_<>_{}_)
assume A ^b meets A ` ; ::_thesis: A ^deltao <> {}
then consider x being set such that
A10: x in A ^b and
A11: x in A ` by XBOOLE_0:3;
reconsider x = x as Element of FT by A10;
x in U_FT x by A1, FIN_TOPO:def_4;
then A12: U_FT x meets A ` by A11, XBOOLE_0:3;
U_FT x meets A by A10, FIN_TOPO:8;
then x in A ^delta by A12;
hence A ^deltao <> {} by A11, XBOOLE_0:def_4; ::_thesis: verum
end;
( {} = {} FT & A \/ (A `) = [#] FT ) by XBOOLE_1:45;
then not A,A ` are_separated by A2, Th5, XBOOLE_1:79;
hence A ^deltao <> {} by A9, A3, FINTOPO4:def_1; ::_thesis: verum
end;
theorem :: FINTOPO6:21
for FT being non empty RelStr
for A being Subset of FT holds A ^deltai misses A ^deltao
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds A ^deltai misses A ^deltao
let A be Subset of FT; ::_thesis: A ^deltai misses A ^deltao
A misses A ` by XBOOLE_1:79;
then A1: A /\ (A `) = {} by XBOOLE_0:def_7;
thus (A ^deltai) /\ (A ^deltao) = (A /\ ((A ^delta) /\ (A `))) /\ (A ^delta) by XBOOLE_1:16
.= ((A /\ (A `)) /\ (A ^delta)) /\ (A ^delta) by XBOOLE_1:16
.= {} by A1 ; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
theorem :: FINTOPO6:22
for FT being non empty filled RelStr
for A being Subset of FT holds A ^deltao = (A ^b) \ A
proof
let FT be non empty filled RelStr ; ::_thesis: for A being Subset of FT holds A ^deltao = (A ^b) \ A
let A be Subset of FT; ::_thesis: A ^deltao = (A ^b) \ A
A1: (A `) /\ ((A `) ^b) = A ` by FIN_TOPO:13, XBOOLE_1:28;
thus A ^deltao = (A `) /\ ((A ^b) /\ ((A `) ^b)) by FIN_TOPO:18
.= (A ^b) /\ ((A `) /\ ((A `) ^b)) by XBOOLE_1:16
.= (A ^b) \ A by A1, SUBSET_1:13 ; ::_thesis: verum
end;
theorem :: FINTOPO6:23
for FT being non empty RelStr
for A, B being Subset of FT st A,B are_separated holds
A ^deltao misses B
proof
let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT st A,B are_separated holds
A ^deltao misses B
let A, B be Subset of FT; ::_thesis: ( A,B are_separated implies A ^deltao misses B )
assume A,B are_separated ; ::_thesis: A ^deltao misses B
then A1: A ^b misses B by FINTOPO4:def_1;
thus (A ^deltao) /\ B = (A `) /\ ((A ^delta) /\ B) by XBOOLE_1:16
.= (A `) /\ (((A ^b) /\ ((A `) ^b)) /\ B) by FIN_TOPO:18
.= (A `) /\ (((A `) ^b) /\ ((A ^b) /\ B)) by XBOOLE_1:16
.= (A `) /\ (((A `) ^b) /\ {}) by A1, XBOOLE_0:def_7
.= {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
theorem :: FINTOPO6:24
for FT being non empty RelStr
for A, B being Subset of FT st FT is filled & A misses B & A ^deltao misses B & B ^deltao misses A holds
A,B are_separated
proof
let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT st FT is filled & A misses B & A ^deltao misses B & B ^deltao misses A holds
A,B are_separated
let A, B be Subset of FT; ::_thesis: ( FT is filled & A misses B & A ^deltao misses B & B ^deltao misses A implies A,B are_separated )
assume that
A1: FT is filled and
A2: A /\ B = {} and
A3: (A ^deltao) /\ B = {} and
A4: (B ^deltao) /\ A = {} ; :: according to XBOOLE_0:def_7 ::_thesis: A,B are_separated
(B `) /\ ((B ^delta) /\ A) = {} by A4, XBOOLE_1:16;
then (B `) /\ (((B ^b) /\ ((B `) ^b)) /\ A) = {} by FIN_TOPO:18;
then (B `) /\ (((B `) ^b) /\ ((B ^b) /\ A)) = {} by XBOOLE_1:16;
then A5: ((B `) /\ ((B `) ^b)) /\ ((B ^b) /\ A) = {} by XBOOLE_1:16;
(B `) /\ ((B `) ^b) = B ` by A1, FIN_TOPO:13, XBOOLE_1:28;
then B ` misses (B ^b) /\ A by A5, XBOOLE_0:def_7;
then (B ^b) /\ A c= B by SUBSET_1:24;
then ((B ^b) /\ A) /\ A c= B /\ A by XBOOLE_1:26;
then (B ^b) /\ (A /\ A) c= B /\ A by XBOOLE_1:16;
then (B ^b) /\ A = {} by A2, XBOOLE_1:3;
then A6: A misses B ^b by XBOOLE_0:def_7;
(A `) /\ ((A ^delta) /\ B) = {} by A3, XBOOLE_1:16;
then (A `) /\ (((A ^b) /\ ((A `) ^b)) /\ B) = {} by FIN_TOPO:18;
then (A `) /\ (((A `) ^b) /\ ((A ^b) /\ B)) = {} by XBOOLE_1:16;
then A7: ((A `) /\ ((A `) ^b)) /\ ((A ^b) /\ B) = {} by XBOOLE_1:16;
(A `) /\ ((A `) ^b) = A ` by A1, FIN_TOPO:13, XBOOLE_1:28;
then A ` misses (A ^b) /\ B by A7, XBOOLE_0:def_7;
then (A ^b) /\ B c= A by SUBSET_1:24;
then ((A ^b) /\ B) /\ B c= A /\ B by XBOOLE_1:26;
then (A ^b) /\ (B /\ B) c= A /\ B by XBOOLE_1:16;
then (A ^b) /\ B = {} by A2, XBOOLE_1:3;
then A ^b misses B by XBOOLE_0:def_7;
hence A,B are_separated by A6, FINTOPO4:def_1; ::_thesis: verum
end;
theorem Th25: :: FINTOPO6:25
for FT being non empty RelStr
for x being Point of FT holds {x} is connected
proof
let FT be non empty RelStr ; ::_thesis: for x being Point of FT holds {x} is connected
let x be Point of FT; ::_thesis: {x} is connected
assume not {x} is connected ; ::_thesis: contradiction
then consider P, Q being Subset of FT such that
A1: {x} = P \/ Q and
A2: P <> {} and
A3: Q <> {} and
A4: P misses Q and
( not P ^b meets Q or not P meets Q ^b ) by Th3;
P <> Q
proof
assume not P <> Q ; ::_thesis: contradiction
then P /\ Q = P ;
hence contradiction by A2, A4, XBOOLE_0:def_7; ::_thesis: verum
end;
hence contradiction by A1, A2, A3, ZFMISC_1:38; ::_thesis: verum
end;
registration
let FT be non empty RelStr ;
let x be Point of FT;
cluster{x} -> connected for Subset of FT;
coherence
for b1 being Subset of FT st b1 = {x} holds
b1 is connected by Th25;
end;
definition
let FT be non empty RelStr ;
let A be Subset of FT;
predA is_a_component_of FT means :Def4: :: FINTOPO6:def 4
( A is connected & ( for B being Subset of FT st B is connected & A c= B holds
A = B ) );
end;
:: deftheorem Def4 defines is_a_component_of FINTOPO6:def_4_:_
for FT being non empty RelStr
for A being Subset of FT holds
( A is_a_component_of FT iff ( A is connected & ( for B being Subset of FT st B is connected & A c= B holds
A = B ) ) );
theorem :: FINTOPO6:26
for FT being non empty RelStr
for A being Subset of FT st A is_a_component_of FT holds
A <> {} FT
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st A is_a_component_of FT holds
A <> {} FT
let A be Subset of FT; ::_thesis: ( A is_a_component_of FT implies A <> {} FT )
set x = the Point of FT;
{} c= { the Point of FT} by XBOOLE_1:2;
hence ( A is_a_component_of FT implies A <> {} FT ) by Def4; ::_thesis: verum
end;
theorem Th27: :: FINTOPO6:27
for FT being non empty RelStr
for A, B being Subset of FT st A is closed & B is closed & A misses B holds
A,B are_separated
proof
let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT st A is closed & B is closed & A misses B holds
A,B are_separated
let A, B be Subset of FT; ::_thesis: ( A is closed & B is closed & A misses B implies A,B are_separated )
assume that
A1: A is closed and
A2: B is closed and
A3: A misses B ; ::_thesis: A,B are_separated
A4: A /\ B = {} by A3, XBOOLE_0:def_7;
then A /\ (B ^b) = {} by A2, FIN_TOPO:def_15;
then A5: A misses B ^b by XBOOLE_0:def_7;
(A ^b) /\ B = {} by A1, A4, FIN_TOPO:def_15;
then A ^b misses B by XBOOLE_0:def_7;
hence A,B are_separated by A5, FINTOPO4:def_1; ::_thesis: verum
end;
theorem Th28: :: FINTOPO6:28
for FT being non empty RelStr
for A, B being Subset of FT st FT is filled & [#] FT = A \/ B & A,B are_separated holds
( A is open & A is closed )
proof
let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT st FT is filled & [#] FT = A \/ B & A,B are_separated holds
( A is open & A is closed )
let A, B be Subset of FT; ::_thesis: ( FT is filled & [#] FT = A \/ B & A,B are_separated implies ( A is open & A is closed ) )
assume that
A1: FT is filled and
A2: [#] FT = A \/ B and
A3: A,B are_separated ; ::_thesis: ( A is open & A is closed )
A4: B c= B ^b by A1, FIN_TOPO:13;
now__::_thesis:_(_A_misses_B_^b_implies_B_^b_=_B_)
assume A misses B ^b ; ::_thesis: B ^b = B
then B ^b c= B by A2, XBOOLE_1:73;
hence B ^b = B by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
then A5: B is closed by A3, FINTOPO4:def_1, FIN_TOPO:def_15;
A6: A c= A ^b by A1, FIN_TOPO:13;
A7: now__::_thesis:_(_A_^b_misses_B_implies_A_^b_=_A_)
assume A ^b misses B ; ::_thesis: A ^b = A
then A ^b c= A by A2, XBOOLE_1:73;
hence A ^b = A by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
B ` = A by A1, A2, A3, FINTOPO4:6, PRE_TOPC:5;
hence ( A is open & A is closed ) by A3, A7, A5, FINTOPO4:def_1, FIN_TOPO:24, FIN_TOPO:def_15; ::_thesis: verum
end;
theorem Th29: :: FINTOPO6:29
for FT being non empty RelStr
for A, B, A1, B1 being Subset of FT st A,B are_separated & A1 c= A & B1 c= B holds
A1,B1 are_separated
proof
let FT be non empty RelStr ; ::_thesis: for A, B, A1, B1 being Subset of FT st A,B are_separated & A1 c= A & B1 c= B holds
A1,B1 are_separated
let A, B, A1, B1 be Subset of FT; ::_thesis: ( A,B are_separated & A1 c= A & B1 c= B implies A1,B1 are_separated )
assume that
A1: A,B are_separated and
A2: A1 c= A and
A3: B1 c= B ; ::_thesis: A1,B1 are_separated
A misses B ^b by A1, FINTOPO4:def_1;
then A4: A /\ (B ^b) = {} by XBOOLE_0:def_7;
B1 ^b c= B ^b by A3, FIN_TOPO:14;
then A1 /\ (B1 ^b) = {} FT by A2, A4, XBOOLE_1:3, XBOOLE_1:27;
then A5: A1 misses B1 ^b by XBOOLE_0:def_7;
A ^b misses B by A1, FINTOPO4:def_1;
then A6: (A ^b) /\ B = {} by XBOOLE_0:def_7;
A1 ^b c= A ^b by A2, FIN_TOPO:14;
then (A1 ^b) /\ B1 = {} FT by A3, A6, XBOOLE_1:3, XBOOLE_1:27;
then A1 ^b misses B1 by XBOOLE_0:def_7;
hence A1,B1 are_separated by A5, FINTOPO4:def_1; ::_thesis: verum
end;
theorem Th30: :: FINTOPO6:30
for FT being non empty RelStr
for A, B, C being Subset of FT st A,B are_separated & A,C are_separated holds
A,B \/ C are_separated
proof
let FT be non empty RelStr ; ::_thesis: for A, B, C being Subset of FT st A,B are_separated & A,C are_separated holds
A,B \/ C are_separated
let A, B, C be Subset of FT; ::_thesis: ( A,B are_separated & A,C are_separated implies A,B \/ C are_separated )
assume that
A1: A,B are_separated and
A2: A,C are_separated ; ::_thesis: A,B \/ C are_separated
A3: A ^b misses C by A2, FINTOPO4:def_1;
A ^b misses B by A1, FINTOPO4:def_1;
then A4: (A ^b) /\ B = {} by XBOOLE_0:def_7;
(A ^b) /\ (B \/ C) = ((A ^b) /\ B) \/ ((A ^b) /\ C) by XBOOLE_1:23
.= {} by A3, A4, XBOOLE_0:def_7 ;
then A5: A ^b misses B \/ C by XBOOLE_0:def_7;
A misses B ^b by A1, FINTOPO4:def_1;
then A6: A /\ (B ^b) = {} by XBOOLE_0:def_7;
A7: A misses C ^b by A2, FINTOPO4:def_1;
A /\ ((B \/ C) ^b) = A /\ ((B ^b) \/ (C ^b)) by Th1
.= (A /\ (B ^b)) \/ (A /\ (C ^b)) by XBOOLE_1:23
.= {} by A7, A6, XBOOLE_0:def_7 ;
then A misses (B \/ C) ^b by XBOOLE_0:def_7;
hence A,B \/ C are_separated by A5, FINTOPO4:def_1; ::_thesis: verum
end;
theorem :: FINTOPO6:31
for FT being non empty RelStr st FT is filled & FT is symmetric & ( for A, B being Subset of FT st [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed holds
A meets B ) holds
FT is connected
proof
let FT be non empty RelStr ; ::_thesis: ( FT is filled & FT is symmetric & ( for A, B being Subset of FT st [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed holds
A meets B ) implies FT is connected )
assume A1: ( FT is filled & FT is symmetric ) ; ::_thesis: ( ex A, B being Subset of FT st
( [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed & not A meets B ) or FT is connected )
assume A2: for A, B being Subset of FT st [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed holds
A meets B ; ::_thesis: FT is connected
assume not FT is connected ; ::_thesis: contradiction
then not [#] FT is connected by Def1;
then consider P, Q being Subset of FT such that
A3: [#] FT = P \/ Q and
A4: P misses Q and
A5: P,Q are_separated and
A6: ( P <> {} FT & Q <> {} FT ) by A1, Th7;
( P is closed & Q is closed ) by A1, A3, A5, Th28;
hence contradiction by A2, A3, A4, A6; ::_thesis: verum
end;
theorem :: FINTOPO6:32
for FT being non empty RelStr st FT is connected holds
for A, B being Subset of FT st [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed holds
A meets B
proof
let FT be non empty RelStr ; ::_thesis: ( FT is connected implies for A, B being Subset of FT st [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed holds
A meets B )
assume A1: [#] FT is connected ; :: according to FINTOPO6:def_1 ::_thesis: for A, B being Subset of FT st [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed holds
A meets B
given A, B being Subset of FT such that A2: ( [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed & A misses B ) ; ::_thesis: contradiction
thus contradiction by A1, A2, Th4, Th27; ::_thesis: verum
end;
theorem Th33: :: FINTOPO6:33
for FT being non empty RelStr
for A, B, C being Subset of FT st FT is filled & A is connected & A c= B \/ C & B,C are_separated & not A c= B holds
A c= C
proof
let FT be non empty RelStr ; ::_thesis: for A, B, C being Subset of FT st FT is filled & A is connected & A c= B \/ C & B,C are_separated & not A c= B holds
A c= C
let A, B, C be Subset of FT; ::_thesis: ( FT is filled & A is connected & A c= B \/ C & B,C are_separated & not A c= B implies A c= C )
assume that
A1: FT is filled and
A2: A is connected and
A3: A c= B \/ C and
A4: B,C are_separated ; ::_thesis: ( A c= B or A c= C )
A5: (A /\ B) \/ (A /\ C) = A /\ (B \/ C) by XBOOLE_1:23
.= A by A3, XBOOLE_1:28 ;
assume that
A6: not A c= B and
A7: not A c= C ; ::_thesis: contradiction
A meets B by A3, A7, XBOOLE_1:73;
then A8: A /\ B <> {} by XBOOLE_0:def_7;
A meets C by A3, A6, XBOOLE_1:73;
then A9: A /\ C <> {} by XBOOLE_0:def_7;
A10: ( A /\ B c= B & A /\ C c= C ) by XBOOLE_1:17;
then ( {} FT = {} & A /\ B misses A /\ C ) by A1, A4, Th29, FINTOPO4:6;
hence contradiction by A2, A4, A8, A9, A10, A5, Th4, Th29; ::_thesis: verum
end;
theorem Th34: :: FINTOPO6:34
for FT being non empty RelStr
for A, B being Subset of FT st FT is symmetric & A is connected & B is connected & not A,B are_separated holds
A \/ B is connected
proof
let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT st FT is symmetric & A is connected & B is connected & not A,B are_separated holds
A \/ B is connected
let A, B be Subset of FT; ::_thesis: ( FT is symmetric & A is connected & B is connected & not A,B are_separated implies A \/ B is connected )
assume that
A1: FT is symmetric and
A2: A is connected and
A3: B is connected and
A4: not A,B are_separated ; ::_thesis: A \/ B is connected
given P, Q being Subset of FT such that A5: A \/ B = P \/ Q and
A6: P <> {} and
A7: Q <> {} and
A8: P misses Q and
A9: P ^b misses Q ; :: according to FIN_TOPO:def_16 ::_thesis: contradiction
set P2 = A /\ P;
set Q2 = A /\ Q;
A10: A /\ P misses A /\ Q by A8, XBOOLE_1:76;
A11: Q ^b misses P by A1, A9, Th6;
A12: now__::_thesis:_(_A_c=_Q_implies_not_B_c=_P_)
assume that
A13: A c= Q and
A14: B c= P ; ::_thesis: contradiction
percases ( A ^b meets B or A meets B ^b ) by A4, FINTOPO4:def_1;
suppose A ^b meets B ; ::_thesis: contradiction
then Q ^b meets B by A13, FIN_TOPO:14, XBOOLE_1:63;
hence contradiction by A11, A14, XBOOLE_1:63; ::_thesis: verum
end;
suppose A meets B ^b ; ::_thesis: contradiction
then not A ^b misses B by A1, Th6;
then Q ^b meets B by A13, FIN_TOPO:14, XBOOLE_1:63;
hence contradiction by A11, A14, XBOOLE_1:63; ::_thesis: verum
end;
end;
end;
A15: now__::_thesis:_not_A_/\_P_=_{}
assume A16: A /\ P = {} ; ::_thesis: contradiction
then A17: A /\ Q = (A /\ P) \/ (A /\ Q)
.= A /\ (P \/ Q) by XBOOLE_1:23
.= A by A5, XBOOLE_1:21 ;
A18: now__::_thesis:_not_B_/\_Q_=_{}
assume B /\ Q = {} ; ::_thesis: contradiction
then B /\ P = (B /\ Q) \/ (B /\ P)
.= B /\ (Q \/ P) by XBOOLE_1:23
.= B by A5, XBOOLE_1:21 ;
hence contradiction by A12, A17, XBOOLE_1:18; ::_thesis: verum
end;
set P3 = B /\ P;
set Q3 = B /\ Q;
A19: (B /\ P) \/ (B /\ Q) = B /\ (P \/ Q) by XBOOLE_1:23
.= B by A5, XBOOLE_1:21 ;
A20: B /\ P misses B /\ Q by A8, XBOOLE_1:76;
( (B /\ P) ^b c= P ^b & B /\ Q c= Q ) by FIN_TOPO:14, XBOOLE_1:17;
then A21: (B /\ P) ^b misses B /\ Q by A9, XBOOLE_1:64;
B /\ P = (A /\ P) \/ (B /\ P) by A16
.= (A \/ B) /\ P by XBOOLE_1:23
.= P by A5, XBOOLE_1:21 ;
hence contradiction by A3, A6, A18, A19, A20, A21, FIN_TOPO:def_16; ::_thesis: verum
end;
A22: now__::_thesis:_(_A_c=_P_implies_not_B_c=_Q_)
assume that
A23: A c= P and
A24: B c= Q ; ::_thesis: contradiction
A25: A ^b c= P ^b by A23, FIN_TOPO:14;
percases ( A ^b meets B or A meets B ^b ) by A4, FINTOPO4:def_1;
suppose A ^b meets B ; ::_thesis: contradiction
hence contradiction by A9, A24, A25, XBOOLE_1:64; ::_thesis: verum
end;
suppose A meets B ^b ; ::_thesis: contradiction
then not A ^b misses B by A1, Th6;
hence contradiction by A9, A24, A25, XBOOLE_1:64; ::_thesis: verum
end;
end;
end;
A26: now__::_thesis:_not_A_/\_Q_=_{}
assume A27: A /\ Q = {} ; ::_thesis: contradiction
then A28: A /\ P = (A /\ Q) \/ (A /\ P)
.= A /\ (Q \/ P) by XBOOLE_1:23
.= A by A5, XBOOLE_1:21 ;
A29: now__::_thesis:_not_B_/\_P_=_{}
assume B /\ P = {} ; ::_thesis: contradiction
then B /\ Q = (B /\ P) \/ (B /\ Q)
.= B /\ (P \/ Q) by XBOOLE_1:23
.= B by A5, XBOOLE_1:21 ;
hence contradiction by A22, A28, XBOOLE_1:18; ::_thesis: verum
end;
set P3 = B /\ Q;
set Q3 = B /\ P;
A30: (B /\ P) \/ (B /\ Q) = B /\ (P \/ Q) by XBOOLE_1:23
.= B by A5, XBOOLE_1:21 ;
A31: B /\ Q misses B /\ P by A8, XBOOLE_1:76;
( (B /\ Q) ^b c= Q ^b & B /\ P c= P ) by FIN_TOPO:14, XBOOLE_1:17;
then A32: (B /\ Q) ^b misses B /\ P by A11, XBOOLE_1:64;
B /\ Q = (A /\ Q) \/ (B /\ Q) by A27
.= (A \/ B) /\ Q by XBOOLE_1:23
.= Q by A5, XBOOLE_1:21 ;
hence contradiction by A3, A7, A29, A30, A31, A32, FIN_TOPO:def_16; ::_thesis: verum
end;
( (A /\ P) ^b c= P ^b & A /\ Q c= Q ) by FIN_TOPO:14, XBOOLE_1:17;
then A33: (A /\ P) ^b misses A /\ Q by A9, XBOOLE_1:64;
(A /\ P) \/ (A /\ Q) = A /\ (P \/ Q) by XBOOLE_1:23
.= A by A5, XBOOLE_1:21 ;
hence contradiction by A2, A15, A26, A10, A33, FIN_TOPO:def_16; ::_thesis: verum
end;
theorem Th35: :: FINTOPO6:35
for FT being non empty RelStr
for A, C being Subset of FT st FT is symmetric & C is connected & C c= A & A c= C ^b holds
A is connected
proof
let FT be non empty RelStr ; ::_thesis: for A, C being Subset of FT st FT is symmetric & C is connected & C c= A & A c= C ^b holds
A is connected
let A, C be Subset of FT; ::_thesis: ( FT is symmetric & C is connected & C c= A & A c= C ^b implies A is connected )
assume that
A1: FT is symmetric and
A2: C is connected and
A3: C c= A and
A4: A c= C ^b ; ::_thesis: A is connected
let P2, Q2 be Subset of FT; :: according to FIN_TOPO:def_16 ::_thesis: ( not A = P2 \/ Q2 or P2 = {} or Q2 = {} or not P2 misses Q2 or not P2 ^b misses Q2 )
assume that
A5: A = P2 \/ Q2 and
A6: P2 <> {} and
A7: Q2 <> {} and
A8: P2 misses Q2 ; ::_thesis: not P2 ^b misses Q2
assume A9: P2 ^b misses Q2 ; ::_thesis: contradiction
set x2 = the Element of Q2;
A10: the Element of Q2 in Q2 by A7;
Q2 c= Q2 \/ P2 by XBOOLE_1:7;
then Q2 c= C ^b by A4, A5, XBOOLE_1:1;
then the Element of Q2 in C ^b by A10;
then consider z2 being Element of FT such that
A11: z2 = the Element of Q2 and
A12: U_FT z2 meets C ;
set y3 = the Element of (U_FT z2) /\ C;
A13: (U_FT z2) /\ C <> {} by A12, XBOOLE_0:def_7;
then the Element of (U_FT z2) /\ C in (U_FT z2) /\ C ;
then reconsider y4 = the Element of (U_FT z2) /\ C as Element of FT ;
the Element of (U_FT z2) /\ C in U_FT z2 by A13, XBOOLE_0:def_4;
then z2 in U_FT y4 by A1, FIN_TOPO:def_13;
then z2 in (U_FT y4) /\ Q2 by A7, A11, XBOOLE_0:def_4;
then A14: U_FT y4 meets Q2 by XBOOLE_0:def_7;
set P3 = P2 /\ C;
set Q3 = Q2 /\ C;
A15: C = A /\ C by A3, XBOOLE_1:28
.= (P2 /\ C) \/ (Q2 /\ C) by A5, XBOOLE_1:23 ;
set x = the Element of P2;
A16: the Element of P2 in P2 by A6;
P2 c= P2 \/ Q2 by XBOOLE_1:7;
then P2 c= C ^b by A4, A5, XBOOLE_1:1;
then the Element of P2 in C ^b by A16;
then consider z being Element of FT such that
A17: z = the Element of P2 and
A18: U_FT z meets C ;
set y = the Element of (U_FT z) /\ C;
A19: (U_FT z) /\ C <> {} by A18, XBOOLE_0:def_7;
then the Element of (U_FT z) /\ C in (U_FT z) /\ C ;
then reconsider y2 = the Element of (U_FT z) /\ C as Element of FT ;
the Element of (U_FT z) /\ C in U_FT z by A19, XBOOLE_0:def_4;
then z in U_FT y2 by A1, FIN_TOPO:def_13;
then z in (U_FT y2) /\ P2 by A6, A17, XBOOLE_0:def_4;
then U_FT y2 meets P2 by XBOOLE_0:def_7;
then A20: y2 in P2 ^b ;
A21: y4 in C by A13, XBOOLE_0:def_4;
A22: now__::_thesis:_not_Q2_/\_C_=_{}
assume Q2 /\ C = {} ; ::_thesis: contradiction
then A23: y4 in P2 by A21, A15, XBOOLE_0:def_4;
consider w being Element of FT such that
A24: w = y4 and
A25: U_FT w meets Q2 by A14;
consider s being set such that
A26: s in U_FT w and
A27: s in Q2 by A25, XBOOLE_0:3;
reconsider s2 = s as Element of FT by A26;
w in U_FT s2 by A1, A26, FIN_TOPO:def_13;
then U_FT s2 meets P2 by A23, A24, XBOOLE_0:3;
then s2 in P2 ^b ;
hence contradiction by A9, A27, XBOOLE_0:3; ::_thesis: verum
end;
A28: P2 /\ C c= P2 by XBOOLE_1:17;
A29: y2 in C by A19, XBOOLE_0:def_4;
A30: now__::_thesis:_not_P2_/\_C_=_{}
assume P2 /\ C = {} ; ::_thesis: contradiction
then y2 in Q2 by A29, A15, XBOOLE_0:def_4;
then y2 in (P2 ^b) /\ Q2 by A20, XBOOLE_0:def_4;
hence contradiction by A9, XBOOLE_0:def_7; ::_thesis: verum
end;
P2 /\ C misses Q2 by A8, XBOOLE_1:17, XBOOLE_1:63;
then P2 /\ C misses Q2 /\ C by XBOOLE_1:17, XBOOLE_1:63;
then (P2 /\ C) ^b meets Q2 /\ C by A2, A15, A30, A22, FIN_TOPO:def_16;
then P2 ^b meets Q2 /\ C by A28, FIN_TOPO:14, XBOOLE_1:63;
hence contradiction by A9, XBOOLE_1:17, XBOOLE_1:63; ::_thesis: verum
end;
theorem Th36: :: FINTOPO6:36
for FT being non empty RelStr
for C being Subset of FT st FT is filled & FT is symmetric & C is connected holds
C ^b is connected
proof
let FT be non empty RelStr ; ::_thesis: for C being Subset of FT st FT is filled & FT is symmetric & C is connected holds
C ^b is connected
let C be Subset of FT; ::_thesis: ( FT is filled & FT is symmetric & C is connected implies C ^b is connected )
assume that
A1: ( FT is filled & FT is symmetric ) and
A2: C is connected ; ::_thesis: C ^b is connected
C c= C ^b by A1, FIN_TOPO:13;
hence C ^b is connected by A1, A2, Th35; ::_thesis: verum
end;
theorem Th37: :: FINTOPO6:37
for FT being non empty RelStr
for A, B, C being Subset of FT st FT is filled & FT is symmetric & FT is connected & A is connected & ([#] FT) \ A = B \/ C & B,C are_separated holds
A \/ B is connected
proof
let FT be non empty RelStr ; ::_thesis: for A, B, C being Subset of FT st FT is filled & FT is symmetric & FT is connected & A is connected & ([#] FT) \ A = B \/ C & B,C are_separated holds
A \/ B is connected
let A, B, C be Subset of FT; ::_thesis: ( FT is filled & FT is symmetric & FT is connected & A is connected & ([#] FT) \ A = B \/ C & B,C are_separated implies A \/ B is connected )
assume that
A1: ( FT is filled & FT is symmetric ) and
A2: FT is connected and
A3: A is connected and
A4: ([#] FT) \ A = B \/ C and
A5: B,C are_separated ; ::_thesis: A \/ B is connected
A6: [#] FT is connected by A2, Def1;
now__::_thesis:_for_P,_Q_being_Subset_of_FT_st_A_\/_B_=_P_\/_Q_&_P_misses_Q_&_P,Q_are_separated_&_not_P_=_{}_FT_holds_
Q_=_{}_FT
let P, Q be Subset of FT; ::_thesis: ( A \/ B = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT implies Q = {} FT )
assume that
A7: A \/ B = P \/ Q and
P misses Q and
A8: P,Q are_separated ; ::_thesis: ( P = {} FT or Q = {} FT )
A9: [#] FT = A \/ (B \/ C) by A4, XBOOLE_1:45
.= (P \/ Q) \/ C by A7, XBOOLE_1:4 ;
A10: now__::_thesis:_(_not_A_c=_Q_or_P_=_{}_FT_or_Q_=_{}_FT_)
A11: [#] FT = P \/ (Q \/ C) by A9, XBOOLE_1:4;
assume A c= Q ; ::_thesis: ( P = {} FT or Q = {} FT )
then P misses A by A1, A8, Th29, FINTOPO4:6;
then P c= B by A7, XBOOLE_1:7, XBOOLE_1:73;
then A12: P,C are_separated by A5, Th29;
then P misses Q \/ C by A1, A8, Th30, FINTOPO4:6;
hence ( P = {} FT or Q = {} FT ) by A6, A8, A12, A11, Th4, Th30; ::_thesis: verum
end;
now__::_thesis:_(_not_A_c=_P_or_P_=_{}_FT_or_Q_=_{}_FT_)
A13: [#] FT = Q \/ (P \/ C) by A9, XBOOLE_1:4;
assume A c= P ; ::_thesis: ( P = {} FT or Q = {} FT )
then Q misses A by A1, A8, Th29, FINTOPO4:6;
then Q c= B by A7, XBOOLE_1:7, XBOOLE_1:73;
then A14: Q,C are_separated by A5, Th29;
then Q misses P \/ C by A1, A8, Th30, FINTOPO4:6;
hence ( P = {} FT or Q = {} FT ) by A6, A8, A14, A13, Th4, Th30; ::_thesis: verum
end;
hence ( P = {} FT or Q = {} FT ) by A1, A3, A7, A8, A10, Th33, XBOOLE_1:7; ::_thesis: verum
end;
hence A \/ B is connected by A1, Th7; ::_thesis: verum
end;
theorem Th38: :: FINTOPO6:38
for FT being non empty RelStr
for X9 being non empty SubSpace of FT
for A being Subset of FT
for B being Subset of X9 st A = B holds
( A is connected iff B is connected )
proof
let FT be non empty RelStr ; ::_thesis: for X9 being non empty SubSpace of FT
for A being Subset of FT
for B being Subset of X9 st A = B holds
( A is connected iff B is connected )
let X9 be non empty SubSpace of FT; ::_thesis: for A being Subset of FT
for B being Subset of X9 st A = B holds
( A is connected iff B is connected )
let A8 be Subset of FT; ::_thesis: for B being Subset of X9 st A8 = B holds
( A8 is connected iff B is connected )
let B8 be Subset of X9; ::_thesis: ( A8 = B8 implies ( A8 is connected iff B8 is connected ) )
assume A1: A8 = B8 ; ::_thesis: ( A8 is connected iff B8 is connected )
percases ( A8 = {} or A8 <> {} ) ;
suppose A8 = {} ; ::_thesis: ( A8 is connected iff B8 is connected )
hence ( A8 is connected iff B8 is connected ) by A1; ::_thesis: verum
end;
supposeA2: A8 <> {} ; ::_thesis: ( A8 is connected iff B8 is connected )
then reconsider A = A8 as non empty Subset of FT ;
reconsider B = B8 as non empty Subset of X9 by A1, A2;
reconsider X = X9 as non empty RelStr ;
A3: now__::_thesis:_(_not_A8_is_connected_implies_not_B8_is_connected_)
assume not A8 is connected ; ::_thesis: not B8 is connected
then consider P, Q being Subset of FT such that
A4: A8 = P \/ Q and
A5: ( P <> {} & Q <> {} & P misses Q ) and
A6: P ^b misses Q by FIN_TOPO:def_16;
Q c= A8 by A4, XBOOLE_1:7;
then reconsider Q9 = Q as Subset of X by A1, XBOOLE_1:1;
P c= A8 by A4, XBOOLE_1:7;
then reconsider P9 = P as Subset of X by A1, XBOOLE_1:1;
A7: Q9 c= the carrier of X ;
P9 ^b = (P ^b) /\ ([#] X) by Th13;
then (P9 ^b) /\ Q9 = (P ^b) /\ (([#] X) /\ Q) by XBOOLE_1:16
.= (P ^b) /\ Q by A7, XBOOLE_1:28
.= {} by A6, XBOOLE_0:def_7 ;
then P9 ^b misses Q9 by XBOOLE_0:def_7;
hence not B8 is connected by A1, A4, A5, FIN_TOPO:def_16; ::_thesis: verum
end;
now__::_thesis:_(_not_B_is_connected_implies_not_A_is_connected_)
assume not B is connected ; ::_thesis: not A is connected
then consider P, Q being Subset of X9 such that
A8: ( B8 = P \/ Q & P <> {} & Q <> {} & P misses Q ) and
A9: P ^b misses Q by FIN_TOPO:def_16;
the carrier of X c= the carrier of FT by Def2;
then reconsider Q9 = Q as Subset of FT by XBOOLE_1:1;
the carrier of X c= the carrier of FT by Def2;
then reconsider P9 = P as Subset of FT by XBOOLE_1:1;
A10: P ^b = (P9 ^b) /\ ([#] X) by Th13;
(P9 ^b) /\ Q9 = (P9 ^b) /\ (([#] X) /\ Q) by XBOOLE_1:28
.= (P ^b) /\ Q by A10, XBOOLE_1:16
.= {} by A9, XBOOLE_0:def_7 ;
then P9 ^b misses Q9 by XBOOLE_0:def_7;
hence not A is connected by A1, A8, FIN_TOPO:def_16; ::_thesis: verum
end;
hence ( A8 is connected iff B8 is connected ) by A3; ::_thesis: verum
end;
end;
end;
theorem :: FINTOPO6:39
for FT being non empty RelStr
for A being Subset of FT st FT is filled & FT is symmetric & A is_a_component_of FT holds
A is closed
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st FT is filled & FT is symmetric & A is_a_component_of FT holds
A is closed
let A be Subset of FT; ::_thesis: ( FT is filled & FT is symmetric & A is_a_component_of FT implies A is closed )
assume that
A1: ( FT is filled & FT is symmetric ) and
A2: A is_a_component_of FT ; ::_thesis: A is closed
A is connected by A2, Def4;
then A3: A ^b is connected by A1, Th36;
A c= A ^b by A1, FIN_TOPO:13;
hence A = A ^b by A2, A3, Def4; :: according to FIN_TOPO:def_15 ::_thesis: verum
end;
theorem Th40: :: FINTOPO6:40
for FT being non empty RelStr
for A, B being Subset of FT st FT is symmetric & A is_a_component_of FT & B is_a_component_of FT & not A = B holds
A,B are_separated
proof
let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT st FT is symmetric & A is_a_component_of FT & B is_a_component_of FT & not A = B holds
A,B are_separated
let A, B be Subset of FT; ::_thesis: ( FT is symmetric & A is_a_component_of FT & B is_a_component_of FT & not A = B implies A,B are_separated )
assume that
A1: FT is symmetric and
A2: A is_a_component_of FT and
A3: B is_a_component_of FT ; ::_thesis: ( A = B or A,B are_separated )
A4: A is connected by A2, Def4;
A5: A c= A \/ B by XBOOLE_1:7;
assume that
A6: A <> B and
A7: not A,B are_separated ; ::_thesis: contradiction
B is connected by A3, Def4;
then A \/ B is connected by A1, A7, A4, Th34;
then ( B c= A \/ B & A = A \/ B ) by A2, A5, Def4, XBOOLE_1:7;
hence contradiction by A3, A6, A4, Def4; ::_thesis: verum
end;
theorem :: FINTOPO6:41
for FT being non empty RelStr
for A, B being Subset of FT st FT is filled & FT is symmetric & A is_a_component_of FT & B is_a_component_of FT & not A = B holds
A misses B by Th40, FINTOPO4:6;
theorem :: FINTOPO6:42
for FT being non empty RelStr
for C being Subset of FT st FT is filled & FT is symmetric & C is connected holds
for S being Subset of FT holds
( not S is_a_component_of FT or C misses S or C c= S )
proof
let FT be non empty RelStr ; ::_thesis: for C being Subset of FT st FT is filled & FT is symmetric & C is connected holds
for S being Subset of FT holds
( not S is_a_component_of FT or C misses S or C c= S )
let C be Subset of FT; ::_thesis: ( FT is filled & FT is symmetric & C is connected implies for S being Subset of FT holds
( not S is_a_component_of FT or C misses S or C c= S ) )
assume A1: ( FT is filled & FT is symmetric & C is connected ) ; ::_thesis: for S being Subset of FT holds
( not S is_a_component_of FT or C misses S or C c= S )
let S be Subset of FT; ::_thesis: ( not S is_a_component_of FT or C misses S or C c= S )
assume A2: S is_a_component_of FT ; ::_thesis: ( C misses S or C c= S )
A3: S c= C \/ S by XBOOLE_1:7;
assume A4: C meets S ; ::_thesis: C c= S
S is connected by A2, Def4;
then C \/ S is connected by A1, A4, Th34, FINTOPO4:6;
then S = C \/ S by A2, A3, Def4;
hence C c= S by XBOOLE_1:7; ::_thesis: verum
end;
definition
let FT be non empty RelStr ;
let A be non empty Subset of FT;
let B be Subset of FT;
predB is_a_component_of A means :Def5: :: FINTOPO6:def 5
ex B1 being Subset of (FT | A) st
( B1 = B & B1 is_a_component_of FT | A );
end;
:: deftheorem Def5 defines is_a_component_of FINTOPO6:def_5_:_
for FT being non empty RelStr
for A being non empty Subset of FT
for B being Subset of FT holds
( B is_a_component_of A iff ex B1 being Subset of (FT | A) st
( B1 = B & B1 is_a_component_of FT | A ) );
theorem :: FINTOPO6:43
for FT being non empty RelStr
for A, C being Subset of FT
for D being non empty Subset of FT st FT is filled & FT is symmetric & D = ([#] FT) \ A & FT is connected & A is connected & C is_a_component_of D holds
([#] FT) \ C is connected
proof
let FT be non empty RelStr ; ::_thesis: for A, C being Subset of FT
for D being non empty Subset of FT st FT is filled & FT is symmetric & D = ([#] FT) \ A & FT is connected & A is connected & C is_a_component_of D holds
([#] FT) \ C is connected
let A, C be Subset of FT; ::_thesis: for D being non empty Subset of FT st FT is filled & FT is symmetric & D = ([#] FT) \ A & FT is connected & A is connected & C is_a_component_of D holds
([#] FT) \ C is connected
let D be non empty Subset of FT; ::_thesis: ( FT is filled & FT is symmetric & D = ([#] FT) \ A & FT is connected & A is connected & C is_a_component_of D implies ([#] FT) \ C is connected )
assume that
A1: ( FT is filled & FT is symmetric ) and
A2: D = ([#] FT) \ A and
A3: FT is connected and
A4: A is connected and
A5: C is_a_component_of D ; ::_thesis: ([#] FT) \ C is connected
consider C1 being Subset of (FT | D) such that
A6: C1 = C and
A7: C1 is_a_component_of FT | D by A5, Def5;
reconsider C2 = C1 as Subset of FT by A6;
C1 c= [#] (FT | D) ;
then C1 c= ([#] FT) \ A by A2, Def3;
then A8: (([#] FT) \ A) ` c= C2 ` by SUBSET_1:12;
then A9: A c= C2 ` by PRE_TOPC:3;
A10: A c= ([#] FT) \ C2 by A8, PRE_TOPC:3;
A11: C1 is connected by A7, Def4;
now__::_thesis:_for_P,_Q_being_Subset_of_FT_st_([#]_FT)_\_C_=_P_\/_Q_&_P_misses_Q_&_P,Q_are_separated_&_not_P_=_{}_FT_holds_
Q_=_{}_FT
A misses C1 by A9, SUBSET_1:23;
then A12: A /\ C1 = {} by XBOOLE_0:def_7;
let P, Q be Subset of FT; ::_thesis: ( ([#] FT) \ C = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT implies Q = {} FT )
assume that
A13: ([#] FT) \ C = P \/ Q and
A14: P misses Q and
A15: P,Q are_separated ; ::_thesis: ( P = {} FT or Q = {} FT )
A16: C is connected by A6, A11, Th38;
A17: now__::_thesis:_(_A_c=_Q_implies_P_=_{}_FT_)
assume A18: A c= Q ; ::_thesis: P = {} FT
P c= Q ` by A14, SUBSET_1:23;
then ( Q misses Q ` & A /\ P c= Q /\ (Q `) ) by A18, XBOOLE_1:27, XBOOLE_1:79;
then A19: A /\ P c= {} by XBOOLE_0:def_7;
(C \/ P) /\ A = (A /\ C) \/ (A /\ P) by XBOOLE_1:23
.= {} by A6, A12, A19, XBOOLE_1:3 ;
then C \/ P misses A by XBOOLE_0:def_7;
then C \/ P c= A ` by SUBSET_1:23;
then C \/ P c= [#] (FT | D) by A2, Def3;
then reconsider C1P1 = C \/ P as Subset of (FT | D) ;
C \/ P is connected by A1, A3, A13, A15, A16, Th37;
then A20: C1P1 is connected by Th38;
C c= C1 \/ P by A6, XBOOLE_1:7;
then C1P1 = C1 by A6, A7, A20, Def4;
then A21: P c= C by A6, XBOOLE_1:7;
P c= ([#] FT) \ C by A13, XBOOLE_1:7;
then ( C misses C ` & P c= C /\ (([#] FT) \ C) ) by A21, XBOOLE_1:19, XBOOLE_1:79;
then P c= {} by XBOOLE_0:def_7;
hence P = {} FT by XBOOLE_1:3; ::_thesis: verum
end;
A22: P misses P ` by XBOOLE_1:79;
A23: Q c= ([#] FT) \ C by A13, XBOOLE_1:7;
now__::_thesis:_(_A_c=_P_implies_Q_=_{}_FT_)
assume A24: A c= P ; ::_thesis: Q = {} FT
Q c= P ` by A14, SUBSET_1:23;
then A /\ Q c= P /\ (P `) by A24, XBOOLE_1:27;
then A25: A /\ Q c= {} by A22, XBOOLE_0:def_7;
(C \/ Q) /\ A = (A /\ C) \/ (A /\ Q) by XBOOLE_1:23
.= {} by A6, A12, A25, XBOOLE_1:3 ;
then C \/ Q misses A by XBOOLE_0:def_7;
then C \/ Q c= A ` by SUBSET_1:23;
then C \/ Q c= [#] (FT | D) by A2, Def3;
then reconsider C1Q1 = C \/ Q as Subset of (FT | D) ;
C \/ Q is connected by A1, A3, A13, A15, A16, Th37;
then A26: C1Q1 is connected by Th38;
C1 c= C1 \/ Q by XBOOLE_1:7;
then C1Q1 = C1 by A6, A7, A26, Def4;
then Q c= C by A6, XBOOLE_1:7;
then ( C misses C ` & Q c= C /\ (([#] FT) \ C) ) by A23, XBOOLE_1:19, XBOOLE_1:79;
then Q c= {} by XBOOLE_0:def_7;
hence Q = {} FT by XBOOLE_1:3; ::_thesis: verum
end;
hence ( P = {} FT or Q = {} FT ) by A1, A4, A6, A10, A13, A15, A17, Th33; ::_thesis: verum
end;
hence ([#] FT) \ C is connected by A1, Th7; ::_thesis: verum
end;
begin
definition
let FT be non empty RelStr ;
let f be FinSequence of FT;
attrf is continuous means :Def6: :: FINTOPO6:def 6
( 1 <= len f & ( for i being Nat
for x1 being Element of FT st 1 <= i & i < len f & x1 = f . i holds
f . (i + 1) in U_FT x1 ) );
end;
:: deftheorem Def6 defines continuous FINTOPO6:def_6_:_
for FT being non empty RelStr
for f being FinSequence of FT holds
( f is continuous iff ( 1 <= len f & ( for i being Nat
for x1 being Element of FT st 1 <= i & i < len f & x1 = f . i holds
f . (i + 1) in U_FT x1 ) ) );
Lm2: for FT being non empty RelStr
for x being Element of FT holds <*x*> is continuous
proof
let FT be non empty RelStr ; ::_thesis: for x being Element of FT holds <*x*> is continuous
let x be Element of FT; ::_thesis: <*x*> is continuous
thus 1 <= len <*x*> by FINSEQ_1:39; :: according to FINTOPO6:def_6 ::_thesis: for i being Nat
for x1 being Element of FT st 1 <= i & i < len <*x*> & x1 = <*x*> . i holds
<*x*> . (i + 1) in U_FT x1
thus for i being Nat
for x1 being Element of FT st 1 <= i & i < len <*x*> & x1 = <*x*> . i holds
<*x*> . (i + 1) in U_FT x1 by FINSEQ_1:39; ::_thesis: verum
end;
registration
let FT be non empty RelStr ;
let x be Element of FT;
cluster<*x*> -> continuous for FinSequence of FT;
coherence
for b1 being FinSequence of FT st b1 = <*x*> holds
b1 is continuous by Lm2;
end;
theorem Th44: :: FINTOPO6:44
for FT being non empty RelStr
for f being FinSequence of FT
for x, y being Element of FT st f is continuous & y = f . (len f) & x in U_FT y holds
f ^ <*x*> is continuous
proof
let FT be non empty RelStr ; ::_thesis: for f being FinSequence of FT
for x, y being Element of FT st f is continuous & y = f . (len f) & x in U_FT y holds
f ^ <*x*> is continuous
let f be FinSequence of FT; ::_thesis: for x, y being Element of FT st f is continuous & y = f . (len f) & x in U_FT y holds
f ^ <*x*> is continuous
let x, y be Element of FT; ::_thesis: ( f is continuous & y = f . (len f) & x in U_FT y implies f ^ <*x*> is continuous )
assume that
A1: f is continuous and
A2: y = f . (len f) and
A3: x in U_FT y ; ::_thesis: f ^ <*x*> is continuous
reconsider g = f ^ <*x*> as FinSequence of FT ;
A4: dom f = Seg (len f) by FINSEQ_1:def_3;
A5: len <*x*> = 1 by FINSEQ_1:39;
A6: for i being Nat
for x1 being Element of FT st 1 <= i & i < len g & x1 = g . i holds
g . (i + 1) in U_FT x1
proof
let i be Nat; ::_thesis: for x1 being Element of FT st 1 <= i & i < len g & x1 = g . i holds
g . (i + 1) in U_FT x1
let x1 be Element of FT; ::_thesis: ( 1 <= i & i < len g & x1 = g . i implies g . (i + 1) in U_FT x1 )
assume that
A7: 1 <= i and
A8: i < len g and
A9: x1 = g . i ; ::_thesis: g . (i + 1) in U_FT x1
( i + 1 <= len g & 1 < i + 1 ) by A7, A8, NAT_1:13;
then i + 1 in dom g by FINSEQ_3:25;
then g . (i + 1) = g /. (i + 1) by PARTFUN1:def_6;
then reconsider x2 = g . (i + 1) as Element of FT ;
now__::_thesis:_x2_in_U_FT_x1
percases ( i < len f or i >= len f ) ;
supposeA10: i < len f ; ::_thesis: x2 in U_FT x1
A11: 1 <= i + 1 by NAT_1:11;
i + 1 <= len f by A10, NAT_1:13;
then i + 1 in dom f by A11, FINSEQ_3:25;
then A12: g . (i + 1) = f . (i + 1) by FINSEQ_1:def_7;
i in dom f by A4, A7, A10, FINSEQ_1:1;
then g . i = f . i by FINSEQ_1:def_7;
hence x2 in U_FT x1 by A1, A7, A9, A10, A12, Def6; ::_thesis: verum
end;
supposeA13: i >= len f ; ::_thesis: x2 in U_FT x1
len g = (len f) + 1 by A5, FINSEQ_1:22;
then A14: i <= len f by A8, NAT_1:13;
then A15: i = len f by A13, XXREAL_0:1;
i in dom f by A4, A7, A14, FINSEQ_1:1;
then x1 = y by A2, A9, A15, FINSEQ_1:def_7;
hence x2 in U_FT x1 by A3, A15, FINSEQ_1:42; ::_thesis: verum
end;
end;
end;
hence g . (i + 1) in U_FT x1 ; ::_thesis: verum
end;
len (f ^ <*x*>) = (len f) + (len <*x*>) by FINSEQ_1:22
.= (len f) + 1 by FINSEQ_1:39 ;
then len (f ^ <*x*>) >= 1 by NAT_1:11;
hence f ^ <*x*> is continuous by A6, Def6; ::_thesis: verum
end;
theorem Th45: :: FINTOPO6:45
for FT being non empty RelStr
for f, g being FinSequence of FT st f is continuous & g is continuous & g . 1 in U_FT (f /. (len f)) holds
f ^ g is continuous
proof
let FT be non empty RelStr ; ::_thesis: for f, g being FinSequence of FT st f is continuous & g is continuous & g . 1 in U_FT (f /. (len f)) holds
f ^ g is continuous
let f, g be FinSequence of FT; ::_thesis: ( f is continuous & g is continuous & g . 1 in U_FT (f /. (len f)) implies f ^ g is continuous )
assume that
A1: f is continuous and
A2: g is continuous and
A3: g . 1 in U_FT (f /. (len f)) ; ::_thesis: f ^ g is continuous
A4: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
len g >= 1 by A2, Def6;
then len (f ^ g) >= 0 + 1 by A4, XREAL_1:7;
hence len (f ^ g) >= 1 ; :: according to FINTOPO6:def_6 ::_thesis: for i being Nat
for x1 being Element of FT st 1 <= i & i < len (f ^ g) & x1 = (f ^ g) . i holds
(f ^ g) . (i + 1) in U_FT x1
let i be Nat; ::_thesis: for x1 being Element of FT st 1 <= i & i < len (f ^ g) & x1 = (f ^ g) . i holds
(f ^ g) . (i + 1) in U_FT x1
let x1 be Element of FT; ::_thesis: ( 1 <= i & i < len (f ^ g) & x1 = (f ^ g) . i implies (f ^ g) . (i + 1) in U_FT x1 )
set g2 = f ^ g;
A5: dom f = Seg (len f) by FINSEQ_1:def_3;
A6: len f >= 1 by A1, Def6;
assume that
A7: 1 <= i and
A8: i < len (f ^ g) and
A9: x1 = (f ^ g) . i ; ::_thesis: (f ^ g) . (i + 1) in U_FT x1
( i + 1 <= len (f ^ g) & 1 < i + 1 ) by A7, A8, NAT_1:13;
then i + 1 in dom (f ^ g) by FINSEQ_3:25;
then (f ^ g) . (i + 1) = (f ^ g) /. (i + 1) by PARTFUN1:def_6;
then reconsider x2 = (f ^ g) . (i + 1) as Element of FT ;
percases ( i < len f or i >= len f ) ;
supposeA10: i < len f ; ::_thesis: (f ^ g) . (i + 1) in U_FT x1
A11: 1 <= i + 1 by NAT_1:11;
i + 1 <= len f by A10, NAT_1:13;
then i + 1 in dom f by A11, FINSEQ_3:25;
then A12: (f ^ g) . (i + 1) = f . (i + 1) by FINSEQ_1:def_7;
i in dom f by A5, A7, A10, FINSEQ_1:1;
then (f ^ g) . i = f . i by FINSEQ_1:def_7;
hence (f ^ g) . (i + 1) in U_FT x1 by A1, A7, A9, A10, A12, Def6; ::_thesis: verum
end;
supposeA13: i >= len f ; ::_thesis: (f ^ g) . (i + 1) in U_FT x1
then A14: i + 1 > len f by NAT_1:13;
A15: i < (len f) + (len g) by A8, FINSEQ_1:22;
A16: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
then A17: i + 1 <= (len f) + (len g) by A8, NAT_1:13;
percases ( i = len f or i > len f ) by A13, XXREAL_0:1;
supposeA18: i = len f ; ::_thesis: (f ^ g) . (i + 1) in U_FT x1
A19: len f in dom f by A6, FINSEQ_3:25;
then A20: x1 = f . (len f) by A9, A18, FINSEQ_1:def_7
.= f /. (len f) by A19, PARTFUN1:def_6 ;
x2 = g . ((i + 1) - (len f)) by A14, A16, A17, FINSEQ_1:24
.= g . 1 by A18 ;
hence (f ^ g) . (i + 1) in U_FT x1 by A3, A20; ::_thesis: verum
end;
supposeA21: i > len f ; ::_thesis: (f ^ g) . (i + 1) in U_FT x1
set j = i -' (len f);
A22: i - (len f) > 0 by A21, XREAL_1:50;
then A23: i -' (len f) = i - (len f) by XREAL_0:def_2;
then (i -' (len f)) + 1 = (i + 1) - (len f) ;
then A24: x2 = g . ((i -' (len f)) + 1) by A14, A16, A17, FINSEQ_1:24;
A25: i - (len f) < len g by A15, XREAL_1:19;
i >= (len f) + 1 by A21, NAT_1:13;
then A26: x1 = g . (i -' (len f)) by A9, A15, A23, FINSEQ_1:23;
i -' (len f) >= 0 + 1 by A22, A23, NAT_1:13;
hence (f ^ g) . (i + 1) in U_FT x1 by A2, A23, A24, A26, A25, Def6; ::_thesis: verum
end;
end;
end;
end;
end;
definition
let FT be non empty RelStr ;
let A be Subset of FT;
attrA is arcwise_connected means :Def7: :: FINTOPO6:def 7
for x1, x2 being Element of FT st x1 in A & x2 in A holds
ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 );
end;
:: deftheorem Def7 defines arcwise_connected FINTOPO6:def_7_:_
for FT being non empty RelStr
for A being Subset of FT holds
( A is arcwise_connected iff for x1, x2 being Element of FT st x1 in A & x2 in A holds
ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) );
registration
let FT be non empty RelStr ;
cluster empty -> arcwise_connected for Element of K32( the carrier of FT);
coherence
for b1 being Subset of FT st b1 is empty holds
b1 is arcwise_connected
proof
let S be Subset of FT; ::_thesis: ( S is empty implies S is arcwise_connected )
assume S is empty ; ::_thesis: S is arcwise_connected
hence for x1, x2 being Element of FT st x1 in S & x2 in S holds
ex f being FinSequence of FT st
( f is continuous & rng f c= S & f . 1 = x1 & f . (len f) = x2 ) ; :: according to FINTOPO6:def_7 ::_thesis: verum
end;
end;
Lm3: for FT being non empty RelStr
for x being Element of FT holds {x} is arcwise_connected
proof
let FT be non empty RelStr ; ::_thesis: for x being Element of FT holds {x} is arcwise_connected
let x be Element of FT; ::_thesis: {x} is arcwise_connected
set A = {x};
A1: rng <*x*> c= {x} by FINSEQ_1:39;
A2: <*x*> . 1 = x by FINSEQ_1:40;
then A3: <*x*> . (len <*x*>) = x by FINSEQ_1:40;
for x1, x2 being Element of FT st x1 in {x} & x2 in {x} holds
ex f being FinSequence of FT st
( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 )
proof
let x1, x2 be Element of FT; ::_thesis: ( x1 in {x} & x2 in {x} implies ex f being FinSequence of FT st
( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 ) )
assume ( x1 in {x} & x2 in {x} ) ; ::_thesis: ex f being FinSequence of FT st
( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 )
then ( x1 = x & x2 = x ) by TARSKI:def_1;
hence ex f being FinSequence of FT st
( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 ) by A2, A3, A1; ::_thesis: verum
end;
hence {x} is arcwise_connected by Def7; ::_thesis: verum
end;
registration
let FT be non empty RelStr ;
let x be Element of FT;
cluster{x} -> arcwise_connected for Subset of FT;
coherence
for b1 being Subset of FT st b1 = {x} holds
b1 is arcwise_connected by Lm3;
end;
theorem :: FINTOPO6:46
for FT being non empty RelStr
for A being Subset of FT st FT is symmetric holds
( A is connected iff A is arcwise_connected )
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st FT is symmetric holds
( A is connected iff A is arcwise_connected )
let A be Subset of FT; ::_thesis: ( FT is symmetric implies ( A is connected iff A is arcwise_connected ) )
assume A1: FT is symmetric ; ::_thesis: ( A is connected iff A is arcwise_connected )
now__::_thesis:_(_not_A_is_arcwise_connected_implies_not_A_is_connected_)
assume not A is arcwise_connected ; ::_thesis: not A is connected
then consider x1, x2 being Element of FT such that
A2: x1 in A and
A3: x2 in A and
A4: for f being FinSequence of FT holds
( not f is continuous or not rng f c= A or not f . 1 = x1 or not f . (len f) = x2 ) by Def7;
A5: { z where z is Element of FT : ( z in A & ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) } c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { z where z is Element of FT : ( z in A & ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) } or x in A )
assume x in { z where z is Element of FT : ( z in A & ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) } ; ::_thesis: x in A
then ex z being Element of FT st
( x = z & z in A & ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) ;
hence x in A ; ::_thesis: verum
end;
then reconsider G = { z where z is Element of FT : ( z in A & ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) } as Subset of FT by XBOOLE_1:1;
A6: G misses A \ G by XBOOLE_1:79;
A7: now__::_thesis:_not_G_^b_meets_A_\_G
assume G ^b meets A \ G ; ::_thesis: contradiction
then consider u being set such that
A8: u in G ^b and
A9: u in A \ G by XBOOLE_0:3;
A10: not u in G by A9, XBOOLE_0:def_5;
consider x being Element of FT such that
A11: u = x and
A12: U_FT x meets G by A8;
consider y being set such that
A13: y in U_FT x and
A14: y in G by A12, XBOOLE_0:3;
consider z2 being Element of FT such that
A15: y = z2 and
z2 in A and
A16: ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z2 ) by A14;
consider f being FinSequence of FT such that
A17: f is continuous and
A18: rng f c= A and
A19: f . 1 = x1 and
A20: f . (len f) = z2 by A16;
reconsider g = f ^ <*x*> as FinSequence of FT ;
A21: rng g = (rng f) \/ (rng <*x*>) by FINSEQ_1:31
.= (rng f) \/ {x} by FINSEQ_1:38 ;
A22: u in A by A9, XBOOLE_0:def_5;
then {x} c= A by A11, ZFMISC_1:31;
then A23: rng g c= A by A18, A21, XBOOLE_1:8;
1 <= len f by A17, Def6;
then 1 in dom f by FINSEQ_3:25;
then A24: ( g . ((len f) + 1) = x & g . 1 = x1 ) by A19, FINSEQ_1:42, FINSEQ_1:def_7;
x in U_FT z2 by A1, A13, A15, FIN_TOPO:def_13;
then A25: g is continuous by A17, A20, Th44;
len g = (len f) + (len <*x*>) by FINSEQ_1:22
.= (len f) + 1 by FINSEQ_1:39 ;
hence contradiction by A22, A10, A11, A25, A24, A23; ::_thesis: verum
end;
A26: now__::_thesis:_not_G_=_{}
{x1} c= A by A2, ZFMISC_1:31;
then A27: rng <*x1*> c= A by FINSEQ_1:38;
assume A28: G = {} ; ::_thesis: contradiction
A29: <*x1*> . 1 = x1 by FINSEQ_1:40;
then <*x1*> . (len <*x1*>) = x1 by FINSEQ_1:39;
then x1 in G by A2, A27, A29;
hence contradiction by A28; ::_thesis: verum
end;
A30: now__::_thesis:_not_A_\_G_=_{}
assume A \ G = {} ; ::_thesis: contradiction
then A c= G by XBOOLE_1:37;
then G = A by A5, XBOOLE_0:def_10;
then ex z being Element of FT st
( z = x2 & z in A & ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) by A3;
hence contradiction by A4; ::_thesis: verum
end;
A = G \/ (A \ G) by A5, XBOOLE_1:45;
hence not A is connected by A30, A26, A6, A7, FIN_TOPO:def_16; ::_thesis: verum
end;
hence ( A is connected implies A is arcwise_connected ) ; ::_thesis: ( A is arcwise_connected implies A is connected )
now__::_thesis:_(_not_A_is_connected_implies_(_not_A_is_arcwise_connected_&_not_A_is_arcwise_connected_)_)
assume not A is connected ; ::_thesis: ( not A is arcwise_connected & not A is arcwise_connected )
then consider P, Q being Subset of FT such that
A31: A = P \/ Q and
A32: P <> {} and
A33: Q <> {} and
A34: P misses Q and
A35: P ^b misses Q by FIN_TOPO:def_16;
set q0 = the Element of Q;
the Element of Q in Q by A33;
then reconsider q1 = the Element of Q as Element of FT ;
set p0 = the Element of P;
the Element of P in P by A32;
then reconsider p1 = the Element of P as Element of FT ;
A36: ( p1 in A & q1 in A ) by A31, A32, A33, XBOOLE_0:def_3;
hereby ::_thesis: not A is arcwise_connected
assume A is arcwise_connected ; ::_thesis: contradiction
then consider f being FinSequence of FT such that
A37: f is continuous and
A38: rng f c= A and
A39: f . 1 = p1 and
A40: f . (len f) = q1 by A36, Def7;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len f & f . $1 in P );
len f >= 1 by A37, Def6;
then A41: ex k being Nat st S1[k] by A32, A39;
A42: for k being Nat st S1[k] holds
k <= len f ;
consider i0 being Nat such that
A43: ( S1[i0] & ( for n being Nat st S1[n] holds
n <= i0 ) ) from NAT_1:sch_6(A42, A41);
i0 <> len f by A33, A34, A40, A43, XBOOLE_0:3;
then A44: i0 < len f by A43, XXREAL_0:1;
then A45: i0 + 1 <= len f by NAT_1:13;
reconsider u0 = f . i0 as Element of FT by A43;
A46: 1 < i0 + 1 by A43, NAT_1:13;
then i0 + 1 in dom f by A45, FINSEQ_3:25;
then A47: f . (i0 + 1) in rng f by FUNCT_1:def_3;
then reconsider z0 = f . (i0 + 1) as Element of FT ;
z0 in U_FT u0 by A37, A43, A44, Def6;
then f . i0 in U_FT z0 by A1, FIN_TOPO:def_13;
then U_FT z0 meets P by A43, XBOOLE_0:3;
then A48: z0 in P ^b ;
now__::_thesis:_not_f_._(i0_+_1)_in_P
assume f . (i0 + 1) in P ; ::_thesis: contradiction
then i0 + 1 <= i0 by A43, A45, A46;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
then f . (i0 + 1) in Q by A31, A38, A47, XBOOLE_0:def_3;
hence contradiction by A35, A48, XBOOLE_0:3; ::_thesis: verum
end;
hence not A is arcwise_connected ; ::_thesis: verum
end;
hence ( A is arcwise_connected implies A is connected ) ; ::_thesis: verum
end;
theorem Th47: :: FINTOPO6:47
for FT being non empty RelStr
for g being FinSequence of FT
for k being Nat st g is continuous & 1 <= k holds
g | k is continuous
proof
let FT be non empty RelStr ; ::_thesis: for g being FinSequence of FT
for k being Nat st g is continuous & 1 <= k holds
g | k is continuous
let g be FinSequence of FT; ::_thesis: for k being Nat st g is continuous & 1 <= k holds
g | k is continuous
let k be Nat; ::_thesis: ( g is continuous & 1 <= k implies g | k is continuous )
assume that
A1: g is continuous and
A2: 1 <= k ; ::_thesis: g | k is continuous
percases ( len g <= k or k <= len g ) ;
suppose len g <= k ; ::_thesis: g | k is continuous
hence g | k is continuous by A1, FINSEQ_1:58; ::_thesis: verum
end;
supposeA3: k <= len g ; ::_thesis: g | k is continuous
hence len (g | k) >= 1 by A2, FINSEQ_1:59; :: according to FINTOPO6:def_6 ::_thesis: for i being Nat
for x1 being Element of FT st 1 <= i & i < len (g | k) & x1 = (g | k) . i holds
(g | k) . (i + 1) in U_FT x1
let i be Nat; ::_thesis: for x1 being Element of FT st 1 <= i & i < len (g | k) & x1 = (g | k) . i holds
(g | k) . (i + 1) in U_FT x1
let x11 be Element of FT; ::_thesis: ( 1 <= i & i < len (g | k) & x11 = (g | k) . i implies (g | k) . (i + 1) in U_FT x11 )
assume that
A4: 1 <= i and
A5: i < len (g | k) and
A6: x11 = (g | k) . i ; ::_thesis: (g | k) . (i + 1) in U_FT x11
A7: len (g | k) = k by A3, FINSEQ_1:59;
then A8: (g | k) . i = g . i by A5, FINSEQ_3:112;
i + 1 <= k by A7, A5, NAT_1:13;
then A9: (g | k) . (i + 1) = g . (i + 1) by FINSEQ_3:112;
i < len g by A3, A7, A5, XXREAL_0:2;
hence (g | k) . (i + 1) in U_FT x11 by A1, A4, A6, A8, A9, Def6; ::_thesis: verum
end;
end;
end;
theorem Th48: :: FINTOPO6:48
for FT being non empty RelStr
for g being FinSequence of FT
for k being Element of NAT st g is continuous & k < len g holds
g /^ k is continuous
proof
let FT be non empty RelStr ; ::_thesis: for g being FinSequence of FT
for k being Element of NAT st g is continuous & k < len g holds
g /^ k is continuous
let g be FinSequence of FT; ::_thesis: for k being Element of NAT st g is continuous & k < len g holds
g /^ k is continuous
let k be Element of NAT ; ::_thesis: ( g is continuous & k < len g implies g /^ k is continuous )
assume that
A1: g is continuous and
A2: k < len g ; ::_thesis: g /^ k is continuous
A3: (len g) - k > 0 by A2, XREAL_1:50;
then A4: (len g) - k = (len g) -' k by XREAL_0:def_2;
A5: len (g /^ k) = (len g) - k by A2, RFINSEQ:def_1;
A6: for i being Nat
for x11 being Element of FT st 1 <= i & i < len (g /^ k) & x11 = (g /^ k) . i holds
(g /^ k) . (i + 1) in U_FT x11
proof
let i be Nat; ::_thesis: for x11 being Element of FT st 1 <= i & i < len (g /^ k) & x11 = (g /^ k) . i holds
(g /^ k) . (i + 1) in U_FT x11
let x11 be Element of FT; ::_thesis: ( 1 <= i & i < len (g /^ k) & x11 = (g /^ k) . i implies (g /^ k) . (i + 1) in U_FT x11 )
assume that
A7: 1 <= i and
A8: i < len (g /^ k) and
A9: x11 = (g /^ k) . i ; ::_thesis: (g /^ k) . (i + 1) in U_FT x11
A10: 1 <= 1 + i by NAT_1:11;
i in dom (g /^ k) by A7, A8, FINSEQ_3:25;
then A11: (g /^ k) . i = g . (i + k) by A2, RFINSEQ:def_1;
i <= i + k by NAT_1:11;
then A12: ( (i + 1) + k = (i + k) + 1 & 1 <= i + k ) by A7, XXREAL_0:2;
i + 1 <= (len g) -' k by A5, A4, A8, NAT_1:13;
then i + 1 in dom (g /^ k) by A5, A4, A10, FINSEQ_3:25;
then A13: (g /^ k) . (i + 1) = g . ((i + 1) + k) by A2, RFINSEQ:def_1;
i + k < ((len g) - k) + k by A5, A8, XREAL_1:6;
hence (g /^ k) . (i + 1) in U_FT x11 by A1, A9, A11, A13, A12, Def6; ::_thesis: verum
end;
(len g) -' k >= 0 + 1 by A3, A4, NAT_1:13;
hence g /^ k is continuous by A5, A4, A6, Def6; ::_thesis: verum
end;
definition
let FT be non empty RelStr ;
let g be FinSequence of FT;
let A be Subset of FT;
let x1, x2 be Element of FT;
predg is_minimum_path_in A,x1,x2 means :Def8: :: FINTOPO6:def 8
( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds
len g <= len h ) );
end;
:: deftheorem Def8 defines is_minimum_path_in FINTOPO6:def_8_:_
for FT being non empty RelStr
for g being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT holds
( g is_minimum_path_in A,x1,x2 iff ( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds
len g <= len h ) ) );
theorem :: FINTOPO6:49
for FT being non empty RelStr
for A being Subset of FT
for x being Element of FT st x in A holds
<*x*> is_minimum_path_in A,x,x
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT
for x being Element of FT st x in A holds
<*x*> is_minimum_path_in A,x,x
let A be Subset of FT; ::_thesis: for x being Element of FT st x in A holds
<*x*> is_minimum_path_in A,x,x
let x be Element of FT; ::_thesis: ( x in A implies <*x*> is_minimum_path_in A,x,x )
assume A1: x in A ; ::_thesis: <*x*> is_minimum_path_in A,x,x
thus <*x*> is continuous ; :: according to FINTOPO6:def_8 ::_thesis: ( rng <*x*> c= A & <*x*> . 1 = x & <*x*> . (len <*x*>) = x & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x & h . (len h) = x holds
len <*x*> <= len h ) )
{x} c= A by A1, ZFMISC_1:31;
hence rng <*x*> c= A by FINSEQ_1:38; ::_thesis: ( <*x*> . 1 = x & <*x*> . (len <*x*>) = x & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x & h . (len h) = x holds
len <*x*> <= len h ) )
len <*x*> = 1 by FINSEQ_1:40;
hence ( <*x*> . 1 = x & <*x*> . (len <*x*>) = x & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x & h . (len h) = x holds
len <*x*> <= len h ) ) by Def6, FINSEQ_1:40; ::_thesis: verum
end;
Lm4: for FT being non empty RelStr
for f being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT st f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 holds
ex g being FinSequence of FT st
( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds
len g <= len h ) )
proof
let FT be non empty RelStr ; ::_thesis: for f being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT st f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 holds
ex g being FinSequence of FT st
( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds
len g <= len h ) )
let f be FinSequence of FT; ::_thesis: for A being Subset of FT
for x1, x2 being Element of FT st f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 holds
ex g being FinSequence of FT st
( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds
len g <= len h ) )
let A be Subset of FT; ::_thesis: for x1, x2 being Element of FT st f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 holds
ex g being FinSequence of FT st
( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds
len g <= len h ) )
let x1, x2 be Element of FT; ::_thesis: ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 implies ex g being FinSequence of FT st
( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds
len g <= len h ) ) )
defpred S1[ Nat] means ex g being FinSequence of FT st
( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & $1 = len g );
assume ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) ; ::_thesis: ex g being FinSequence of FT st
( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds
len g <= len h ) )
then A1: ex k being Nat st S1[k] ;
ex k being Nat st
( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from NAT_1:sch_5(A1);
then consider k0 being Nat such that
A2: S1[k0] and
A3: for n being Nat st S1[n] holds
k0 <= n ;
consider g0 being FinSequence of FT such that
A4: ( g0 is continuous & rng g0 c= A & g0 . 1 = x1 & g0 . (len g0) = x2 ) and
A5: k0 = len g0 by A2;
for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds
len g0 <= len h by A3, A5;
hence ex g being FinSequence of FT st
( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds
len g <= len h ) ) by A4; ::_thesis: verum
end;
theorem :: FINTOPO6:50
for FT being non empty RelStr
for A being Subset of FT holds
( A is arcwise_connected iff for x1, x2 being Element of FT st x1 in A & x2 in A holds
ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 )
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds
( A is arcwise_connected iff for x1, x2 being Element of FT st x1 in A & x2 in A holds
ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 )
let A be Subset of FT; ::_thesis: ( A is arcwise_connected iff for x1, x2 being Element of FT st x1 in A & x2 in A holds
ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 )
thus ( A is arcwise_connected implies for x1, x2 being Element of FT st x1 in A & x2 in A holds
ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ) ::_thesis: ( ( for x1, x2 being Element of FT st x1 in A & x2 in A holds
ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ) implies A is arcwise_connected )
proof
assume A1: A is arcwise_connected ; ::_thesis: for x1, x2 being Element of FT st x1 in A & x2 in A holds
ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2
thus for x1, x2 being Element of FT st x1 in A & x2 in A holds
ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ::_thesis: verum
proof
let x1, x2 be Element of FT; ::_thesis: ( x1 in A & x2 in A implies ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 )
assume ( x1 in A & x2 in A ) ; ::_thesis: ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2
then ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) by A1, Def7;
then consider g2 being FinSequence of FT such that
A2: ( g2 is continuous & rng g2 c= A & g2 . 1 = x1 & g2 . (len g2) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds
len g2 <= len h ) ) by Lm4;
g2 is_minimum_path_in A,x1,x2 by A2, Def8;
hence ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ; ::_thesis: verum
end;
end;
assume A3: for x1, x2 being Element of FT st x1 in A & x2 in A holds
ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ; ::_thesis: A is arcwise_connected
for x1, x2 being Element of FT st x1 in A & x2 in A holds
ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 )
proof
let x1, x2 be Element of FT; ::_thesis: ( x1 in A & x2 in A implies ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) )
assume ( x1 in A & x2 in A ) ; ::_thesis: ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 )
then consider g being FinSequence of FT such that
A4: g is_minimum_path_in A,x1,x2 by A3;
A5: ( g . 1 = x1 & g . (len g) = x2 ) by A4, Def8;
( g is continuous & rng g c= A ) by A4, Def8;
hence ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) by A5; ::_thesis: verum
end;
hence A is arcwise_connected by Def7; ::_thesis: verum
end;
theorem :: FINTOPO6:51
for FT being non empty RelStr
for A being Subset of FT
for x1, x2 being Element of FT st ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) holds
ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT
for x1, x2 being Element of FT st ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) holds
ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2
let A be Subset of FT; ::_thesis: for x1, x2 being Element of FT st ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) holds
ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2
let x1, x2 be Element of FT; ::_thesis: ( ex f being FinSequence of FT st
( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) implies ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 )
given f being FinSequence of FT such that A1: ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) ; ::_thesis: ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2
consider g2 being FinSequence of FT such that
A2: ( g2 is continuous & rng g2 c= A & g2 . 1 = x1 & g2 . (len g2) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds
len g2 <= len h ) ) by A1, Lm4;
g2 is_minimum_path_in A,x1,x2 by A2, Def8;
hence ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ; ::_thesis: verum
end;
theorem Th52: :: FINTOPO6:52
for FT being non empty RelStr
for g being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT
for k being Element of NAT st g is_minimum_path_in A,x1,x2 & 1 <= k & k <= len g holds
( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )
proof
let FT be non empty RelStr ; ::_thesis: for g being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT
for k being Element of NAT st g is_minimum_path_in A,x1,x2 & 1 <= k & k <= len g holds
( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )
let g be FinSequence of FT; ::_thesis: for A being Subset of FT
for x1, x2 being Element of FT
for k being Element of NAT st g is_minimum_path_in A,x1,x2 & 1 <= k & k <= len g holds
( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )
let A be Subset of FT; ::_thesis: for x1, x2 being Element of FT
for k being Element of NAT st g is_minimum_path_in A,x1,x2 & 1 <= k & k <= len g holds
( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )
let x1, x2 be Element of FT; ::_thesis: for k being Element of NAT st g is_minimum_path_in A,x1,x2 & 1 <= k & k <= len g holds
( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )
let k be Element of NAT ; ::_thesis: ( g is_minimum_path_in A,x1,x2 & 1 <= k & k <= len g implies ( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k ) )
assume that
A1: g is_minimum_path_in A,x1,x2 and
A2: 1 <= k and
A3: k <= len g ; ::_thesis: ( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )
A4: k in dom g by A2, A3, FINSEQ_3:25;
g is continuous by A1, Def8;
hence g | k is continuous by A2, Th47; ::_thesis: ( rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )
A5: rng (g | k) c= rng g by FINSEQ_5:19;
rng g c= A by A1, Def8;
hence rng (g | k) c= A by A5, XBOOLE_1:1; ::_thesis: ( (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k )
g . 1 = x1 by A1, Def8;
hence (g | k) . 1 = x1 by A2, FINSEQ_3:112; ::_thesis: (g | k) . (len (g | k)) = g /. k
len (g | k) = k by A3, FINSEQ_1:59;
hence (g | k) . (len (g | k)) = g . k by FINSEQ_3:112
.= g /. k by A4, PARTFUN1:def_6 ;
::_thesis: verum
end;
theorem Th53: :: FINTOPO6:53
for FT being non empty RelStr
for g being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT
for k being Element of NAT st g is_minimum_path_in A,x1,x2 & k < len g holds
( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 )
proof
let FT be non empty RelStr ; ::_thesis: for g being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT
for k being Element of NAT st g is_minimum_path_in A,x1,x2 & k < len g holds
( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 )
let g be FinSequence of FT; ::_thesis: for A being Subset of FT
for x1, x2 being Element of FT
for k being Element of NAT st g is_minimum_path_in A,x1,x2 & k < len g holds
( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 )
let A be Subset of FT; ::_thesis: for x1, x2 being Element of FT
for k being Element of NAT st g is_minimum_path_in A,x1,x2 & k < len g holds
( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 )
let x1, x2 be Element of FT; ::_thesis: for k being Element of NAT st g is_minimum_path_in A,x1,x2 & k < len g holds
( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 )
let k be Element of NAT ; ::_thesis: ( g is_minimum_path_in A,x1,x2 & k < len g implies ( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 ) )
assume that
A1: g is_minimum_path_in A,x1,x2 and
A2: k < len g ; ::_thesis: ( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 )
A3: len (g /^ k) = (len g) - k by A2, RFINSEQ:def_1;
g is continuous by A1, Def8;
hence g /^ k is continuous by A2, Th48; ::_thesis: ( rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 )
A4: rng (g /^ k) c= rng g by FINSEQ_5:33;
rng g c= A by A1, Def8;
hence rng (g /^ k) c= A by A4, XBOOLE_1:1; ::_thesis: ( (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 )
A5: len (g /^ k) = (len g) - k by A2, RFINSEQ:def_1;
( 1 <= 1 + k & k + 1 <= len g ) by A2, NAT_1:11, NAT_1:13;
then A6: 1 + k in dom g by FINSEQ_3:25;
A7: (len g) - k > 0 by A2, XREAL_1:50;
then (len g) -' k = (len g) - k by XREAL_0:def_2;
then (len g) - k >= 0 + 1 by A7, NAT_1:13;
then 1 in dom (g /^ k) by A5, FINSEQ_3:25;
hence (g /^ k) . 1 = g . (1 + k) by A2, RFINSEQ:def_1
.= g /. (1 + k) by A6, PARTFUN1:def_6 ;
::_thesis: (g /^ k) . (len (g /^ k)) = x2
A8: (len g) - k > 0 by A2, XREAL_1:50;
then A9: (len g) - k = (len g) -' k by XREAL_0:def_2;
then (len g) -' k >= 0 + 1 by A8, NAT_1:13;
then (len g) -' k in dom (g /^ k) by A5, A9, FINSEQ_3:25;
hence (g /^ k) . (len (g /^ k)) = g . (((len g) -' k) + k) by A2, A9, A3, RFINSEQ:def_1
.= x2 by A1, A9, Def8 ;
::_thesis: verum
end;
theorem :: FINTOPO6:54
for FT being non empty RelStr
for g being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds
for k being Nat st 1 <= k & k <= len g holds
g | k is_minimum_path_in A,x1,g /. k
proof
let FT be non empty RelStr ; ::_thesis: for g being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds
for k being Nat st 1 <= k & k <= len g holds
g | k is_minimum_path_in A,x1,g /. k
let g be FinSequence of FT; ::_thesis: for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds
for k being Nat st 1 <= k & k <= len g holds
g | k is_minimum_path_in A,x1,g /. k
let A be Subset of FT; ::_thesis: for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds
for k being Nat st 1 <= k & k <= len g holds
g | k is_minimum_path_in A,x1,g /. k
let x1, x2 be Element of FT; ::_thesis: ( g is_minimum_path_in A,x1,x2 implies for k being Nat st 1 <= k & k <= len g holds
g | k is_minimum_path_in A,x1,g /. k )
assume A1: g is_minimum_path_in A,x1,x2 ; ::_thesis: for k being Nat st 1 <= k & k <= len g holds
g | k is_minimum_path_in A,x1,g /. k
then A2: rng g c= A by Def8;
A3: g is continuous by A1, Def8;
then A4: 1 <= len g by Def6;
A5: g . (len g) = x2 by A1, Def8;
let k be Nat; ::_thesis: ( 1 <= k & k <= len g implies g | k is_minimum_path_in A,x1,g /. k )
assume that
A6: 1 <= k and
A7: k <= len g ; ::_thesis: g | k is_minimum_path_in A,x1,g /. k
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A8: ( (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k ) by A1, A6, A7, Th52;
A9: ( g | k is continuous & rng (g | k) c= A ) by A1, A6, A7, Th52;
now__::_thesis:_g_|_k_is_minimum_path_in_A,x1,g_/._k
percases ( k < len g or k = len g ) by A7, XXREAL_0:1;
supposeA10: k < len g ; ::_thesis: g | k is_minimum_path_in A,x1,g /. k
now__::_thesis:_g_|_k_is_minimum_path_in_A,x1,g_/._k
k in dom g by A6, A7, FINSEQ_3:25;
then A11: g /. k = g . k by PARTFUN1:def_6;
k + 1 <= len g by A10, NAT_1:13;
then A12: (g /^ k) . 1 = g . (k + 1) by FINSEQ_6:114;
rng (g /^ k) c= rng g by FINSEQ_5:33;
then A13: rng (g /^ k) c= A by A2, XBOOLE_1:1;
assume not g | k is_minimum_path_in A,x1,g /. k ; ::_thesis: contradiction
then consider h being FinSequence of FT such that
A14: h is continuous and
A15: rng h c= A and
A16: h . 1 = x1 and
A17: h . (len h) = g /. k and
A18: len (g | k) > len h by A9, A8, Def8;
reconsider s = h ^ (g /^ k) as FinSequence of FT ;
A19: len s = (len h) + (len (g /^ k)) by FINSEQ_1:22;
rng s = (rng h) \/ (rng (g /^ k)) by FINSEQ_1:31;
then A20: rng s c= A by A15, A13, XBOOLE_1:8;
A21: g /^ k is continuous by A1, A10, Th53;
then 1 <= len (g /^ k) by Def6;
then len (g /^ k) in dom (g /^ k) by FINSEQ_3:25;
then A22: s . (len s) = (g /^ k) . (len (g /^ k)) by A19, FINSEQ_1:def_7
.= x2 by A5, A10, JORDAN4:6 ;
A23: 1 <= len h by A14, Def6;
then 1 in dom h by FINSEQ_3:25;
then A24: s . 1 = x1 by A16, FINSEQ_1:def_7;
len h in dom h by A23, FINSEQ_3:25;
then h . (len h) = h /. (len h) by PARTFUN1:def_6;
then (g /^ k) . 1 in U_FT (h /. (len h)) by A3, A6, A10, A17, A12, A11, Def6;
then A25: s is continuous by A14, A21, Th45;
g = (g | k) ^ (g /^ k) by RFINSEQ:8;
then len g = (len (g | k)) + (len (g /^ k)) by FINSEQ_1:22;
then len s < len g by A18, A19, XREAL_1:8;
hence contradiction by A1, A25, A20, A24, A22, Def8; ::_thesis: verum
end;
hence g | k is_minimum_path_in A,x1,g /. k ; ::_thesis: verum
end;
supposeA26: k = len g ; ::_thesis: g | k is_minimum_path_in A,x1,g /. k
A27: len g in dom g by A4, FINSEQ_3:25;
g | k = g by A26, FINSEQ_1:58;
hence g | k is_minimum_path_in A,x1,g /. k by A1, A5, A26, A27, PARTFUN1:def_6; ::_thesis: verum
end;
end;
end;
hence g | k is_minimum_path_in A,x1,g /. k ; ::_thesis: verum
end;
theorem :: FINTOPO6:55
for FT being non empty RelStr
for g being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds
g is one-to-one
proof
let FT be non empty RelStr ; ::_thesis: for g being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds
g is one-to-one
let g be FinSequence of FT; ::_thesis: for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds
g is one-to-one
let A be Subset of FT; ::_thesis: for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds
g is one-to-one
let x1, x2 be Element of FT; ::_thesis: ( g is_minimum_path_in A,x1,x2 implies g is one-to-one )
assume A1: g is_minimum_path_in A,x1,x2 ; ::_thesis: g is one-to-one
then A2: g is continuous by Def8;
A3: for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds
len g <= len h by A1, Def8;
A4: rng g c= A by A1, Def8;
A5: g . 1 = x1 by A1, Def8;
A6: g . (len g) = x2 by A1, Def8;
assume not g is one-to-one ; ::_thesis: contradiction
then consider y1, y2 being set such that
A7: y1 in dom g and
A8: y2 in dom g and
A9: g . y1 = g . y2 and
A10: y1 <> y2 by FUNCT_1:def_4;
reconsider n1 = y1, n2 = y2 as Element of NAT by A7, A8;
A11: dom g = Seg (len g) by FINSEQ_1:def_3;
then A12: 1 <= n1 by A7, FINSEQ_1:1;
A13: n2 <= len g by A8, A11, FINSEQ_1:1;
A14: 1 <= n2 by A8, A11, FINSEQ_1:1;
A15: n1 <= len g by A7, A11, FINSEQ_1:1;
percases ( n1 > n2 or n2 > n1 ) by A10, XXREAL_0:1;
supposeA16: n1 > n2 ; ::_thesis: contradiction
set k = (len g) -' n1;
set g2 = (g | n2) ^ (g /^ n1);
A17: len (g /^ n1) = (len g) - n1 by A15, RFINSEQ:def_1;
A18: (len g) - n1 >= 0 by A15, XREAL_1:48;
then A19: (len g) -' n1 = (len g) - n1 by XREAL_0:def_2;
A20: len (g | n2) = n2 by A13, FINSEQ_1:59;
then A21: ((g | n2) ^ (g /^ n1)) . 1 = (g | n2) . 1 by A14, FINSEQ_1:64
.= g . 1 by A14, FINSEQ_3:112 ;
A22: len ((g | n2) ^ (g /^ n1)) = (len (g | n2)) + (len (g /^ n1)) by FINSEQ_1:22
.= n2 + ((len g) - n1) by A15, A20, RFINSEQ:def_1 ;
percases ( n1 < len g or n1 = len g ) by A15, XXREAL_0:1;
suppose n1 < len g ; ::_thesis: contradiction
then n1 + 1 <= len g by NAT_1:13;
then A23: (n1 + 1) - n1 <= (len g) - n1 by XREAL_1:13;
then A24: 0 + 1 <= n2 + ((len g) - n1) by XREAL_1:7;
A25: (g | n2) ^ (g /^ n1) is continuous
proof
thus len ((g | n2) ^ (g /^ n1)) >= 1 by A22, A24; :: according to FINTOPO6:def_6 ::_thesis: for i being Nat
for x1 being Element of FT st 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & x1 = ((g | n2) ^ (g /^ n1)) . i holds
((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT x1
let i be Nat; ::_thesis: for x1 being Element of FT st 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & x1 = ((g | n2) ^ (g /^ n1)) . i holds
((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT x1
let z1 be Element of FT; ::_thesis: ( 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & z1 = ((g | n2) ^ (g /^ n1)) . i implies ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 )
assume that
A26: 1 <= i and
A27: i < len ((g | n2) ^ (g /^ n1)) and
A28: z1 = ((g | n2) ^ (g /^ n1)) . i ; ::_thesis: ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1
A29: i + 1 <= len ((g | n2) ^ (g /^ n1)) by A27, NAT_1:13;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
1 < i + 1 by A26, NAT_1:13;
then i + 1 in dom ((g | n2) ^ (g /^ n1)) by A29, FINSEQ_3:25;
then ((g | n2) ^ (g /^ n1)) . (i + 1) = ((g | n2) ^ (g /^ n1)) /. (i + 1) by PARTFUN1:def_6;
then reconsider z2 = ((g | n2) ^ (g /^ n1)) . (i + 1) as Element of FT ;
now__::_thesis:_z2_in_U_FT_z1
percases ( i < n2 or i >= n2 ) ;
supposeA30: i < n2 ; ::_thesis: z2 in U_FT z1
then A31: i + 1 <= n2 by NAT_1:13;
i + 1 <= len (g | n2) by A20, A30, NAT_1:13;
then A32: z2 = (g | n2) . (i + 1) by FINSEQ_1:64, NAT_1:12
.= g . (i + 1) by A31, FINSEQ_3:112 ;
A33: i < len g by A13, A30, XXREAL_0:2;
z1 = (g | n2) . i by A20, A26, A28, A30, FINSEQ_1:64
.= g . i by A30, FINSEQ_3:112 ;
hence z2 in U_FT z1 by A2, A26, A33, A32, Def6; ::_thesis: verum
end;
supposeA34: i >= n2 ; ::_thesis: z2 in U_FT z1
i - n2 < (n2 + ((len g) - n1)) - n2 by A22, A27, XREAL_1:9;
then A35: i -' n2 < (len g) - n1 by A34, XREAL_1:233;
then A36: (i -' n2) + n1 < ((len g) - n1) + n1 by XREAL_1:6;
A37: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by A20, A34, XREAL_1:233
.= i ;
A38: now__::_thesis:_z1_=_g_._((i_-'_n2)_+_n1)
percases ( i > n2 or i = n2 ) by A34, XXREAL_0:1;
suppose i > n2 ; ::_thesis: z1 = g . ((i -' n2) + n1)
then A39: i - n2 > 0 by XREAL_1:50;
then i -' n2 = i - n2 by XREAL_0:def_2;
then A40: 0 + 1 <= i -' n2 by A39, NAT_1:13;
then A41: i -' n2 in dom (g /^ n1) by A17, A35, FINSEQ_3:25;
thus z1 = (g /^ n1) . (i -' n2) by A17, A28, A35, A37, A40, FINSEQ_1:65
.= g . ((i -' n2) + n1) by A15, A41, RFINSEQ:def_1 ; ::_thesis: verum
end;
supposeA42: i = n2 ; ::_thesis: z1 = g . ((i -' n2) + n1)
hence z1 = (g | n2) . n2 by A20, A26, A28, FINSEQ_1:64
.= g . (0 + n1) by A9, FINSEQ_3:112
.= g . ((i -' n2) + n1) by A42, XREAL_1:232 ;
::_thesis: verum
end;
end;
end;
i -' n2 < (len g) -' n1 by A15, A35, XREAL_1:233;
then (i -' n2) + 1 <= (len g) -' n1 by NAT_1:13;
then A43: (i -' n2) + 1 <= len (g /^ n1) by A15, A17, XREAL_1:233;
1 <= (i -' n2) + 1 by NAT_1:12;
then A44: (i -' n2) + 1 in dom (g /^ n1) by A43, FINSEQ_3:25;
(len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by A20, A34, XREAL_1:233
.= i + 1 ;
then A45: z2 = (g /^ n1) . ((i -' n2) + 1) by A43, FINSEQ_1:65, NAT_1:12
.= g . (((i -' n2) + 1) + n1) by A15, A44, RFINSEQ:def_1
.= g . (((i -' n2) + n1) + 1) ;
1 <= (i -' n2) + n1 by A12, NAT_1:12;
hence z2 in U_FT z1 by A2, A38, A45, A36, Def6; ::_thesis: verum
end;
end;
end;
hence ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 ; ::_thesis: verum
end;
A46: rng (g /^ n1) c= rng g by FINSEQ_5:33;
( rng ((g | n2) ^ (g /^ n1)) = (rng (g | n2)) \/ (rng (g /^ n1)) & rng (g | n2) c= rng g ) by FINSEQ_1:31, FINSEQ_5:19;
then A47: rng ((g | n2) ^ (g /^ n1)) c= rng g by A46, XBOOLE_1:8;
A48: ((len g) -' n1) + n1 = len g by A19;
A49: (len g) -' n1 in dom (g /^ n1) by A19, A17, A23, FINSEQ_3:25;
then ((g | n2) ^ (g /^ n1)) . ((len (g | n2)) + ((len g) -' n1)) = (g /^ n1) . ((len g) -' n1) by FINSEQ_1:def_7
.= x2 by A6, A15, A49, A48, RFINSEQ:def_1 ;
then ((g | n2) ^ (g /^ n1)) . (len ((g | n2) ^ (g /^ n1))) = x2 by A20, A22, A18, XREAL_0:def_2;
then len g <= len ((g | n2) ^ (g /^ n1)) by A4, A5, A3, A21, A47, A25, XBOOLE_1:1;
then (len g) - n2 <= (n2 + ((len g) - n1)) - n2 by A22, XREAL_1:13;
hence contradiction by A16, XREAL_1:10; ::_thesis: verum
end;
supposeA50: n1 = len g ; ::_thesis: contradiction
A51: len (g /^ n1) = (len g) - n1 by A15, RFINSEQ:def_1;
A52: (g | n2) ^ (g /^ n1) is continuous
proof
thus 1 <= len ((g | n2) ^ (g /^ n1)) by A8, A11, A22, A50, FINSEQ_1:1; :: according to FINTOPO6:def_6 ::_thesis: for i being Nat
for x1 being Element of FT st 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & x1 = ((g | n2) ^ (g /^ n1)) . i holds
((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT x1
let i be Nat; ::_thesis: for x1 being Element of FT st 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & x1 = ((g | n2) ^ (g /^ n1)) . i holds
((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT x1
let z1 be Element of FT; ::_thesis: ( 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & z1 = ((g | n2) ^ (g /^ n1)) . i implies ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 )
assume that
A53: 1 <= i and
A54: i < len ((g | n2) ^ (g /^ n1)) and
A55: z1 = ((g | n2) ^ (g /^ n1)) . i ; ::_thesis: ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1
A56: i + 1 <= len ((g | n2) ^ (g /^ n1)) by A54, NAT_1:13;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
1 < i + 1 by A53, NAT_1:13;
then i + 1 in dom ((g | n2) ^ (g /^ n1)) by A56, FINSEQ_3:25;
then ((g | n2) ^ (g /^ n1)) . (i + 1) = ((g | n2) ^ (g /^ n1)) /. (i + 1) by PARTFUN1:def_6;
then reconsider z2 = ((g | n2) ^ (g /^ n1)) . (i + 1) as Element of FT ;
percases ( i < n2 or i >= n2 ) ;
supposeA57: i < n2 ; ::_thesis: ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1
then A58: i + 1 <= n2 by NAT_1:13;
i + 1 <= len (g | n2) by A20, A57, NAT_1:13;
then A59: z2 = (g | n2) . (i + 1) by FINSEQ_1:64, NAT_1:12
.= g . (i + 1) by A58, FINSEQ_3:112 ;
A60: i < len g by A13, A57, XXREAL_0:2;
z1 = (g | n2) . i by A20, A53, A55, A57, FINSEQ_1:64
.= g . i by A57, FINSEQ_3:112 ;
hence ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 by A2, A53, A60, A59, Def6; ::_thesis: verum
end;
supposeA61: i >= n2 ; ::_thesis: ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1
i - n2 < (n2 + ((len g) - n1)) - n2 by A22, A54, XREAL_1:9;
then A62: i -' n2 < (len g) - n1 by A61, XREAL_1:233;
then A63: (i -' n2) + n1 < ((len g) - n1) + n1 by XREAL_1:6;
A64: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by A20, A61, XREAL_1:233
.= i ;
A65: now__::_thesis:_z1_=_g_._((i_-'_n2)_+_n1)
percases ( i > n2 or i = n2 ) by A61, XXREAL_0:1;
suppose i > n2 ; ::_thesis: z1 = g . ((i -' n2) + n1)
then A66: i - n2 > 0 by XREAL_1:50;
then i -' n2 = i - n2 by XREAL_0:def_2;
then A67: 0 + 1 <= i -' n2 by A66, NAT_1:13;
then A68: i -' n2 in dom (g /^ n1) by A51, A62, FINSEQ_3:25;
thus z1 = (g /^ n1) . (i -' n2) by A51, A55, A62, A64, A67, FINSEQ_1:65
.= g . ((i -' n2) + n1) by A15, A68, RFINSEQ:def_1 ; ::_thesis: verum
end;
supposeA69: i = n2 ; ::_thesis: z1 = g . ((i -' n2) + n1)
hence z1 = (g | n2) . n2 by A20, A53, A55, FINSEQ_1:64
.= g . (0 + n1) by A9, FINSEQ_3:112
.= g . ((i -' n2) + n1) by A69, XREAL_1:232 ;
::_thesis: verum
end;
end;
end;
i -' n2 < (len g) -' n1 by A15, A62, XREAL_1:233;
then (i -' n2) + 1 <= (len g) -' n1 by NAT_1:13;
then A70: (i -' n2) + 1 <= len (g /^ n1) by A15, A51, XREAL_1:233;
1 <= (i -' n2) + 1 by NAT_1:12;
then A71: (i -' n2) + 1 in dom (g /^ n1) by A70, FINSEQ_3:25;
(len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by A20, A61, XREAL_1:233
.= i + 1 ;
then A72: z2 = (g /^ n1) . ((i -' n2) + 1) by A70, FINSEQ_1:65, NAT_1:12
.= g . (((i -' n2) + 1) + n1) by A15, A71, RFINSEQ:def_1
.= g . (((i -' n2) + n1) + 1) ;
1 <= (i -' n2) + n1 by A12, NAT_1:12;
hence ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 by A2, A65, A72, A63, Def6; ::_thesis: verum
end;
end;
end;
A73: rng (g | n2) c= rng g by FINSEQ_5:19;
A74: (g | n2) ^ (g /^ n1) = (g | n2) ^ {} by A50, REVROT_1:2
.= g | n2 by FINSEQ_1:34 ;
then ((g | n2) ^ (g /^ n1)) . (len ((g | n2) ^ (g /^ n1))) = x2 by A6, A9, A20, A50, FINSEQ_3:112;
then len g <= len ((g | n2) ^ (g /^ n1)) by A4, A5, A3, A21, A74, A73, A52, XBOOLE_1:1;
then (len g) - n2 <= (n2 + ((len g) - n1)) - n2 by A22, XREAL_1:13;
hence contradiction by A16, XREAL_1:10; ::_thesis: verum
end;
end;
end;
supposeA75: n2 > n1 ; ::_thesis: contradiction
set k = (len g) -' n2;
set g2 = (g | n1) ^ (g /^ n2);
A76: len (g /^ n2) = (len g) - n2 by A13, RFINSEQ:def_1;
(len g) - n2 >= 0 by A13, XREAL_1:48;
then A77: (len g) -' n2 = (len g) - n2 by XREAL_0:def_2;
A78: len (g | n1) = n1 by A15, FINSEQ_1:59;
then A79: ((g | n1) ^ (g /^ n2)) . 1 = (g | n1) . 1 by A12, FINSEQ_1:64
.= x1 by A5, A12, FINSEQ_3:112 ;
A80: len ((g | n1) ^ (g /^ n2)) = (len (g | n1)) + (len (g /^ n2)) by FINSEQ_1:22
.= n1 + ((len g) - n2) by A13, A78, RFINSEQ:def_1 ;
percases ( n2 < len g or n2 = len g ) by A13, XXREAL_0:1;
suppose n2 < len g ; ::_thesis: contradiction
then n2 + 1 <= len g by NAT_1:13;
then A81: (n2 + 1) - n2 <= (len g) - n2 by XREAL_1:13;
then A82: 0 + 1 <= n1 + ((len g) - n2) by XREAL_1:7;
A83: (g | n1) ^ (g /^ n2) is continuous
proof
thus len ((g | n1) ^ (g /^ n2)) >= 1 by A80, A82; :: according to FINTOPO6:def_6 ::_thesis: for i being Nat
for x1 being Element of FT st 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & x1 = ((g | n1) ^ (g /^ n2)) . i holds
((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT x1
let i be Nat; ::_thesis: for x1 being Element of FT st 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & x1 = ((g | n1) ^ (g /^ n2)) . i holds
((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT x1
let z1 be Element of FT; ::_thesis: ( 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & z1 = ((g | n1) ^ (g /^ n2)) . i implies ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 )
assume that
A84: 1 <= i and
A85: i < len ((g | n1) ^ (g /^ n2)) and
A86: z1 = ((g | n1) ^ (g /^ n2)) . i ; ::_thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1
A87: i + 1 <= len ((g | n1) ^ (g /^ n2)) by A85, NAT_1:13;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
1 < i + 1 by A84, NAT_1:13;
then i + 1 in dom ((g | n1) ^ (g /^ n2)) by A87, FINSEQ_3:25;
then ((g | n1) ^ (g /^ n2)) . (i + 1) = ((g | n1) ^ (g /^ n2)) /. (i + 1) by PARTFUN1:def_6;
then reconsider z2 = ((g | n1) ^ (g /^ n2)) . (i + 1) as Element of FT ;
percases ( i < n1 or i >= n1 ) ;
supposeA88: i < n1 ; ::_thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1
then A89: i + 1 <= n1 by NAT_1:13;
i + 1 <= len (g | n1) by A78, A88, NAT_1:13;
then A90: z2 = (g | n1) . (i + 1) by FINSEQ_1:64, NAT_1:12
.= g . (i + 1) by A89, FINSEQ_3:112 ;
A91: i < len g by A15, A88, XXREAL_0:2;
z1 = (g | n1) . i by A78, A84, A86, A88, FINSEQ_1:64
.= g . i by A88, FINSEQ_3:112 ;
hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by A2, A84, A91, A90, Def6; ::_thesis: verum
end;
supposeA92: i >= n1 ; ::_thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1
i - n1 < (n1 + ((len g) - n2)) - n1 by A80, A85, XREAL_1:9;
then A93: i -' n1 < (len g) - n2 by A92, XREAL_1:233;
then A94: (i -' n1) + n2 < ((len g) - n2) + n2 by XREAL_1:6;
A95: (len (g | n1)) + (i -' n1) = n1 + (i - n1) by A78, A92, XREAL_1:233
.= i ;
A96: now__::_thesis:_z1_=_g_._((i_-'_n1)_+_n2)
percases ( i > n1 or i = n1 ) by A92, XXREAL_0:1;
suppose i > n1 ; ::_thesis: z1 = g . ((i -' n1) + n2)
then A97: i - n1 > 0 by XREAL_1:50;
then i -' n1 = i - n1 by XREAL_0:def_2;
then A98: 0 + 1 <= i -' n1 by A97, NAT_1:13;
then A99: i -' n1 in dom (g /^ n2) by A76, A93, FINSEQ_3:25;
thus z1 = (g /^ n2) . (i -' n1) by A76, A86, A93, A95, A98, FINSEQ_1:65
.= g . ((i -' n1) + n2) by A13, A99, RFINSEQ:def_1 ; ::_thesis: verum
end;
supposeA100: i = n1 ; ::_thesis: z1 = g . ((i -' n1) + n2)
hence z1 = (g | n1) . n1 by A78, A84, A86, FINSEQ_1:64
.= g . (0 + n2) by A9, FINSEQ_3:112
.= g . ((i -' n1) + n2) by A100, XREAL_1:232 ;
::_thesis: verum
end;
end;
end;
i -' n1 < (len g) -' n2 by A13, A93, XREAL_1:233;
then (i -' n1) + 1 <= (len g) -' n2 by NAT_1:13;
then A101: (i -' n1) + 1 <= len (g /^ n2) by A13, A76, XREAL_1:233;
1 <= (i -' n1) + 1 by NAT_1:12;
then A102: (i -' n1) + 1 in dom (g /^ n2) by A101, FINSEQ_3:25;
(len (g | n1)) + ((i -' n1) + 1) = ((i - n1) + 1) + n1 by A78, A92, XREAL_1:233
.= i + 1 ;
then A103: z2 = (g /^ n2) . ((i -' n1) + 1) by A101, FINSEQ_1:65, NAT_1:12
.= g . (((i -' n1) + 1) + n2) by A13, A102, RFINSEQ:def_1
.= g . (((i -' n1) + n2) + 1) ;
1 <= (i -' n1) + n2 by A14, NAT_1:12;
hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by A2, A96, A103, A94, Def6; ::_thesis: verum
end;
end;
end;
A104: rng (g /^ n2) c= rng g by FINSEQ_5:33;
( rng ((g | n1) ^ (g /^ n2)) = (rng (g | n1)) \/ (rng (g /^ n2)) & rng (g | n1) c= rng g ) by FINSEQ_1:31, FINSEQ_5:19;
then rng ((g | n1) ^ (g /^ n2)) c= rng g by A104, XBOOLE_1:8;
then A105: rng ((g | n1) ^ (g /^ n2)) c= A by A4, XBOOLE_1:1;
A106: ((len g) -' n2) + n2 = len g by A77;
A107: (len g) -' n2 in dom (g /^ n2) by A77, A76, A81, FINSEQ_3:25;
then ((g | n1) ^ (g /^ n2)) . ((len (g | n1)) + ((len g) -' n2)) = (g /^ n2) . ((len g) -' n2) by FINSEQ_1:def_7
.= x2 by A6, A13, A107, A106, RFINSEQ:def_1 ;
then ((g | n1) ^ (g /^ n2)) . (len ((g | n1) ^ (g /^ n2))) = x2 by A15, A80, A77, FINSEQ_1:59;
then len g <= len ((g | n1) ^ (g /^ n2)) by A1, A79, A105, A83, Def8;
then (len g) - n1 <= (n1 + ((len g) - n2)) - n1 by A80, XREAL_1:13;
hence contradiction by A75, XREAL_1:10; ::_thesis: verum
end;
supposeA108: n2 = len g ; ::_thesis: contradiction
A109: len (g /^ n2) = (len g) - n2 by A13, RFINSEQ:def_1;
A110: (g | n1) ^ (g /^ n2) is continuous
proof
thus len ((g | n1) ^ (g /^ n2)) >= 1 by A7, A11, A80, A108, FINSEQ_1:1; :: according to FINTOPO6:def_6 ::_thesis: for i being Nat
for x1 being Element of FT st 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & x1 = ((g | n1) ^ (g /^ n2)) . i holds
((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT x1
let i be Nat; ::_thesis: for x1 being Element of FT st 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & x1 = ((g | n1) ^ (g /^ n2)) . i holds
((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT x1
let z1 be Element of FT; ::_thesis: ( 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & z1 = ((g | n1) ^ (g /^ n2)) . i implies ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 )
assume that
A111: 1 <= i and
A112: i < len ((g | n1) ^ (g /^ n2)) and
A113: z1 = ((g | n1) ^ (g /^ n2)) . i ; ::_thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1
A114: i + 1 <= len ((g | n1) ^ (g /^ n2)) by A112, NAT_1:13;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
1 < i + 1 by A111, NAT_1:13;
then i + 1 in dom ((g | n1) ^ (g /^ n2)) by A114, FINSEQ_3:25;
then ((g | n1) ^ (g /^ n2)) . (i + 1) = ((g | n1) ^ (g /^ n2)) /. (i + 1) by PARTFUN1:def_6;
then reconsider z2 = ((g | n1) ^ (g /^ n2)) . (i + 1) as Element of FT ;
percases ( i < n1 or i >= n1 ) ;
supposeA115: i < n1 ; ::_thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1
then A116: i + 1 <= n1 by NAT_1:13;
i + 1 <= len (g | n1) by A78, A115, NAT_1:13;
then A117: z2 = (g | n1) . (i + 1) by FINSEQ_1:64, NAT_1:12
.= g . (i + 1) by A116, FINSEQ_3:112 ;
A118: i < len g by A15, A115, XXREAL_0:2;
z1 = (g | n1) . i by A78, A111, A113, A115, FINSEQ_1:64
.= g . i by A115, FINSEQ_3:112 ;
hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by A2, A111, A118, A117, Def6; ::_thesis: verum
end;
supposeA119: i >= n1 ; ::_thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1
i - n1 < (n1 + ((len g) - n2)) - n1 by A80, A112, XREAL_1:9;
then A120: i -' n1 < (len g) - n2 by A119, XREAL_1:233;
then A121: (i -' n1) + n2 < ((len g) - n2) + n2 by XREAL_1:6;
A122: (len (g | n1)) + (i -' n1) = n1 + (i - n1) by A78, A119, XREAL_1:233
.= i ;
A123: now__::_thesis:_z1_=_g_._((i_-'_n1)_+_n2)
percases ( i > n1 or i = n1 ) by A119, XXREAL_0:1;
suppose i > n1 ; ::_thesis: z1 = g . ((i -' n1) + n2)
then A124: i - n1 > 0 by XREAL_1:50;
then i -' n1 = i - n1 by XREAL_0:def_2;
then A125: 0 + 1 <= i -' n1 by A124, NAT_1:13;
then A126: i -' n1 in dom (g /^ n2) by A109, A120, FINSEQ_3:25;
thus z1 = (g /^ n2) . (i -' n1) by A109, A113, A120, A122, A125, FINSEQ_1:65
.= g . ((i -' n1) + n2) by A13, A126, RFINSEQ:def_1 ; ::_thesis: verum
end;
supposeA127: i = n1 ; ::_thesis: z1 = g . ((i -' n1) + n2)
hence z1 = (g | n1) . n1 by A78, A111, A113, FINSEQ_1:64
.= g . (0 + n2) by A9, FINSEQ_3:112
.= g . ((i -' n1) + n2) by A127, XREAL_1:232 ;
::_thesis: verum
end;
end;
end;
i -' n1 < (len g) -' n2 by A13, A120, XREAL_1:233;
then (i -' n1) + 1 <= (len g) -' n2 by NAT_1:13;
then A128: (i -' n1) + 1 <= len (g /^ n2) by A13, A109, XREAL_1:233;
1 <= (i -' n1) + 1 by NAT_1:12;
then A129: (i -' n1) + 1 in dom (g /^ n2) by A128, FINSEQ_3:25;
(len (g | n1)) + ((i -' n1) + 1) = ((i - n1) + 1) + n1 by A78, A119, XREAL_1:233
.= i + 1 ;
then A130: z2 = (g /^ n2) . ((i -' n1) + 1) by A128, FINSEQ_1:65, NAT_1:12
.= g . (((i -' n1) + 1) + n2) by A13, A129, RFINSEQ:def_1
.= g . (((i -' n1) + n2) + 1) ;
1 <= (i -' n1) + n2 by A14, NAT_1:12;
hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by A2, A123, A130, A121, Def6; ::_thesis: verum
end;
end;
end;
A131: (g | n1) ^ (g /^ n2) = (g | n1) ^ {} by A108, REVROT_1:2
.= g | n1 by FINSEQ_1:34 ;
rng (g | n1) c= rng g by FINSEQ_5:19;
then A132: rng ((g | n1) ^ (g /^ n2)) c= A by A4, A131, XBOOLE_1:1;
((g | n1) ^ (g /^ n2)) . (len ((g | n1) ^ (g /^ n2))) = x2 by A6, A9, A78, A108, A131, FINSEQ_3:112;
then len g <= len ((g | n1) ^ (g /^ n2)) by A1, A79, A132, A110, Def8;
then (len g) - n1 <= (n1 + ((len g) - n2)) - n1 by A80, XREAL_1:13;
hence contradiction by A75, XREAL_1:10; ::_thesis: verum
end;
end;
end;
end;
end;
definition
let FT be non empty RelStr ;
let f be FinSequence of FT;
attrf is inv_continuous means :Def9: :: FINTOPO6:def 9
( 1 <= len f & ( for i, j being Nat
for y being Element of FT st 1 <= i & i <= len f & 1 <= j & j <= len f & y = f . i & i <> j & f . j in U_FT y & not i = j + 1 holds
j = i + 1 ) );
end;
:: deftheorem Def9 defines inv_continuous FINTOPO6:def_9_:_
for FT being non empty RelStr
for f being FinSequence of FT holds
( f is inv_continuous iff ( 1 <= len f & ( for i, j being Nat
for y being Element of FT st 1 <= i & i <= len f & 1 <= j & j <= len f & y = f . i & i <> j & f . j in U_FT y & not i = j + 1 holds
j = i + 1 ) ) );
theorem Th56: :: FINTOPO6:56
for FT being non empty RelStr
for g being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds
g is inv_continuous
proof
let FT be non empty RelStr ; ::_thesis: for g being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds
g is inv_continuous
let g be FinSequence of FT; ::_thesis: for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds
g is inv_continuous
let A be Subset of FT; ::_thesis: for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds
g is inv_continuous
let x1, x2 be Element of FT; ::_thesis: ( g is_minimum_path_in A,x1,x2 & FT is symmetric implies g is inv_continuous )
assume that
A1: g is_minimum_path_in A,x1,x2 and
A2: FT is symmetric ; ::_thesis: g is inv_continuous
A3: g . 1 = x1 by A1, Def8;
A4: g . (len g) = x2 by A1, Def8;
A5: g is continuous by A1, Def8;
hence 1 <= len g by Def6; :: according to FINTOPO6:def_9 ::_thesis: for i, j being Nat
for y being Element of FT st 1 <= i & i <= len g & 1 <= j & j <= len g & y = g . i & i <> j & g . j in U_FT y & not i = j + 1 holds
j = i + 1
let i2, j2 be Nat; ::_thesis: for y being Element of FT st 1 <= i2 & i2 <= len g & 1 <= j2 & j2 <= len g & y = g . i2 & i2 <> j2 & g . j2 in U_FT y & not i2 = j2 + 1 holds
j2 = i2 + 1
let y be Element of FT; ::_thesis: ( 1 <= i2 & i2 <= len g & 1 <= j2 & j2 <= len g & y = g . i2 & i2 <> j2 & g . j2 in U_FT y & not i2 = j2 + 1 implies j2 = i2 + 1 )
assume that
A6: 1 <= i2 and
A7: i2 <= len g and
A8: 1 <= j2 and
A9: j2 <= len g and
A10: y = g . i2 and
A11: i2 <> j2 and
A12: g . j2 in U_FT y ; ::_thesis: ( i2 = j2 + 1 or j2 = i2 + 1 )
A13: rng g c= A by A1, Def8;
hereby ::_thesis: verum
assume that
A14: i2 <> j2 + 1 and
A15: j2 <> i2 + 1 ; ::_thesis: contradiction
percases ( i2 < j2 or j2 < i2 ) by A11, XXREAL_0:1;
supposeA16: i2 < j2 ; ::_thesis: contradiction
set n1 = j2 -' 1;
set n2 = i2;
reconsider n1 = j2 -' 1, n2 = i2 as Element of NAT by ORDINAL1:def_12;
i2 + 1 <= j2 by A16, NAT_1:13;
then i2 + 1 < j2 by A15, XXREAL_0:1;
then i2 < j2 - 1 by XREAL_1:20;
then A17: n1 > n2 by A8, XREAL_1:233;
1 < j2 by A6, A16, XXREAL_0:2;
then 1 + 1 <= j2 by NAT_1:13;
then 1 <= j2 - 1 by XREAL_1:19;
then A18: 1 <= n1 by A8, XREAL_1:233;
set k = (len g) -' n1;
reconsider g2 = (g | n2) ^ (g /^ n1) as FinSequence of FT ;
A19: len (g | n2) = n2 by A7, FINSEQ_1:59;
A20: j2 -' 1 <= j2 by NAT_D:35;
then A21: n1 <= len g by A9, XXREAL_0:2;
then A22: len (g /^ n1) = (len g) - n1 by RFINSEQ:def_1;
A23: (len g) - n1 >= 0 by A21, XREAL_1:48;
then A24: (len g) -' n1 = (len g) - n1 by XREAL_0:def_2;
A25: len g2 = (len (g | n2)) + (len (g /^ n1)) by FINSEQ_1:22
.= n2 + ((len g) - n1) by A21, A19, RFINSEQ:def_1 ;
A26: g2 . 1 = (g | n2) . 1 by A6, A19, FINSEQ_1:64
.= x1 by A3, A6, FINSEQ_3:112 ;
now__::_thesis:_contradiction
percases ( n1 < len g or n1 = len g ) by A21, XXREAL_0:1;
suppose n1 < len g ; ::_thesis: contradiction
then n1 + 1 <= len g by NAT_1:13;
then A27: (n1 + 1) - n1 <= (len g) - n1 by XREAL_1:13;
then A28: 0 + 1 <= n2 + ((len g) - n1) by XREAL_1:7;
A29: g2 is continuous
proof
thus len g2 >= 1 by A25, A28; :: according to FINTOPO6:def_6 ::_thesis: for i being Nat
for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds
g2 . (i + 1) in U_FT x1
let i be Nat; ::_thesis: for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds
g2 . (i + 1) in U_FT x1
let z1 be Element of FT; ::_thesis: ( 1 <= i & i < len g2 & z1 = g2 . i implies g2 . (i + 1) in U_FT z1 )
assume that
A30: 1 <= i and
A31: i < len g2 and
A32: z1 = g2 . i ; ::_thesis: g2 . (i + 1) in U_FT z1
A33: i + 1 <= len g2 by A31, NAT_1:13;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
1 < i + 1 by A30, NAT_1:13;
then i + 1 in dom g2 by A33, FINSEQ_3:25;
then g2 . (i + 1) = g2 /. (i + 1) by PARTFUN1:def_6;
then reconsider z2 = g2 . (i + 1) as Element of FT ;
percases ( i < n2 or i >= n2 ) ;
supposeA34: i < n2 ; ::_thesis: g2 . (i + 1) in U_FT z1
then A35: i + 1 <= n2 by NAT_1:13;
i + 1 <= len (g | n2) by A19, A34, NAT_1:13;
then A36: z2 = (g | n2) . (i + 1) by FINSEQ_1:64, NAT_1:12
.= g . (i + 1) by A35, FINSEQ_3:112 ;
A37: i < len g by A7, A34, XXREAL_0:2;
z1 = (g | n2) . i by A19, A30, A32, A34, FINSEQ_1:64
.= g . i by A34, FINSEQ_3:112 ;
hence g2 . (i + 1) in U_FT z1 by A5, A30, A37, A36, Def6; ::_thesis: verum
end;
supposeA38: i >= n2 ; ::_thesis: g2 . (i + 1) in U_FT z1
i - n2 < (n2 + ((len g) - n1)) - n2 by A25, A31, XREAL_1:9;
then A39: i -' n2 < (len g) - n1 by A38, XREAL_1:233;
then i -' n2 < (len g) -' n1 by A9, A20, XREAL_1:233, XXREAL_0:2;
then (i -' n2) + 1 <= (len g) -' n1 by NAT_1:13;
then A40: (i -' n2) + 1 <= len (g /^ n1) by A9, A20, A22, XREAL_1:233, XXREAL_0:2;
A41: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by A19, A38, XREAL_1:233
.= i ;
A42: (len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by A19, A38, XREAL_1:233
.= i + 1 ;
1 <= (i -' n2) + 1 by NAT_1:12;
then A43: (i -' n2) + 1 in dom (g /^ n1) by A40, FINSEQ_3:25;
percases ( i > n2 or i = n2 ) by A38, XXREAL_0:1;
suppose i > n2 ; ::_thesis: g2 . (i + 1) in U_FT z1
then A44: i - n2 > 0 by XREAL_1:50;
then i -' n2 = i - n2 by XREAL_0:def_2;
then A45: 0 + 1 <= i -' n2 by A44, NAT_1:13;
then A46: i -' n2 in dom (g /^ n1) by A22, A39, FINSEQ_3:25;
A47: z2 = (g /^ n1) . ((i -' n2) + 1) by A40, A42, FINSEQ_1:65, NAT_1:12
.= g . (((i -' n2) + 1) + n1) by A21, A43, RFINSEQ:def_1
.= g . (((i -' n2) + n1) + 1) ;
A48: ( 1 <= (i -' n2) + n1 & (i -' n2) + n1 < ((len g) - n1) + n1 ) by A18, A39, NAT_1:12, XREAL_1:6;
z1 = (g /^ n1) . (i -' n2) by A22, A32, A39, A41, A45, FINSEQ_1:65
.= g . ((i -' n2) + n1) by A21, A46, RFINSEQ:def_1 ;
hence g2 . (i + 1) in U_FT z1 by A5, A47, A48, Def6; ::_thesis: verum
end;
supposeA49: i = n2 ; ::_thesis: g2 . (i + 1) in U_FT z1
then A50: z1 = (g | n2) . n2 by A19, A30, A32, FINSEQ_1:64
.= y by A10, FINSEQ_3:112 ;
z2 = (g /^ n1) . ((i -' n2) + 1) by A40, A42, FINSEQ_1:65, NAT_1:12
.= g . (((i -' n2) + 1) + n1) by A21, A43, RFINSEQ:def_1
.= g . (((i -' n2) + n1) + 1)
.= g . ((0 + (j2 -' 1)) + 1) by A49, XREAL_1:232
.= g . ((j2 - 1) + 1) by A8, XREAL_1:233 ;
hence g2 . (i + 1) in U_FT z1 by A12, A50; ::_thesis: verum
end;
end;
end;
end;
end;
A51: rng (g /^ n1) c= rng g by FINSEQ_5:33;
( rng g2 = (rng (g | n2)) \/ (rng (g /^ n1)) & rng (g | n2) c= rng g ) by FINSEQ_1:31, FINSEQ_5:19;
then rng g2 c= rng g by A51, XBOOLE_1:8;
then A52: rng g2 c= A by A13, XBOOLE_1:1;
A53: ((len g) -' n1) + n1 = len g by A24;
A54: (len g) -' n1 in dom (g /^ n1) by A24, A22, A27, FINSEQ_3:25;
then g2 . ((len (g | n2)) + ((len g) -' n1)) = (g /^ n1) . ((len g) -' n1) by FINSEQ_1:def_7
.= x2 by A4, A21, A54, A53, RFINSEQ:def_1 ;
then g2 . (len g2) = x2 by A19, A25, A23, XREAL_0:def_2;
then len g <= len g2 by A1, A26, A52, A29, Def8;
then (len g) - n2 <= (n2 + ((len g) - n1)) - n2 by A25, XREAL_1:13;
hence contradiction by A17, XREAL_1:10; ::_thesis: verum
end;
suppose n1 = len g ; ::_thesis: contradiction
then j2 - 1 = len g by A8, XREAL_1:233;
then j2 = (len g) + 1 ;
hence contradiction by A9, NAT_1:13; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
supposeA55: j2 < i2 ; ::_thesis: contradiction
reconsider n1 = i2 -' 1, n2 = j2 as Element of NAT by ORDINAL1:def_12;
j2 + 1 <= i2 by A55, NAT_1:13;
then j2 + 1 < i2 by A14, XXREAL_0:1;
then j2 < i2 - 1 by XREAL_1:20;
then A56: n1 > n2 by A6, XREAL_1:233;
1 < i2 by A8, A55, XXREAL_0:2;
then 1 + 1 <= i2 by NAT_1:13;
then 1 <= i2 - 1 by XREAL_1:19;
then A57: 1 <= n1 by A6, XREAL_1:233;
set k = (len g) -' n1;
reconsider g2 = (g | n2) ^ (g /^ n1) as FinSequence of FT ;
A58: len (g | n2) = n2 by A9, FINSEQ_1:59;
A59: i2 -' 1 <= i2 by NAT_D:35;
then A60: n1 <= len g by A7, XXREAL_0:2;
then A61: len (g /^ n1) = (len g) - n1 by RFINSEQ:def_1;
A62: (len g) - n1 >= 0 by A60, XREAL_1:48;
then A63: (len g) -' n1 = (len g) - n1 by XREAL_0:def_2;
A64: len g2 = (len (g | n2)) + (len (g /^ n1)) by FINSEQ_1:22
.= n2 + ((len g) - n1) by A60, A58, RFINSEQ:def_1 ;
A65: g2 . 1 = (g | n2) . 1 by A8, A58, FINSEQ_1:64
.= x1 by A3, A8, FINSEQ_3:112 ;
now__::_thesis:_contradiction
percases ( n1 < len g or n1 = len g ) by A60, XXREAL_0:1;
suppose n1 < len g ; ::_thesis: contradiction
then n1 + 1 <= len g by NAT_1:13;
then A66: (n1 + 1) - n1 <= (len g) - n1 by XREAL_1:13;
then A67: 0 + 1 <= n2 + ((len g) - n1) by XREAL_1:7;
A68: g2 is continuous
proof
thus len g2 >= 1 by A64, A67; :: according to FINTOPO6:def_6 ::_thesis: for i being Nat
for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds
g2 . (i + 1) in U_FT x1
let i be Nat; ::_thesis: for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds
g2 . (i + 1) in U_FT x1
let z1 be Element of FT; ::_thesis: ( 1 <= i & i < len g2 & z1 = g2 . i implies g2 . (i + 1) in U_FT z1 )
assume that
A69: 1 <= i and
A70: i < len g2 and
A71: z1 = g2 . i ; ::_thesis: g2 . (i + 1) in U_FT z1
A72: i + 1 <= len g2 by A70, NAT_1:13;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
1 < i + 1 by A69, NAT_1:13;
then i + 1 in dom g2 by A72, FINSEQ_3:25;
then g2 . (i + 1) = g2 /. (i + 1) by PARTFUN1:def_6;
then reconsider z2 = g2 . (i + 1) as Element of FT ;
percases ( i < n2 or i >= n2 ) ;
supposeA73: i < n2 ; ::_thesis: g2 . (i + 1) in U_FT z1
then A74: i + 1 <= n2 by NAT_1:13;
i + 1 <= len (g | n2) by A58, A73, NAT_1:13;
then A75: z2 = (g | n2) . (i + 1) by FINSEQ_1:64, NAT_1:12
.= g . (i + 1) by A74, FINSEQ_3:112 ;
A76: i < len g by A9, A73, XXREAL_0:2;
z1 = (g | n2) . i by A58, A69, A71, A73, FINSEQ_1:64
.= g . i by A73, FINSEQ_3:112 ;
hence g2 . (i + 1) in U_FT z1 by A5, A69, A76, A75, Def6; ::_thesis: verum
end;
supposeA77: i >= n2 ; ::_thesis: g2 . (i + 1) in U_FT z1
i - n2 < (n2 + ((len g) - n1)) - n2 by A64, A70, XREAL_1:9;
then A78: i -' n2 < (len g) - n1 by A77, XREAL_1:233;
then i -' n2 < (len g) -' n1 by A7, A59, XREAL_1:233, XXREAL_0:2;
then (i -' n2) + 1 <= (len g) -' n1 by NAT_1:13;
then A79: (i -' n2) + 1 <= len (g /^ n1) by A7, A59, A61, XREAL_1:233, XXREAL_0:2;
A80: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by A58, A77, XREAL_1:233
.= i ;
A81: (len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by A58, A77, XREAL_1:233
.= i + 1 ;
1 <= (i -' n2) + 1 by NAT_1:12;
then A82: (i -' n2) + 1 in dom (g /^ n1) by A79, FINSEQ_3:25;
percases ( i > n2 or i = n2 ) by A77, XXREAL_0:1;
suppose i > n2 ; ::_thesis: g2 . (i + 1) in U_FT z1
then A83: i - n2 > 0 by XREAL_1:50;
then i -' n2 = i - n2 by XREAL_0:def_2;
then A84: 0 + 1 <= i -' n2 by A83, NAT_1:13;
then A85: i -' n2 in dom (g /^ n1) by A61, A78, FINSEQ_3:25;
A86: z2 = (g /^ n1) . ((i -' n2) + 1) by A79, A81, FINSEQ_1:65, NAT_1:12
.= g . (((i -' n2) + 1) + n1) by A60, A82, RFINSEQ:def_1
.= g . (((i -' n2) + n1) + 1) ;
A87: ( 1 <= (i -' n2) + n1 & (i -' n2) + n1 < ((len g) - n1) + n1 ) by A57, A78, NAT_1:12, XREAL_1:6;
z1 = (g /^ n1) . (i -' n2) by A61, A71, A78, A80, A84, FINSEQ_1:65
.= g . ((i -' n2) + n1) by A60, A85, RFINSEQ:def_1 ;
hence g2 . (i + 1) in U_FT z1 by A5, A86, A87, Def6; ::_thesis: verum
end;
supposeA88: i = n2 ; ::_thesis: g2 . (i + 1) in U_FT z1
then A89: z1 = (g | n2) . n2 by A58, A69, A71, FINSEQ_1:64
.= g . j2 by FINSEQ_3:112 ;
z2 = (g /^ n1) . ((i -' n2) + 1) by A79, A81, FINSEQ_1:65, NAT_1:12
.= g . (((i -' n2) + 1) + n1) by A60, A82, RFINSEQ:def_1
.= g . (((i -' n2) + n1) + 1)
.= g . ((0 + (i2 -' 1)) + 1) by A88, XREAL_1:232
.= g . ((i2 - 1) + 1) by A6, XREAL_1:233
.= y by A10 ;
hence g2 . (i + 1) in U_FT z1 by A2, A12, A89, FIN_TOPO:def_13; ::_thesis: verum
end;
end;
end;
end;
end;
A90: rng (g /^ n1) c= rng g by FINSEQ_5:33;
( rng g2 = (rng (g | n2)) \/ (rng (g /^ n1)) & rng (g | n2) c= rng g ) by FINSEQ_1:31, FINSEQ_5:19;
then rng g2 c= rng g by A90, XBOOLE_1:8;
then A91: rng g2 c= A by A13, XBOOLE_1:1;
A92: ((len g) -' n1) + n1 = len g by A63;
A93: (len g) -' n1 in dom (g /^ n1) by A63, A61, A66, FINSEQ_3:25;
then g2 . ((len (g | n2)) + ((len g) -' n1)) = (g /^ n1) . ((len g) -' n1) by FINSEQ_1:def_7
.= x2 by A4, A60, A93, A92, RFINSEQ:def_1 ;
then g2 . (len g2) = x2 by A58, A64, A62, XREAL_0:def_2;
then len g <= len g2 by A1, A65, A91, A68, Def8;
then (len g) - n2 <= (n2 + ((len g) - n1)) - n2 by A64, XREAL_1:13;
hence contradiction by A56, XREAL_1:10; ::_thesis: verum
end;
suppose n1 = len g ; ::_thesis: contradiction
then i2 - 1 = len g by A6, XREAL_1:233;
then i2 = (len g) + 1 ;
hence contradiction by A7, NAT_1:13; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
end;
end;
end;
theorem :: FINTOPO6:57
for FT being non empty RelStr
for g being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & x1 <> x2 holds
( ( for i being Nat st 1 < i & i < len g holds
(rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ) & (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} )
proof
let FT be non empty RelStr ; ::_thesis: for g being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & x1 <> x2 holds
( ( for i being Nat st 1 < i & i < len g holds
(rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ) & (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} )
let g be FinSequence of FT; ::_thesis: for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & x1 <> x2 holds
( ( for i being Nat st 1 < i & i < len g holds
(rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ) & (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} )
let A be Subset of FT; ::_thesis: for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & x1 <> x2 holds
( ( for i being Nat st 1 < i & i < len g holds
(rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ) & (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} )
let x1, x2 be Element of FT; ::_thesis: ( g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & x1 <> x2 implies ( ( for i being Nat st 1 < i & i < len g holds
(rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ) & (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} ) )
assume that
A1: g is_minimum_path_in A,x1,x2 and
A2: ( FT is filled & FT is symmetric ) and
A3: x1 <> x2 ; ::_thesis: ( ( for i being Nat st 1 < i & i < len g holds
(rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ) & (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} )
A4: dom g = Seg (len g) by FINSEQ_1:def_3;
A5: g is continuous by A1, Def8;
then A6: 1 <= len g by Def6;
then A7: len g in dom g by A4;
then A8: g . (len g) = g /. (len g) by PARTFUN1:def_6;
A9: g is inv_continuous by A1, A2, Th56;
then A10: 1 <= len g by Def9;
thus for i being Nat st 1 < i & i < len g holds
(rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ::_thesis: ( (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} )
proof
let i be Nat; ::_thesis: ( 1 < i & i < len g implies (rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} )
assume that
A11: 1 < i and
A12: i < len g ; ::_thesis: (rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))}
A13: i in Seg (len g) by A11, A12, FINSEQ_1:1;
( 1 < i + 1 & i + 1 <= len g ) by A11, A12, NAT_1:13;
then A14: i + 1 in Seg (len g) ;
i -' 1 <= i by NAT_D:35;
then A15: i -' 1 < len g by A12, XXREAL_0:2;
1 + 1 <= i by A11, NAT_1:13;
then A16: 1 <= i - 1 by XREAL_1:19;
then 1 <= i -' 1 by A11, XREAL_1:233;
then A17: i -' 1 in Seg (len g) by A15;
A18: (i -' 1) + 1 = (i - 1) + 1 by A11, XREAL_1:233
.= i ;
thus (rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ::_thesis: verum
proof
thus (rng g) /\ (U_FT (g /. i)) c= {(g . (i -' 1)),(g . i),(g . (i + 1))} :: according to XBOOLE_0:def_10 ::_thesis: {(g . (i -' 1)),(g . i),(g . (i + 1))} c= (rng g) /\ (U_FT (g /. i))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (rng g) /\ (U_FT (g /. i)) or x in {(g . (i -' 1)),(g . i),(g . (i + 1))} )
assume A19: x in (rng g) /\ (U_FT (g /. i)) ; ::_thesis: x in {(g . (i -' 1)),(g . i),(g . (i + 1))}
then A20: x in U_FT (g /. i) by XBOOLE_0:def_4;
x in rng g by A19, XBOOLE_0:def_4;
then consider nx being set such that
A21: nx in dom g and
A22: x = g . nx by FUNCT_1:def_3;
reconsider j = nx as Element of NAT by A21;
( i = j + 1 implies i - 1 = j ) ;
then A23: ( i = j + 1 implies i -' 1 = j ) by A11, XREAL_1:233;
A24: g /. i = g . i by A4, A13, PARTFUN1:def_6;
( 1 <= j & j <= len g ) by A4, A21, FINSEQ_1:1;
then ( j = i or i = j + 1 or j = i + 1 ) by A9, A11, A12, A20, A22, A24, Def9;
hence x in {(g . (i -' 1)),(g . i),(g . (i + 1))} by A22, A23, ENUMSET1:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(g . (i -' 1)),(g . i),(g . (i + 1))} or x in (rng g) /\ (U_FT (g /. i)) )
A25: g . i = g /. i by A4, A13, PARTFUN1:def_6;
A26: g . (i -' 1) = g /. (i -' 1) by A4, A17, PARTFUN1:def_6;
assume A27: x in {(g . (i -' 1)),(g . i),(g . (i + 1))} ; ::_thesis: x in (rng g) /\ (U_FT (g /. i))
percases ( x = g . (i -' 1) or x = g . i or x = g . (i + 1) ) by A27, ENUMSET1:def_1;
supposeA28: x = g . (i -' 1) ; ::_thesis: x in (rng g) /\ (U_FT (g /. i))
g . i in U_FT (g /. (i -' 1)) by A5, A16, A15, A18, A26, Def6;
then A29: x in U_FT (g /. i) by A2, A25, A26, A28, FIN_TOPO:def_13;
x in rng g by A4, A17, A28, FUNCT_1:def_3;
hence x in (rng g) /\ (U_FT (g /. i)) by A29, XBOOLE_0:def_4; ::_thesis: verum
end;
suppose x = g . i ; ::_thesis: x in (rng g) /\ (U_FT (g /. i))
then ( x in rng g & x in U_FT (g /. i) ) by A2, A4, A13, A25, FIN_TOPO:def_4, FUNCT_1:def_3;
hence x in (rng g) /\ (U_FT (g /. i)) by XBOOLE_0:def_4; ::_thesis: verum
end;
suppose x = g . (i + 1) ; ::_thesis: x in (rng g) /\ (U_FT (g /. i))
then ( x in rng g & x in U_FT (g /. i) ) by A5, A4, A11, A12, A14, A25, Def6, FUNCT_1:def_3;
hence x in (rng g) /\ (U_FT (g /. i)) by XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
end;
( g . 1 = x1 & g . (len g) = x2 ) by A1, Def8;
then A30: 1 < len g by A3, A6, XXREAL_0:1;
then A31: 1 + 1 <= len g by NAT_1:13;
then A32: (1 + 1) - 1 <= (len g) - 1 by XREAL_1:13;
A33: 1 in dom g by A10, FINSEQ_3:25;
then A34: g . 1 = g /. 1 by PARTFUN1:def_6;
thus (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} ::_thesis: (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))}
proof
thus (rng g) /\ (U_FT (g /. 1)) c= {(g . 1),(g . 2)} :: according to XBOOLE_0:def_10 ::_thesis: {(g . 1),(g . 2)} c= (rng g) /\ (U_FT (g /. 1))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (rng g) /\ (U_FT (g /. 1)) or x in {(g . 1),(g . 2)} )
assume A35: x in (rng g) /\ (U_FT (g /. 1)) ; ::_thesis: x in {(g . 1),(g . 2)}
then A36: x in U_FT (g /. 1) by XBOOLE_0:def_4;
x in rng g by A35, XBOOLE_0:def_4;
then consider y being set such that
A37: y in dom g and
A38: x = g . y by FUNCT_1:def_3;
reconsider j = y as Element of NAT by A37;
A39: 1 <= j by A4, A37, FINSEQ_1:1;
j <= len g by A4, A37, FINSEQ_1:1;
then ( 1 + 1 = j or 1 = j or j + 1 = 1 ) by A9, A10, A34, A36, A38, A39, Def9;
then ( 1 + 1 = j or 1 = j ) by A39, XREAL_1:7;
hence x in {(g . 1),(g . 2)} by A38, TARSKI:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(g . 1),(g . 2)} or x in (rng g) /\ (U_FT (g /. 1)) )
2 in dom g by A31, A4;
then A40: ( x = g . 2 implies x in rng g ) by FUNCT_1:def_3;
assume A41: x in {(g . 1),(g . 2)} ; ::_thesis: x in (rng g) /\ (U_FT (g /. 1))
A42: now__::_thesis:_(_(_x_=_g_._1_&_x_in_U_FT_(g_/._1)_)_or_(_x_=_g_._2_&_x_in_U_FT_(g_/._1)_)_)
percases ( x = g . 1 or x = g . 2 ) by A41, TARSKI:def_2;
case x = g . 1 ; ::_thesis: x in U_FT (g /. 1)
hence x in U_FT (g /. 1) by A2, A34, FIN_TOPO:def_4; ::_thesis: verum
end;
caseA43: x = g . 2 ; ::_thesis: x in U_FT (g /. 1)
then reconsider xx = x as Element of FT by A40;
xx = g . (1 + 1) by A43;
hence x in U_FT (g /. 1) by A5, A30, A34, Def6; ::_thesis: verum
end;
end;
end;
( x = g . 1 implies x in rng g ) by A33, FUNCT_1:def_3;
hence x in (rng g) /\ (U_FT (g /. 1)) by A40, A42, XBOOLE_0:def_4; ::_thesis: verum
end;
len g < (len g) + 1 by NAT_1:13;
then A44: (len g) - 1 < ((len g) + 1) - 1 by XREAL_1:14;
then A45: (len g) -' 1 < len g by A10, XREAL_1:233;
A46: (len g) -' 1 = (len g) - 1 by A10, XREAL_1:233;
then A47: (len g) -' 1 in dom g by A32, A44, FINSEQ_3:25;
then A48: g . ((len g) -' 1) = g /. ((len g) -' 1) by PARTFUN1:def_6;
A49: 1 <= (len g) -' 1 by A10, A32, XREAL_1:233;
thus (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} ::_thesis: verum
proof
thus (rng g) /\ (U_FT (g /. (len g))) c= {(g . ((len g) -' 1)),(g . (len g))} :: according to XBOOLE_0:def_10 ::_thesis: {(g . ((len g) -' 1)),(g . (len g))} c= (rng g) /\ (U_FT (g /. (len g)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (rng g) /\ (U_FT (g /. (len g))) or x in {(g . ((len g) -' 1)),(g . (len g))} )
assume A50: x in (rng g) /\ (U_FT (g /. (len g))) ; ::_thesis: x in {(g . ((len g) -' 1)),(g . (len g))}
then A51: x in U_FT (g /. (len g)) by XBOOLE_0:def_4;
x in rng g by A50, XBOOLE_0:def_4;
then consider y being set such that
A52: y in dom g and
A53: x = g . y by FUNCT_1:def_3;
reconsider ny = y as Element of NAT by A52;
A54: ny <= len g by A4, A52, FINSEQ_1:1;
1 <= ny by A4, A52, FINSEQ_1:1;
then ( ny + 1 = len g or (len g) + 1 = ny or len g = ny ) by A9, A10, A8, A51, A53, A54, Def9;
then ( ny = (len g) - 1 or len g = ny ) by A54, NAT_1:13;
then ( x = g . ((len g) -' 1) or x = g . (len g) ) by A6, A53, XREAL_1:233;
hence x in {(g . ((len g) -' 1)),(g . (len g))} by TARSKI:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(g . ((len g) -' 1)),(g . (len g))} or x in (rng g) /\ (U_FT (g /. (len g))) )
A55: g . (len g) in U_FT (g /. (len g)) by A2, A8, FIN_TOPO:def_4;
g . (((len g) -' 1) + 1) in U_FT (g /. ((len g) -' 1)) by A5, A49, A45, A48, Def6;
then A56: g . ((len g) -' 1) in U_FT (g /. (len g)) by A2, A8, A46, A48, FIN_TOPO:def_13;
assume x in {(g . ((len g) -' 1)),(g . (len g))} ; ::_thesis: x in (rng g) /\ (U_FT (g /. (len g)))
then A57: ( x = g . ((len g) -' 1) or x = g . (len g) ) by TARSKI:def_2;
then x in rng g by A7, A47, FUNCT_1:def_3;
hence x in (rng g) /\ (U_FT (g /. (len g))) by A57, A55, A56, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
theorem :: FINTOPO6:58
for FT being non empty RelStr
for g being FinSequence of FT
for A being non empty Subset of FT
for x1, x2 being Element of FT
for B0 being Subset of (FT | A) st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & B0 = {x1} holds
for i being Element of NAT st i < len g holds
( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) )
proof
let FT be non empty RelStr ; ::_thesis: for g being FinSequence of FT
for A being non empty Subset of FT
for x1, x2 being Element of FT
for B0 being Subset of (FT | A) st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & B0 = {x1} holds
for i being Element of NAT st i < len g holds
( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) )
let g be FinSequence of FT; ::_thesis: for A being non empty Subset of FT
for x1, x2 being Element of FT
for B0 being Subset of (FT | A) st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & B0 = {x1} holds
for i being Element of NAT st i < len g holds
( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) )
let A be non empty Subset of FT; ::_thesis: for x1, x2 being Element of FT
for B0 being Subset of (FT | A) st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & B0 = {x1} holds
for i being Element of NAT st i < len g holds
( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) )
let x1, x2 be Element of FT; ::_thesis: for B0 being Subset of (FT | A) st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & B0 = {x1} holds
for i being Element of NAT st i < len g holds
( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) )
let B0 be Subset of (FT | A); ::_thesis: ( g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & B0 = {x1} implies for i being Element of NAT st i < len g holds
( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) ) )
assume that
A1: g is_minimum_path_in A,x1,x2 and
A2: ( FT is filled & FT is symmetric ) and
A3: B0 = {x1} ; ::_thesis: for i being Element of NAT st i < len g holds
( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) )
A4: rng g c= A by A1, Def8;
defpred S1[ Nat] means ( $1 + 1 <= len g implies ( g . ($1 + 1) in Finf (B0,$1) & ( $1 >= 1 implies not g . ($1 + 1) in Finf (B0,($1 -' 1)) ) ) );
defpred S2[ Element of NAT ] means for y being Element of FT st y in Finf (B0,$1) holds
ex h being FinSequence of FT st
( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= $1 + 1 );
A5: [#] (FT | A) = A by Def3;
A6: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A7: S2[k] ; ::_thesis: S2[k + 1]
for y being Element of FT st y in Finf (B0,(k + 1)) holds
ex h being FinSequence of FT st
( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= (k + 1) + 1 )
proof
let y be Element of FT; ::_thesis: ( y in Finf (B0,(k + 1)) implies ex h being FinSequence of FT st
( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= (k + 1) + 1 ) )
A8: Finf (B0,(k + 1)) = (Finf (B0,k)) ^f by FINTOPO3:31;
assume y in Finf (B0,(k + 1)) ; ::_thesis: ex h being FinSequence of FT st
( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= (k + 1) + 1 )
then consider x being Element of (FT | A) such that
A9: x = y and
A10: ex y2 being Element of (FT | A) st
( y2 in Finf (B0,k) & x in U_FT y2 ) by A8;
A11: [#] (FT | A) = A by Def3;
then A12: {y} c= A by A9, ZFMISC_1:31;
consider y2 being Element of (FT | A) such that
A13: y2 in Finf (B0,k) and
A14: x in U_FT y2 by A10;
y2 in the carrier of (FT | A) ;
then reconsider y3 = y2 as Element of FT by A11;
consider h2 being FinSequence of FT such that
A15: h2 is continuous and
A16: rng h2 c= A and
A17: h2 . 1 = x1 and
A18: h2 . (len h2) = y3 and
A19: len h2 <= k + 1 by A7, A13;
U_FT y2 = (U_FT y3) /\ A by A11, Def2;
then A20: y in U_FT y3 by A9, A14, XBOOLE_0:def_4;
reconsider h3 = h2 ^ <*y*> as FinSequence of FT ;
( rng (h2 ^ <*y*>) = (rng h2) \/ (rng <*y*>) & rng <*y*> = {y} ) by FINSEQ_1:31, FINSEQ_1:39;
then A21: rng h3 c= A by A16, A12, XBOOLE_1:8;
1 <= len h2 by A15, Def6;
then 1 in dom h2 by FINSEQ_3:25;
then A22: h3 . 1 = x1 by A17, FINSEQ_1:def_7;
len <*y*> = 1 by FINSEQ_1:40;
then A23: len h3 = (len h2) + 1 by FINSEQ_1:22;
then A24: h3 . (len h3) = y by FINSEQ_1:42;
len h3 <= (k + 1) + 1 by A19, A23, XREAL_1:6;
hence ex h being FinSequence of FT st
( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= (k + 1) + 1 ) by A15, A18, A20, A21, A22, A24, Th44; ::_thesis: verum
end;
hence S2[k + 1] ; ::_thesis: verum
end;
A25: g . 1 = x1 by A1, Def8;
then A26: g . 1 in {x1} by TARSKI:def_1;
A27: g . (len g) = x2 by A1, Def8;
A28: g is continuous by A1, Def8;
then 1 <= len g by Def6;
then 1 in dom g by FINSEQ_3:25;
then x1 in rng g by A25, FUNCT_1:def_3;
then A29: {x1} c= A by A4, ZFMISC_1:31;
for y being Element of FT st y in Finf (B0,0) holds
ex h being FinSequence of FT st
( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= 0 + 1 )
proof
let y be Element of FT; ::_thesis: ( y in Finf (B0,0) implies ex h being FinSequence of FT st
( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= 0 + 1 ) )
A30: len <*x1*> = 1 by FINSEQ_1:40;
assume y in Finf (B0,0) ; ::_thesis: ex h being FinSequence of FT st
( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= 0 + 1 )
then y in {x1} by A3, FINTOPO3:32;
then A31: y = x1 by TARSKI:def_1;
( rng <*x1*> = {x1} & <*x1*> . 1 = x1 ) by FINSEQ_1:39, FINSEQ_1:40;
hence ex h being FinSequence of FT st
( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= 0 + 1 ) by A29, A31, A30; ::_thesis: verum
end;
then A32: S2[ 0 ] ;
A33: for k being Element of NAT holds S2[k] from NAT_1:sch_1(A32, A6);
A34: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A35: S1[k] ; ::_thesis: S1[k + 1]
percases ( (k + 1) + 1 > len g or (k + 1) + 1 <= len g ) ;
suppose (k + 1) + 1 > len g ; ::_thesis: S1[k + 1]
hence S1[k + 1] ; ::_thesis: verum
end;
supposeA36: (k + 1) + 1 <= len g ; ::_thesis: S1[k + 1]
A37: 1 <= k + 1 by NAT_1:12;
then 1 < (k + 1) + 1 by NAT_1:13;
then (k + 1) + 1 in dom g by A36, FINSEQ_3:25;
then A38: g . ((k + 1) + 1) in rng g by FUNCT_1:def_3;
reconsider y0 = g . (k + 1) as Element of (FT | A) by A35, A36, NAT_1:13;
A39: k + 1 < len g by A36, NAT_1:13;
then k + 1 in dom g by A37, FINSEQ_3:25;
then A40: g . (k + 1) = g /. (k + 1) by PARTFUN1:def_6;
1 < (k + 1) + 1 by A37, NAT_1:13;
then A41: (k + 1) + 1 in dom g by A36, FINSEQ_3:25;
A42: now__::_thesis:_not_g_._((k_+_1)_+_1)_in_Finf_(B0,k)
assume A43: g . ((k + 1) + 1) in Finf (B0,k) ; ::_thesis: contradiction
now__::_thesis:_g_._((k_+_1)_+_1)_in_(Finf_(B0,(k_-'_1)))_^f
percases ( k = 0 or k > 0 ) ;
supposeA44: k = 0 ; ::_thesis: g . ((k + 1) + 1) in (Finf (B0,(k -' 1))) ^f
then k - 1 < 0 ;
then k -' 1 = 0 by XREAL_0:def_2;
then Finf (B0,k) c= (Finf (B0,(k -' 1))) ^f by A2, A44, FINTOPO3:1;
hence g . ((k + 1) + 1) in (Finf (B0,(k -' 1))) ^f by A43; ::_thesis: verum
end;
suppose k > 0 ; ::_thesis: g . ((k + 1) + 1) in (Finf (B0,(k -' 1))) ^f
then k >= 0 + 1 by NAT_1:13;
then k = (k -' 1) + 1 by XREAL_1:235;
hence g . ((k + 1) + 1) in (Finf (B0,(k -' 1))) ^f by A43, FINTOPO3:31; ::_thesis: verum
end;
end;
end;
then consider x being Element of (FT | A) such that
A45: g . ((k + 1) + 1) = x and
ex y being Element of (FT | A) st
( y in Finf (B0,(k -' 1)) & x in U_FT y ) ;
x in A by A5;
then reconsider x3 = x as Element of FT ;
consider h being FinSequence of FT such that
A46: h is continuous and
A47: rng h c= A and
A48: h . 1 = x1 and
A49: h . (len h) = x3 and
A50: len h <= k + 1 by A33, A43, A45;
reconsider s = h ^ (g /^ ((k + 1) + 1)) as FinSequence of FT ;
A51: len s = (len h) + (len (g /^ ((k + 1) + 1))) by FINSEQ_1:22;
g = (g | ((k + 1) + 1)) ^ (g /^ ((k + 1) + 1)) by RFINSEQ:8;
then A52: len g = (len (g | ((k + 1) + 1))) + (len (g /^ ((k + 1) + 1))) by FINSEQ_1:22;
A53: 1 <= len h by A46, Def6;
then len h in dom h by FINSEQ_3:25;
then A54: h . (len h) = h /. (len h) by PARTFUN1:def_6;
len (g | ((k + 1) + 1)) = (k + 1) + 1 by A36, FINSEQ_1:59;
then A55: len (g | ((k + 1) + 1)) > len h by A50, NAT_1:13;
then A56: len s < len g by A51, A52, XREAL_1:8;
percases ( (k + 1) + 1 < len g or (k + 1) + 1 >= len g ) ;
supposeA57: (k + 1) + 1 < len g ; ::_thesis: contradiction
then len g >= 1 + ((k + 1) + 1) by NAT_1:13;
then 1 <= (len g) - ((k + 1) + 1) by XREAL_1:19;
then 1 <= len (g /^ ((k + 1) + 1)) by A57, RFINSEQ:def_1;
then A58: 1 in dom (g /^ ((k + 1) + 1)) by FINSEQ_3:25;
A59: g . ((k + 1) + 1) = g /. ((k + 1) + 1) by A41, PARTFUN1:def_6;
A60: g /^ ((k + 1) + 1) is continuous by A28, A57, Th48;
then 1 <= len (g /^ ((k + 1) + 1)) by Def6;
then len (g /^ ((k + 1) + 1)) in dom (g /^ ((k + 1) + 1)) by FINSEQ_3:25;
then A61: s . (len s) = (g /^ ((k + 1) + 1)) . (len (g /^ ((k + 1) + 1))) by A51, FINSEQ_1:def_7
.= x2 by A27, A57, JORDAN4:6 ;
1 <= (k + 1) + 1 by NAT_1:12;
then g . (((k + 1) + 1) + 1) in U_FT (g /. ((k + 1) + 1)) by A28, A57, A59, Def6;
then (g /^ ((k + 1) + 1)) . 1 in U_FT (h /. (len h)) by A45, A49, A54, A57, A59, A58, RFINSEQ:def_1;
then A62: s is continuous by A46, A60, Th45;
1 in dom h by A53, FINSEQ_3:25;
then A63: s . 1 = x1 by A48, FINSEQ_1:def_7;
rng (g /^ ((k + 1) + 1)) c= rng g by FINSEQ_5:33;
then A64: rng (g /^ ((k + 1) + 1)) c= A by A4, XBOOLE_1:1;
rng s = (rng h) \/ (rng (g /^ ((k + 1) + 1))) by FINSEQ_1:31;
then rng s c= A by A47, A64, XBOOLE_1:8;
hence contradiction by A1, A56, A62, A63, A61, Def8; ::_thesis: verum
end;
supposeA65: (k + 1) + 1 >= len g ; ::_thesis: contradiction
then g /^ ((k + 1) + 1) = <*> the carrier of FT by FINSEQ_5:32;
then A66: s = h by FINSEQ_1:34;
(k + 1) + 1 = len g by A36, A65, XXREAL_0:1;
hence contradiction by A1, A27, A45, A46, A47, A48, A49, A55, A51, A52, A66, Def8; ::_thesis: verum
end;
end;
end;
[#] (FT | A) = A by Def3;
then A67: U_FT y0 = (U_FT (g /. (k + 1))) /\ A by A40, Def2;
g . ((k + 1) + 1) in U_FT (g /. (k + 1)) by A28, A39, A37, A40, Def6;
then g . ((k + 1) + 1) in U_FT y0 by A4, A67, A38, XBOOLE_0:def_4;
then A68: g . ((k + 1) + 1) in (Finf (B0,k)) ^f by A35, A36, NAT_1:13;
(k + 1) -' 1 = (k + 1) - 1 by NAT_D:37
.= k ;
hence S1[k + 1] by A68, A42, FINTOPO3:31; ::_thesis: verum
end;
end;
end;
let i be Element of NAT ; ::_thesis: ( i < len g implies ( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) ) )
assume i < len g ; ::_thesis: ( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) )
then A69: i + 1 <= len g by NAT_1:13;
Finf ({x1},0) = {x1} by FINTOPO3:32
.= Finf (B0,0) by A3, FINTOPO3:32 ;
then A70: S1[ 0 ] by A26, FINTOPO3:32;
for j being Element of NAT holds S1[j] from NAT_1:sch_1(A70, A34);
hence ( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) ) by A69; ::_thesis: verum
end;