let it1, it2 be non empty strict FMT_Space_Str ; :: thesis: ( the carrier of it1 = the carrier of T & ( for x being Point of it1 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) & the carrier of it2 = the carrier of T & ( for x being Point of it2 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) implies it1 = it2 )

assume that

A3: the carrier of it1 = the carrier of T and

A4: for x being Point of it1 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } and

A5: the carrier of it2 = the carrier of T and

A6: for x being Point of it2 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ; :: thesis: it1 = it2

A7: for x being Element of it2 holds the BNbd of it2 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) }

assume that

A3: the carrier of it1 = the carrier of T and

A4: for x being Point of it1 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } and

A5: the carrier of it2 = the carrier of T and

A6: for x being Point of it2 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ; :: thesis: it1 = it2

A7: for x being Element of it2 holds the BNbd of it2 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) }

proof

A8:
for x being Element of it1 holds the BNbd of it1 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) }
let x be Element of it2; :: thesis: the BNbd of it2 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) }

the BNbd of it2 . x = U_FMT x ;

hence the BNbd of it2 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) } by A6; :: thesis: verum

end;the BNbd of it2 . x = U_FMT x ;

hence the BNbd of it2 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) } by A6; :: thesis: verum

proof

let x be Element of it1; :: thesis: the BNbd of it1 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) }

the BNbd of it1 . x = U_FMT x ;

hence the BNbd of it1 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) } by A4; :: thesis: verum

end;the BNbd of it1 . x = U_FMT x ;

hence the BNbd of it1 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) } by A4; :: thesis: verum

now :: thesis: for x being Point of it1 holds the BNbd of it1 . x = the BNbd of it2 . x

hence
it1 = it2
by A3, A5, FUNCT_2:63; :: thesis: verumlet x be Point of it1; :: thesis: the BNbd of it1 . x = the BNbd of it2 . x

thus the BNbd of it1 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) } by A8

.= the BNbd of it2 . x by A3, A5, A7 ; :: thesis: verum

end;thus the BNbd of it1 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) } by A8

.= the BNbd of it2 . x by A3, A5, A7 ; :: thesis: verum