let X, Y be non empty TopSpace; :: thesis: for N being net of
for i being Element of
for x being Point of holds the mapping of (commute N,x,(Omega Y)) . i = (the mapping of N . i) . x
let N be net of ; :: thesis: for i being Element of
for x being Point of holds the mapping of (commute N,x,(Omega Y)) . i = (the mapping of N . i) . x
let i be Element of ; :: thesis: for x being Point of holds the mapping of (commute N,x,(Omega Y)) . i = (the mapping of N . i) . x
let x be Point of ; :: 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