assume not P ^ E is empty ; :: thesis: contradiction
then consider a being object such that
A1: a in P ^ E ;
consider p, q being FinSequence such that
( a = p ^ q & p in P ) and
A2: q in E by A1, Def2;
thus contradiction by A2; :: thesis: verum