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:56 ;
:: thesis: verum