let X, Y be non empty TopSpace; for N being net of ContMaps (X,(Omega Y))
for i being Element of N
for x being Point of X holds the mapping of (commute (N,x,(Omega Y))) . i = ( the mapping of N . i) . x
let N be net of ContMaps (X,(Omega Y)); for i being Element of N
for x being Point of X holds the mapping of (commute (N,x,(Omega Y))) . i = ( the mapping of N . i) . x
let i be Element of N; for x being Point of X holds the mapping of (commute (N,x,(Omega Y))) . i = ( the mapping of N . i) . x
let x be Point of X; the mapping of (commute (N,x,(Omega Y))) . i = ( the mapping of N . i) . x
A1:
the mapping of N in Funcs ( the carrier of N,(Funcs ( the carrier of X, the carrier of Y)))
by Lm4;
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;
hence the mapping of (commute (N,x,(Omega Y))) . i =
((commute the mapping of N) . x) . i
by Def3
.=
( the mapping of N . i) . x
by A1, FUNCT_6:56
;
verum