let X, Y, x be set ; :: thesis: pi (X /\ Y),x c= (pi X,x) /\ (pi Y,x)
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in pi (X /\ Y),x or y in (pi X,x) /\ (pi Y,x) )
assume y in pi (X /\ Y),x ; :: thesis: y in (pi X,x) /\ (pi Y,x)
then consider f being Function such that
A1: ( f in X /\ Y & y = f . x ) by Def6;
( f in X & f in Y ) by A1, XBOOLE_0:def 4;
then ( y in pi X,x & y in pi Y,x ) by A1, Def6;
hence y in (pi X,x) /\ (pi Y,x) by XBOOLE_0:def 4; :: thesis: verum