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

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