let f be object ; :: according to FUNCT_1:def 13 :: thesis: ( not f in AddressParts T or f is set )

assume f in AddressParts T ; :: thesis: f is set

then ex I being Element of S st

( f = AddressPart I & InsCode I = T ) ;

hence f is set ; :: thesis: verum

assume f in AddressParts T ; :: thesis: f is set

then ex I being Element of S st

( f = AddressPart I & InsCode I = T ) ;

hence f is set ; :: thesis: verum