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 and
A2: y = f . x by Def6;
A3: f in X by A1, XBOOLE_0:def 4;
A4: f in Y by A1, XBOOLE_0:def 4;
A5: y in pi X,x by A2, A3, Def6;
y in pi Y,x by A2, A4, Def6;
hence y in (pi X,x) /\ (pi Y,x) by A5, XBOOLE_0:def 4; :: thesis: verum