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