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
A4: the carrier of it1 = the carrier of T and
A5: 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
A6: the carrier of it2 = the carrier of T and
A7: 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
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 ) }

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

end;

A9: 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

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

end;

now

let 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 A4, A6, A9 ; :: thesis: verum

end;

hence it1 = it2 by A4, A6, FUNCT_2:113; :: thesis: verum