let X, Y, x 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 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;
( 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 set ; :: 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

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

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