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