defpred S₁[ object ] 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 object 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 & F is_differentiable_on X & F `| X = f | X ) ; :: thesis: x in Z
F in PFuncs (REAL,REAL) by PARTFUN1:45;
hence x in Z by A1, A2; :: thesis: verum