let S be Sequence; :: thesis: ( dom S = NAT implies ( S . NAT = {} & last S = {} ) )
assume A1: dom S = NAT ; :: thesis: ( S . NAT = {} & last S = {} )
not NAT in NAT ;
hence S . NAT = {} by A1, FUNCT_1:def 2; :: thesis: last S = {}
hence last S = {} by A1, Th90; :: thesis: verum