let f be Function; ( 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
; f .: (OtherPoints f) c= SomePoints f
let y be object ; TARSKI:def 3 ( not y in f .: (OtherPoints f) or y in SomePoints f )
assume B7:
y in f .: (OtherPoints f)
; 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))
;
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;
verum
end;
hence
y in SomePoints f
by B0, B8, XBOOLE_0:def 5; verum