let x be object ; :: thesis: for X, Y being set holds pi ((X \/ Y),x) = (pi (X,x)) \/ (pi (Y,x))
let X, Y be set ; :: thesis: pi ((X \/ Y),x) = (pi (X,x)) \/ (pi (Y,x))
thus pi ((X \/ Y),x) c= (pi (X,x)) \/ (pi (Y,x)) :: according to XBOOLE_0:def 10 :: thesis: (pi (X,x)) \/ (pi (Y,x)) c= pi ((X \/ Y),x)

proof

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;
( f in X or f in Y ) by A1, XBOOLE_0:def 3;
then ( y in pi (X,x) or y in pi (Y,x) ) by A2, Def6;
hence y in (pi (X,x)) \/ (pi (Y,x)) by XBOOLE_0:def 3; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (pi (X,x)) \/ (pi (Y,x)) or y in pi ((X \/ Y),x) )
assume y in (pi (X,x)) \/ (pi (Y,x)) ; :: thesis: y in pi ((X \/ Y),x)
then A3: ( y in pi (X,x) or y in pi (Y,x) ) by XBOOLE_0:def 3;

A4: now :: thesis: ( y in pi (X,x) implies y in pi ((X \/ Y),x) )

assume y in pi (X,x) ; :: thesis: y in pi ((X \/ Y),x)
then consider f being Function such that
A5: f in X and
A6: y = f . x by Def6;
f in X \/ Y by A5, XBOOLE_0:def 3;
hence y in pi ((X \/ Y),x) by A6, Def6; :: thesis: verum

end;

now :: thesis: ( not y in pi (X,x) implies y in pi ((X \/ Y),x) )

assume not y in pi (X,x) ; :: thesis: y in pi ((X \/ Y),x)
then consider f being Function such that
A7: f in Y and
A8: y = f . x by A3, Def6;
f in X \/ Y by A7, XBOOLE_0:def 3;
hence y in pi ((X \/ Y),x) by A8, Def6; :: thesis: verum

end;

hence y in pi ((X \/ Y),x) by A4; :: thesis: verum