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 & 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 A1, 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 A2: ( y in pi X,x or y in pi Y,x ) by XBOOLE_0:def 3;

A3: now

assume y in pi X,x ; :: thesis: y in pi (X \/ Y),x
then consider f being Function such that
A4: ( f in X & y = f . x ) by Def6;
f in X \/ Y by A4, XBOOLE_0:def 3;
hence y in pi (X \/ Y),x by A4, 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
A5: ( f in Y & y = f . x ) by A2, Def6;
f in X \/ Y by A5, XBOOLE_0:def 3;
hence y in pi (X \/ Y),x by A5, Def6; :: thesis: verum

end;

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