defpred S₁[ set ] means ex F being PartFunc of REAL ,REAL st
( $1 = F & F is_differentiable_on X & F `| X = f | X );
consider Z being set such that
A1: for x being set holds
( x in Z iff ( x in PFuncs REAL ,REAL & S<sub>1</sub>[x] ) ) from XBOOLE_0:sch 1();
take Z ; :: thesis: for x being set holds
( x in Z iff ex F being PartFunc of REAL ,REAL st
( x = F & F is_differentiable_on X & F `| X = f | X ) )
let x be set ; :: thesis: ( x in Z iff ex F being PartFunc of REAL ,REAL st
( x = F & F is_differentiable_on X & F `| X = f | X ) )
thus ( x in Z implies ex F being PartFunc of REAL ,REAL st
( x = F & F is_differentiable_on X & F `| X = f | X ) ) by A1; :: thesis: ( ex F being PartFunc of REAL ,REAL st
( x = F & F is_differentiable_on X & F `| X = f | X ) implies x in Z )
given F being PartFunc of REAL ,REAL such that A2: x = F and
A3: F is_differentiable_on X and
A4: F `| X = f | X ; :: thesis: x in Z
F in PFuncs REAL ,REAL by PARTFUN1:119;
hence x in Z by A1, A2, A3, A4; :: thesis: verum