let X, Y be non empty TopSpace; :: thesis: 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); :: thesis: for x being Point of X holds commute N,x,(Omega Y) is eventually-directed
let x be Point of X; :: thesis: 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));
:: thesis: 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
;
:: thesis: 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));
:: thesis: ( 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:59;
reconsider A =
Na,
C =
Nc as
Element of
(product (the carrier of X --> (Omega Y))) by YELLOW_1:def 5;
assume
j <= k
;
:: thesis: (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;
( the
mapping of
(commute N,x,(Omega Y)) . a = (the mapping of N . i) . x & the
mapping of
(commute N,x,(Omega Y)) . c = (the mapping of N . k) . x )
by Th24;
hence
(commute N,x,(Omega Y)) . i <= (commute N,x,(Omega Y)) . k
by A4, FUNCOP_1:13;
:: thesis: verum
end;
hence
commute N,x,(Omega Y) is eventually-directed
by WAYBEL_0:11; :: thesis: verum