let f be Function; :: thesis: ( f is involutive implies f .: (SomePoints f) c= OtherPoints f )

set F = FieldCover f;

set A1 = SomePoints f;

set A2 = OtherPoints f;

set B1 = f .: (SomePoints f);

set ch = ChoiceOn (FieldCover f);

set A = dom f;

set FP = fixpoints f;

( (f .: (SomePoints f)) \ (rng f) = {} & (OtherPoints f) \+\ (((field f) \ (fixpoints f)) /\ (rng (ChoiceOn (FieldCover f)))) = {} ) ;

then B4: ( f .: (SomePoints f) c= rng f & OtherPoints f = ((field f) \ (fixpoints f)) /\ (rng (ChoiceOn (FieldCover f))) ) by FOMODEL0:29;

assume B2: f is involutive ; :: thesis: f .: (SomePoints f) c= OtherPoints f

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (SomePoints f) or y in OtherPoints f )

assume B3: y in f .: (SomePoints f) ; :: thesis: y in OtherPoints f

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 (FieldCover f) \ {{}} by XBOOLE_0:def 5;

then B1: {x,(f . x)} in dom (ChoiceOn (FieldCover f)) by Lm9;

then ( (ChoiceOn (FieldCover f)) . {x,(f . x)} in rng (ChoiceOn (FieldCover f)) & not x in rng (ChoiceOn (FieldCover f)) ) by B0, XBOOLE_0:def 5, FUNCT_1:def 3;

then ( (ChoiceOn (FieldCover f)) . {x,(f . x)} <> x & (ChoiceOn (FieldCover f)) . {x,(f . x)} in {x,(f . x)} ) by B1, Lm9;

then ( (ChoiceOn (FieldCover f)) . {x,(f . x)} = y & x <> f . x & f . y = x ) by B0, B2, TARSKI:def 2, PARTIT_2:def 2;

then ( y in rng (ChoiceOn (FieldCover f)) & not y is_a_fixpoint_of f ) by B1, FUNCT_1:def 3, ABIAN:def 3;

then ( y in rng (ChoiceOn (FieldCover f)) & y in (rng f) null (dom f) & not y in fixpoints f ) by FOMODEL0:69, B3, B4;

then ( y in (field f) \ (fixpoints f) & y in rng (ChoiceOn (FieldCover f)) ) by XBOOLE_0:def 5;

hence y in OtherPoints f by B4, XBOOLE_0:def 4; :: thesis: verum

set F = FieldCover f;

set A1 = SomePoints f;

set A2 = OtherPoints f;

set B1 = f .: (SomePoints f);

set ch = ChoiceOn (FieldCover f);

set A = dom f;

set FP = fixpoints f;

( (f .: (SomePoints f)) \ (rng f) = {} & (OtherPoints f) \+\ (((field f) \ (fixpoints f)) /\ (rng (ChoiceOn (FieldCover f)))) = {} ) ;

then B4: ( f .: (SomePoints f) c= rng f & OtherPoints f = ((field f) \ (fixpoints f)) /\ (rng (ChoiceOn (FieldCover f))) ) by FOMODEL0:29;

assume B2: f is involutive ; :: thesis: f .: (SomePoints f) c= OtherPoints f

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (SomePoints f) or y in OtherPoints f )

assume B3: y in f .: (SomePoints f) ; :: thesis: y in OtherPoints f

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 (FieldCover f) \ {{}} by XBOOLE_0:def 5;

then B1: {x,(f . x)} in dom (ChoiceOn (FieldCover f)) by Lm9;

then ( (ChoiceOn (FieldCover f)) . {x,(f . x)} in rng (ChoiceOn (FieldCover f)) & not x in rng (ChoiceOn (FieldCover f)) ) by B0, XBOOLE_0:def 5, FUNCT_1:def 3;

then ( (ChoiceOn (FieldCover f)) . {x,(f . x)} <> x & (ChoiceOn (FieldCover f)) . {x,(f . x)} in {x,(f . x)} ) by B1, Lm9;

then ( (ChoiceOn (FieldCover f)) . {x,(f . x)} = y & x <> f . x & f . y = x ) by B0, B2, TARSKI:def 2, PARTIT_2:def 2;

then ( y in rng (ChoiceOn (FieldCover f)) & not y is_a_fixpoint_of f ) by B1, FUNCT_1:def 3, ABIAN:def 3;

then ( y in rng (ChoiceOn (FieldCover f)) & y in (rng f) null (dom f) & not y in fixpoints f ) by FOMODEL0:69, B3, B4;

then ( y in (field f) \ (fixpoints f) & y in rng (ChoiceOn (FieldCover f)) ) by XBOOLE_0:def 5;

hence y in OtherPoints f by B4, XBOOLE_0:def 4; :: thesis: verum