let x be object ; for X, Y being set holds pi ((X \/ Y),x) = (pi (X,x)) \/ (pi (Y,x))
let X, Y be set ; pi ((X \/ Y),x) = (pi (X,x)) \/ (pi (Y,x))
thus
pi ((X \/ Y),x) c= (pi (X,x)) \/ (pi (Y,x))
XBOOLE_0:def 10 (pi (X,x)) \/ (pi (Y,x)) c= pi ((X \/ Y),x)proof
let y be
object ;
TARSKI:def 3 ( not y in pi ((X \/ Y),x) or y in (pi (X,x)) \/ (pi (Y,x)) )
assume
y in pi (
(X \/ Y),
x)
;
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;
verum
end;
let y be object ; TARSKI:def 3 ( 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))
; y in pi ((X \/ Y),x)
then A3:
( y in pi (X,x) or y in pi (Y,x) )
by XBOOLE_0:def 3;
hence
y in pi ((X \/ Y),x)
by A4; verum