let X, Y be non empty TopSpace; :: thesis: 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); :: thesis: 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; :: thesis: 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; :: thesis: 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:86 ;
:: thesis: verum