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) ) )
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 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 )
proof
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;
reconsider n = z `1 , m = z `2 as Nat ;
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;
assume ex n, m being Nat st
( ( 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
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 A9: [n,m] in [:NAT,NAT:] \ [:(Segm i),(Segm j):] by A8, XBOOLE_0:def 5;
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