let i be Integer; :: thesis: ( a in P \ {(0. R)} & a = 0. R implies ( i = 1 iff i = 0 ) )

now :: thesis: ( a in P \ {(0. R)} & a = 0. R implies ( i = 1 iff i = 0 ) )

assume ( a in P \ {(0. R)} & a = 0. R ) ; :: thesis: ( i = 1 iff i = 0 )
then ( not a in {(0. R)} & a = 0. R ) by XBOOLE_0:def 5;
hence ( i = 1 iff i = 0 ) by TARSKI:def 1; :: thesis: verum

end;

hence ( a in P \ {(0. R)} & a = 0. R implies ( i = 1 iff i = 0 ) ) ; :: thesis: verum