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