let f be Function; :: thesis: ( f is involutive implies f .: (OtherPoints f) c= SomePoints f )
set F = FieldCover f;
set S = SomePoints f;
set O = OtherPoints f;
set ch = ChoiceOn (FieldCover f);
set A = field f;
set FP = fixpoints f;
set E = {{}};
assume B5: f is involutive ; :: thesis: f .: (OtherPoints f) c= SomePoints f
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (OtherPoints f) or y in SomePoints f )
assume B7: y in f .: (OtherPoints f) ; :: thesis: y in SomePoints f
then consider x being object such that
B0: ( x in dom f & x in OtherPoints f & y = f . x ) by FUNCT_1:def 6;
reconsider xx = x as set by TARSKI:1;
(f .: (OtherPoints f)) \ (rng f) = {} ;
then ( f .: (OtherPoints f) c= rng f & (rng f) null (dom f) c= field f ) by FOMODEL0:29;
then B8: y in field f by B7, TARSKI:def 3;
(OtherPoints f) \+\ (((field f) \ (fixpoints f)) /\ (rng (ChoiceOn (FieldCover f)))) = {} ;
then B66: x in ((field f) \ (fixpoints f)) /\ (rng (ChoiceOn (FieldCover f))) by B0, FOMODEL0:29;
consider X1 being object such that
B1: ( X1 in dom (ChoiceOn (FieldCover f)) & x = (ChoiceOn (FieldCover f)) . X1 ) by B66, FUNCT_1:def 3;
X1 in (FieldCover f) \ {{}} by B1, Lm9;
then X1 in FieldCover f ;
then consider x1 being Element of dom f such that
B2: ( X1 = {x1,(f . x1)} & x1 in dom f ) ;
B3: {x,(f . x)} = {x1,(f . x1)} by FOMODEL0:70, B5, B2, B1, Lm9;
( f . x in rng (ChoiceOn (FieldCover f)) implies x in fixpoints f )

proof

assume f . x in rng (ChoiceOn (FieldCover f)) ; :: thesis: x in fixpoints f
then consider X2 being object such that
C0: ( X2 in dom (ChoiceOn (FieldCover f)) & f . x = (ChoiceOn (FieldCover f)) . X2 ) by FUNCT_1:def 3;
reconsider X22 = X2 as set by TARSKI:1;
X2 in (FieldCover f) \ {{}} by C0, Lm9;
then X2 in FieldCover f ;
then consider x2 being Element of dom f such that
C1: ( X2 = {x2,(f . x2)} & x2 in dom f ) ;
f . x in X22 by C0, Lm9;
then (ChoiceOn (FieldCover f)) . X1 = (ChoiceOn (FieldCover f)) . X2 by B3, B2, C1, FOMODEL0:71, B5, B0;
then xx is_a_fixpoint_of f by C0, B0, B1, ABIAN:def 3;
hence x in fixpoints f by FOMODEL0:69; :: thesis: verum

end;

hence y in SomePoints f by B0, B8, XBOOLE_0:def 5; :: thesis: verum