let P, Q be set ; :: thesis: ( ( for f being object holds

( f in P iff f is PartFunc of D,NAT ) ) & ( for f being object holds

( f in Q iff f is PartFunc of D,NAT ) ) implies P = Q )

assume for f being object holds

( f in P iff f is PartFunc of D,NAT ) ; :: thesis: ( ex f being object st

( ( f in Q implies f is PartFunc of D,NAT ) implies ( f is PartFunc of D,NAT & not f in Q ) ) or P = Q )

then A3: for f being object holds

( f in P iff S_{1}[f] )
;

assume for f being object holds

( f in Q iff f is PartFunc of D,NAT ) ; :: thesis: P = Q

then A4: for f being object holds

( f in Q iff S_{1}[f] )
;

thus P = Q from XBOOLE_0:sch 2(A3, A4); :: thesis: verum

( f in P iff f is PartFunc of D,NAT ) ) & ( for f being object holds

( f in Q iff f is PartFunc of D,NAT ) ) implies P = Q )

assume for f being object holds

( f in P iff f is PartFunc of D,NAT ) ; :: thesis: ( ex f being object st

( ( f in Q implies f is PartFunc of D,NAT ) implies ( f is PartFunc of D,NAT & not f in Q ) ) or P = Q )

then A3: for f being object holds

( f in P iff S

assume for f being object holds

( f in Q iff f is PartFunc of D,NAT ) ; :: thesis: P = Q

then A4: for f being object holds

( f in Q iff S

thus P = Q from XBOOLE_0:sch 2(A3, A4); :: thesis: verum