let X, Y be non empty TopSpace; for N being eventually-directed net of ContMaps (X,(Omega Y))
for x being Point of X holds commute (N,x,(Omega Y)) is eventually-directed
let N be eventually-directed net of ContMaps (X,(Omega Y)); for x being Point of X holds commute (N,x,(Omega Y)) is eventually-directed
let x be Point of X; 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 (commute (N,x,(Omega Y))) ex j being Element of (commute (N,x,(Omega Y))) st
for k being Element of (commute (N,x,(Omega Y))) st j <= k holds
(commute (N,x,(Omega Y))) . i <= (commute (N,x,(Omega Y))) . k
proof
let i be
Element of
(commute (N,x,(Omega Y)));
ex j being Element of (commute (N,x,(Omega Y))) st
for k being Element of (commute (N,x,(Omega Y))) 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
N ;
consider b being
Element of
N such that A3:
for
c being
Element of
N st
b <= c holds
N . a <= N . c
by WAYBEL_0:11;
reconsider j =
b as
Element of
(commute (N,x,(Omega Y))) by A2;
take
j
;
for k being Element of (commute (N,x,(Omega Y))) st j <= k holds
(commute (N,x,(Omega Y))) . i <= (commute (N,x,(Omega Y))) . k
let k be
Element of
(commute (N,x,(Omega Y)));
( j <= k implies (commute (N,x,(Omega Y))) . i <= (commute (N,x,(Omega Y))) . k )
reconsider c =
k as
Element of
N by A2;
reconsider Na =
N . a,
Nc =
N . c as
Element of
((Omega Y) |^ the carrier of X) by A1, YELLOW_0:58;
reconsider A =
Na,
C =
Nc as
Element of
(product ( the carrier of X --> (Omega Y))) 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;
then
N . a <= N . c
by A3;
then
Na <= Nc
by A1, YELLOW_0:59;
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;
verum
end;
hence
commute (N,x,(Omega Y)) is eventually-directed
by WAYBEL_0:11; verum