defpred S₁[ object ] means ex f being continuous PartFunc of REAL,Y st
( $1 = f & dom f = X );
consider IT being set such that
A1: for x being object holds
( x in IT iff ( x in BoundedFunctions (X,Y) & S₁[x] ) ) from XBOOLE_0:sch 1();
take IT ; :: thesis: ( IT is Subset of (R_VectorSpace_of_BoundedFunctions (X,Y)) & ( for x being set holds
( x in IT iff ex f being continuous PartFunc of REAL,Y st
( x = f & dom f = X ) ) ) )
for x being object st x in IT holds
x in BoundedFunctions (X,Y) by A1;
hence IT is Subset of (R_VectorSpace_of_BoundedFunctions (X,Y)) by TARSKI:def 3; :: thesis: for x being set holds
( x in IT iff ex f being continuous PartFunc of REAL,Y st
( x = f & dom f = X ) )
let x be set ; :: thesis: ( x in IT iff ex f being continuous PartFunc of REAL,Y st
( x = f & dom f = X ) )
thus ( x in IT implies ex f being continuous PartFunc of REAL,Y st
( x = f & dom f = X ) ) by A1; :: thesis: ( ex f being continuous PartFunc of REAL,Y st
( x = f & dom f = X ) implies x in IT )
assume A2: ex f being continuous PartFunc of REAL,Y st
( x = f & dom f = X ) ; :: thesis: x in IT
then consider f being continuous PartFunc of REAL,Y such that
A3: ( x = f & dom f = X ) ;
f is bounded Function of X,Y by A3, Th9;
then x in BoundedFunctions (X,Y) by A3, RSSPACE4:def 5;
hence x in IT by A1, A2; :: thesis: verum