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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union (A (\/) A1) or x in A \/ (Union A1) )
assume A1: x in Union (A (\/) A1) ; :: thesis: x in A \/ (Union A1)
A2: ( x in A or ex k being Nat st x in A1 . k )

proof

consider k being Nat such that
A3: x in (A (\/) A1) . k by A1, PROB_1:12;
x in A \/ (A1 . k) by A3, Def6;
then ( x in A or x in A1 . k ) by XBOOLE_0:def 3;
hence ( x in A or ex k being Nat st x in A1 . k ) ; :: thesis: verum

end;

per cases ( x in A or ex k being Nat st x in A1 . k ) by A2;

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

hence x in A \/ (Union A1) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose ex k being Nat st x in A1 . k ; :: thesis: x in A \/ (Union A1)

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

end;

end;

end;

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

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

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

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

end;

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

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

end;

end;