let f be Function; :: thesis: ( f is involutive implies f .: () c= OtherPoints f )
set F = FieldCover f;
set A1 = SomePoints f;
set A2 = OtherPoints f;
set B1 = f .: ();
set ch = ChoiceOn ();
set A = dom f;
set FP = fixpoints f;
( (f .: ()) \ (rng f) = {} & () \+\ ((() \ ()) /\ (rng ())) = {} ) ;
then B4: ( f .: () c= rng f & OtherPoints f = (() \ ()) /\ (rng ()) ) by FOMODEL0:29;
assume B2: f is involutive ; :: thesis:
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: () or y in OtherPoints f )
assume B3: y in f .: () ; :: thesis:
then consider x being object such that
B0: ( x in dom f & x in SomePoints f & y = f . x ) by FUNCT_1:def 6;
set X = {x,(f . x)};
( {x,(f . x)} in FieldCover f & not {x,(f . x)} in ) by B0;
then {x,(f . x)} in () \ by XBOOLE_0:def 5;
then B1: {x,(f . x)} in dom () by Lm9;
then ( (ChoiceOn ()) . {x,(f . x)} in rng () & not x in rng () ) by ;
then ( (ChoiceOn ()) . {x,(f . x)} <> x & () . {x,(f . x)} in {x,(f . x)} ) by ;
then ( (ChoiceOn ()) . {x,(f . x)} = y & x <> f . x & f . y = x ) by ;
then ( y in rng () & not y is_a_fixpoint_of f ) by ;
then ( y in rng () & y in (rng f) null (dom f) & not y in fixpoints f ) by ;
then ( y in () \ () & y in rng () ) by XBOOLE_0:def 5;
hence y in OtherPoints f by ; :: thesis: verum