the carrier of X --> 0 is linear-Functional of X by Th23;
hence not LinearFunctionals X is empty by Def7; :: thesis: LinearFunctionals X is functional
let x be object ; :: according to FUNCT_1:def 13 :: thesis: ( not x in LinearFunctionals X or x is set )
assume x in LinearFunctionals X ; :: thesis: x is set
hence x is set ; :: thesis: verum