let x be object ; :: thesis: for i, j being Nat

for T being non empty TopSpace

for s being Function of [:NAT,NAT:], the carrier of T holds

( x in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) iff ex n, m being Nat st

( ( i <= n or j <= m ) & x = s . (n,m) ) )

let i, j be Nat; :: thesis: for T being non empty TopSpace

for s being Function of [:NAT,NAT:], the carrier of T holds

( x in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) iff ex n, m being Nat st

( ( i <= n or j <= m ) & x = s . (n,m) ) )

let T be non empty TopSpace; :: thesis: for s being Function of [:NAT,NAT:], the carrier of T holds

( x in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) iff ex n, m being Nat st

( ( i <= n or j <= m ) & x = s . (n,m) ) )

let s be Function of [:NAT,NAT:], the carrier of T; :: thesis: ( x in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) iff ex n, m being Nat st

( ( i <= n or j <= m ) & x = s . (n,m) ) )

( ( i <= n or j <= m ) & x = s . (n,m) ) ; :: thesis: x in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):])

then consider n, m being Nat such that

A6: ( i <= n or j <= m ) and

A7: x = s . (n,m) ;

( n in NAT & m in NAT ) by ORDINAL1:def 12;

then A8: [n,m] in [:NAT,NAT:] by ZFMISC_1:def 2;

not [n,m] in [:(Segm i),(Segm j):]

A10: x = s . [n,m] by BINOP_1:def 1, A7;

[n,m] in dom s by A8, FUNCT_2:def 1;

hence x in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) by A9, A10, FUNCT_1:def 6; :: thesis: verum

for T being non empty TopSpace

for s being Function of [:NAT,NAT:], the carrier of T holds

( x in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) iff ex n, m being Nat st

( ( i <= n or j <= m ) & x = s . (n,m) ) )

let i, j be Nat; :: thesis: for T being non empty TopSpace

for s being Function of [:NAT,NAT:], the carrier of T holds

( x in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) iff ex n, m being Nat st

( ( i <= n or j <= m ) & x = s . (n,m) ) )

let T be non empty TopSpace; :: thesis: for s being Function of [:NAT,NAT:], the carrier of T holds

( x in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) iff ex n, m being Nat st

( ( i <= n or j <= m ) & x = s . (n,m) ) )

let s be Function of [:NAT,NAT:], the carrier of T; :: thesis: ( x in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) iff ex n, m being Nat st

( ( i <= n or j <= m ) & x = s . (n,m) ) )

hereby :: thesis: ( ex n, m being Nat st

( ( i <= n or j <= m ) & x = s . (n,m) ) implies x in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) )

assume
ex n, m being Nat st ( ( i <= n or j <= m ) & x = s . (n,m) ) implies x in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) )

assume
x in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):])
; :: thesis: ex n, m being Nat st

( ( i <= n or j <= m ) & x = s . (n,m) )

then consider y being object such that

A1: y in dom s and

A2: y in [:NAT,NAT:] \ [:(Segm i),(Segm j):] and

A3: x = s . y by FUNCT_1:def 6;

reconsider z = y as Element of [:NAT,NAT:] by A1;

A4: ( not z `1 in Segm i or not z `2 in Segm j )

take n = n; :: thesis: ex m being Nat st

( ( i <= n or j <= m ) & x = s . (n,m) )

take m = m; :: thesis: ( ( i <= n or j <= m ) & x = s . (n,m) )

thus ( i <= n or j <= m ) by A4, NAT_1:44; :: thesis: x = s . (n,m)

z is pair by Th4;

hence x = s . (n,m) by A3, BINOP_1:def 1; :: thesis: verum

end;( ( i <= n or j <= m ) & x = s . (n,m) )

then consider y being object such that

A1: y in dom s and

A2: y in [:NAT,NAT:] \ [:(Segm i),(Segm j):] and

A3: x = s . y by FUNCT_1:def 6;

reconsider z = y as Element of [:NAT,NAT:] by A1;

A4: ( not z `1 in Segm i or not z `2 in Segm j )

proof

reconsider n = z `1 , m = z `2 as Nat ;
assume
( z `1 in Segm i & z `2 in Segm j )
; :: thesis: contradiction

then A5: [(z `1),(z `2)] in [:(Segm i),(Segm j):] by ZFMISC_1:def 2;

z is pair by Th4;

hence contradiction by A2, A5, XBOOLE_0:def 5; :: thesis: verum

end;then A5: [(z `1),(z `2)] in [:(Segm i),(Segm j):] by ZFMISC_1:def 2;

z is pair by Th4;

hence contradiction by A2, A5, XBOOLE_0:def 5; :: thesis: verum

take n = n; :: thesis: ex m being Nat st

( ( i <= n or j <= m ) & x = s . (n,m) )

take m = m; :: thesis: ( ( i <= n or j <= m ) & x = s . (n,m) )

thus ( i <= n or j <= m ) by A4, NAT_1:44; :: thesis: x = s . (n,m)

z is pair by Th4;

hence x = s . (n,m) by A3, BINOP_1:def 1; :: thesis: verum

( ( i <= n or j <= m ) & x = s . (n,m) ) ; :: thesis: x in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):])

then consider n, m being Nat such that

A6: ( i <= n or j <= m ) and

A7: x = s . (n,m) ;

( n in NAT & m in NAT ) by ORDINAL1:def 12;

then A8: [n,m] in [:NAT,NAT:] by ZFMISC_1:def 2;

not [n,m] in [:(Segm i),(Segm j):]

proof

then A9:
[n,m] in [:NAT,NAT:] \ [:(Segm i),(Segm j):]
by A8, XBOOLE_0:def 5;
assume
[n,m] in [:(Segm i),(Segm j):]
; :: thesis: contradiction

then ex a, b being object st

( a in Segm i & b in Segm j & [n,m] = [a,b] ) by ZFMISC_1:def 2;

then ( n in Segm i & m in Segm j ) by XTUPLE_0:1;

hence contradiction by A6, NAT_1:44; :: thesis: verum

end;then ex a, b being object st

( a in Segm i & b in Segm j & [n,m] = [a,b] ) by ZFMISC_1:def 2;

then ( n in Segm i & m in Segm j ) by XTUPLE_0:1;

hence contradiction by A6, NAT_1:44; :: thesis: verum

A10: x = s . [n,m] by BINOP_1:def 1, A7;

[n,m] in dom s by A8, FUNCT_2:def 1;

hence x in s .: ([:NAT,NAT:] \ [:(Segm i),(Segm j):]) by A9, A10, FUNCT_1:def 6; :: thesis: verum