let Z1, Z2 be set ; :: thesis: ( ( for x being set holds
( x in Z1 iff ex F being PartFunc of REAL,REAL st
( x = F & F is_differentiable_on X & F `| X = f | X ) ) ) & ( for x being set holds
( x in Z2 iff ex F being PartFunc of REAL,REAL st
( x = F & F is_differentiable_on X & F `| X = f | X ) ) ) implies Z1 = Z2 )
assume that
A3: for x being set holds
( x in Z1 iff ex F being PartFunc of REAL,REAL st
( x = F & F is_differentiable_on X & F `| X = f | X ) ) and
A4: for x being set holds
( x in Z2 iff ex F being PartFunc of REAL,REAL st
( x = F & F is_differentiable_on X & F `| X = f | X ) ) ; :: thesis: Z1 = Z2
for x being object holds
( x in Z1 iff x in Z2 )

proof

let x be object ; :: thesis: ( x in Z1 iff x in Z2 )
( x in Z1 iff ex F being PartFunc of REAL,REAL st
( x = F & F is_differentiable_on X & F `| X = f | X ) ) by A3;
hence ( x in Z1 iff x in Z2 ) by A4; :: thesis: verum

end;

hence Z1 = Z2 by TARSKI:2; :: thesis: verum