let x be set ; :: thesis: pi ({},x) = {}
consider y being Element of pi ({},x);
assume not pi ({},x) = {} ; :: thesis: contradiction
then ex f being Function st
( f in {} & y = f . x ) by Def6;
hence contradiction ; :: thesis: verum