let x be object ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( x in s .: (square-uparrow n) iff ex i, j being Nat st

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

( n <= i & n <= j & x = s . (i,j) ) ; :: thesis: 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; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: ( x in s .: (square-uparrow n) iff ex i, j being Nat st

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

hereby :: thesis: ( ex i, j being Nat st

( n <= i & n <= j & x = s . (i,j) ) implies x in s .: (square-uparrow n) )

assume
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)
; :: thesis: 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; :: thesis: verum

end;( 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; :: thesis: verum

( n <= i & n <= j & x = s . (i,j) ) ; :: thesis: 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; :: thesis: verum