let x be object ; :: thesis: for X, Y being set holds pi ((X /\ Y),x) c= (pi (X,x)) /\ (pi (Y,x))
let X, Y be set ; :: thesis: pi ((X /\ Y),x) c= (pi (X,x)) /\ (pi (Y,x))
let y be object ; :: 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