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 )

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

hence
y in SomePoints f
by B0, B8, XBOOLE_0:def 5; :: thesis: verum
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;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