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