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 ) }
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 A6; :: thesis: verum
end;
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 A4; :: thesis: verum
end;
now :: thesis: for x being Point of it1 holds the BNbd of it1 . x = the BNbd of it2 . x
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 A3, A5, A7 ; :: thesis: verum
end;
hence it1 = it2 by A3, A5, FUNCT_2:63; :: thesis: verum