let x be object ; for n being Nat
for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T holds
( x in s .: (square-uparrow n) iff ex i, j being Nat st
( n <= i & n <= j & x = s . (i,j) ) )
let n be Nat; for T being non empty TopSpace
for s being Function of [:NAT,NAT:], the carrier of T holds
( x in s .: (square-uparrow n) iff ex i, j being Nat st
( n <= i & n <= j & x = s . (i,j) ) )
let T be non empty TopSpace; for s being Function of [:NAT,NAT:], the carrier of T holds
( x in s .: (square-uparrow n) iff ex i, j being Nat st
( n <= i & n <= j & x = s . (i,j) ) )
let s be Function of [:NAT,NAT:], the carrier of T; ( x in s .: (square-uparrow n) iff ex i, j being Nat st
( n <= i & n <= j & x = s . (i,j) ) )
hereby ( ex i, j being Nat st
( n <= i & n <= j & x = s . (i,j) ) implies x in s .: (square-uparrow n) )
assume
x in s .: (square-uparrow n)
;
ex i, j being Nat st
( n <= i & n <= j & x = s . (i,j) )then consider y being
object such that A1:
y in dom s
and A2:
y in square-uparrow n
and A3:
x = s . y
by FUNCT_1:def 6;
reconsider z =
y as
Element of
[:NAT,NAT:] by A1;
consider i,
j being
Nat such that A4:
z `1 = i
and A5:
z `2 = j
and A6:
n <= i
and A7:
n <= j
by A2, Def3;
consider m1,
m2 being
object such that
m1 in NAT
and
m2 in NAT
and A8:
z = [m1,m2]
by ZFMISC_1:def 2;
x = s . (
i,
j)
by A4, A5, A8, A3, BINOP_1:def 1;
hence
ex
i,
j being
Nat st
(
n <= i &
n <= j &
x = s . (
i,
j) )
by A6, A7;
verum
end;
assume
ex i, j being Nat st
( n <= i & n <= j & x = s . (i,j) )
; x in s .: (square-uparrow n)
then consider i, j being Nat such that
A9:
n <= i
and
A10:
n <= j
and
A11:
x = s . (i,j)
;
A12:
dom s = [:NAT,NAT:]
by FUNCT_2:def 1;
A13:
( i in NAT & j in NAT )
by ORDINAL1:def 12;
A14:
x = s . [i,j]
by A11, BINOP_1:def 1;
( [i,j] `1 = i & [i,j] `2 = j & [i,j] in [:NAT,NAT:] )
by A13, ZFMISC_1:def 2;
then
[i,j] in square-uparrow n
by A9, A10, Def3;
hence
x in s .: (square-uparrow n)
by A12, A14, FUNCT_1:def 6; verum