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

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