set f = the BilinearOperator of X,Y,Z;
the BilinearOperator of X,Y,Z in BilinearOperators (X,Y,Z) by Def6;
hence not BilinearOperators (X,Y,Z) is empty ; :: thesis: BilinearOperators (X,Y,Z) is functional
let x be object ; :: according to FUNCT_1:def 13 :: thesis: ( not x in BilinearOperators (X,Y,Z) or x is set )
assume x in BilinearOperators (X,Y,Z) ; :: thesis: x is set
hence x is set ; :: thesis: verum