let P, Q be set ; :: thesis: ( ( for f being object holds
( f in P iff f is PartFunc of D,RAT ) ) & ( for f being object holds
( f in Q iff f is PartFunc of D,RAT ) ) implies P = Q )
assume for f being object holds
( f in P iff f is PartFunc of D,RAT ) ; :: thesis: ( ex f being object st
( ( f in Q implies f is PartFunc of D,RAT ) implies ( f is PartFunc of D,RAT & 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 PartFunc of D,RAT ) ; :: 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