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
; BilinearOperators (X,Y,Z) is functional
let x be object ; FUNCT_1:def 13 ( not x in BilinearOperators (X,Y,Z) or x is set )
assume
x in BilinearOperators (X,Y,Z)
; x is set
hence
x is set
; verum