let X, Y be non empty TopSpace; for N being eventually-directed net of eventually-directed
for x being Point of holds commute N,x,(Omega Y) is eventually-directed
let N be eventually-directed net of eventually-directed ; for x being Point of holds commute N,x,(Omega Y) is eventually-directed
let x be Point of ; commute N,x,(Omega Y) is eventually-directed
set M = commute N,x,(Omega Y);
set L = (Omega Y) |^ the carrier of X;
for i being Element of ex j being Element of st
for k being Element of st j <= k holds
(commute N,x,(Omega Y)) . i <= (commute N,x,(Omega Y)) . k
proof
let i be
Element of ;
ex j being Element of st
for k being Element of st j <= k holds
(commute N,x,(Omega Y)) . i <= (commute N,x,(Omega Y)) . k
A1:
ContMaps X,
(Omega Y) is
SubRelStr of
(Omega Y) |^ the
carrier of
X
by WAYBEL24:def 3;
then
the
carrier of
(ContMaps X,(Omega Y)) c= the
carrier of
((Omega Y) |^ the carrier of X)
by YELLOW_0:def 13;
then A2:
RelStr(# the
carrier of
N,the
InternalRel of
N #)
= RelStr(# the
carrier of
(commute N,x,(Omega Y)),the
InternalRel of
(commute N,x,(Omega Y)) #)
by Def3;
then reconsider a =
i as
Element of ;
consider b being
Element of
such that A3:
for
c being
Element of st
b <= c holds
N . a <= N . c
by WAYBEL_0:11;
reconsider j =
b as
Element of
by A2;
take
j
;
for k being Element of st j <= k holds
(commute N,x,(Omega Y)) . i <= (commute N,x,(Omega Y)) . k
let k be
Element of ;
( j <= k implies (commute N,x,(Omega Y)) . i <= (commute N,x,(Omega Y)) . k )
reconsider c =
k as
Element of
by A2;
reconsider Na =
N . a,
Nc =
N . c as
Element of
by A1, YELLOW_0:59;
reconsider A =
Na,
C =
Nc as
Element of
by YELLOW_1:def 5;
assume
j <= k
;
(commute N,x,(Omega Y)) . i <= (commute N,x,(Omega Y)) . k
then
b <= c
by A2, YELLOW_0:1;
then
N . a <= N . c
by A3;
then
Na <= Nc
by A1, YELLOW_0:60;
then
A <= C
by YELLOW_1:def 5;
then A4:
A . x <= C . x
by WAYBEL_3:28;
A5:
the
mapping of
(commute N,x,(Omega Y)) . c = (the mapping of N . k) . x
by Th24;
the
mapping of
(commute N,x,(Omega Y)) . a = (the mapping of N . i) . x
by Th24;
hence
(commute N,x,(Omega Y)) . i <= (commute N,x,(Omega Y)) . k
by A4, A5, FUNCOP_1:13;
verum
end;
hence
commute N,x,(Omega Y) is eventually-directed
by WAYBEL_0:11; verum