let X be set ; :: thesis: for A1, A2 being SetSequence of X holds Union (A1 (\/) A2) = (Union A1) \/ (Union A2)
let A1, A2 be SetSequence of X; :: thesis: Union (A1 (\/) A2) = (Union A1) \/ (Union A2)
thus Union (A1 (\/) A2) c= (Union A1) \/ (Union A2) :: according to XBOOLE_0:def 10 :: thesis: (Union A1) \/ (Union A2) c= Union (A1 (\/) A2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union (A1 (\/) A2) or x in (Union A1) \/ (Union A2) )
assume x in Union (A1 (\/) A2) ; :: thesis: x in (Union A1) \/ (Union A2)
then consider n1 being Nat such that
A1: x in (A1 (\/) A2) . n1 by PROB_1:12;
A2: x in (A1 . n1) \/ (A2 . n1) by A1, Def2;

per cases ( x in A1 . n1 or x in A2 . n1 ) by A2, XBOOLE_0:def 3;

suppose x in A1 . n1 ; :: thesis: x in (Union A1) \/ (Union A2)

then x in Union A1 by PROB_1:12;
hence x in (Union A1) \/ (Union A2) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x in A2 . n1 ; :: thesis: x in (Union A1) \/ (Union A2)

then x in Union A2 by PROB_1:12;
hence x in (Union A1) \/ (Union A2) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Union A1) \/ (Union A2) or x in Union (A1 (\/) A2) )
assume A3: x in (Union A1) \/ (Union A2) ; :: thesis: x in Union (A1 (\/) A2)

per cases ( x in Union A1 or x in Union A2 ) by A3, XBOOLE_0:def 3;

suppose x in Union A1 ; :: thesis: x in Union (A1 (\/) A2)

then consider n2 being Nat such that
A4: x in A1 . n2 by PROB_1:12;
x in (A1 . n2) \/ (A2 . n2) by A4, XBOOLE_0:def 3;
then x in (A1 (\/) A2) . n2 by Def2;
hence x in Union (A1 (\/) A2) by PROB_1:12; :: thesis: verum

end;

suppose x in Union A2 ; :: thesis: x in Union (A1 (\/) A2)

then consider n3 being Nat such that
A5: x in A2 . n3 by PROB_1:12;
x in (A1 . n3) \/ (A2 . n3) by A5, XBOOLE_0:def 3;
then x in (A1 (\/) A2) . n3 by Def2;
hence x in Union (A1 (\/) A2) by PROB_1:12; :: thesis: verum

end;

end;