let P, Q be set ; :: thesis: ( ( for f being object holds
( f in P iff f is Function of D,ExtREAL ) ) & ( for f being object holds
( f in Q iff f is Function of D,ExtREAL ) ) implies P = Q )
assume for f being object holds
( f in P iff f is Function of D,ExtREAL ) ; :: thesis: ( ex f being object st
( ( f in Q implies f is Function of D,ExtREAL ) implies ( f is Function of D,ExtREAL & not f in Q ) ) or P = Q )
then A3: for f being object holds
( f in P iff S₁[f] ) ;
assume for f being object holds
( f in Q iff f is Function of D,ExtREAL ) ; :: thesis: P = Q
then A4: for f being object holds
( f in Q iff S₁[f] ) ;
thus P = Q from XBOOLE_0:sch 2(A3, A4); :: thesis: verum