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