defpred S1[ object ] means $1 is MultilinearOperator of X,Y;
consider IT being set such that
A1:
for x being object holds
( x in IT iff ( x in Funcs ( the carrier of (product X), the carrier of Y) & S1[x] ) )
from XBOOLE_0:sch 1();
take
IT
; ( IT is Subset of (RealVectSpace ( the carrier of (product X),Y)) & ( for x being set holds
( x in IT iff x is MultilinearOperator of X,Y ) ) )
for x being object st x in IT holds
x in Funcs ( the carrier of (product X), the carrier of Y)
by A1;
hence
IT is Subset of (RealVectSpace ( the carrier of (product X),Y))
by TARSKI:def 3; for x being set holds
( x in IT iff x is MultilinearOperator of X,Y )
let x be set ; ( x in IT iff x is MultilinearOperator of X,Y )
thus
( x in IT implies x is MultilinearOperator of X,Y )
by A1; ( x is MultilinearOperator of X,Y implies x in IT )
assume A2:
x is MultilinearOperator of X,Y
; x in IT
then
x in Funcs ( the carrier of (product X), the carrier of Y)
by FUNCT_2:8;
hence
x in IT
by A1, A2; verum