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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in Union (A (/\) A1) or x in A /\ (Union A1) )
assume x in Union (A (/\) A1) ; :: thesis: x in A /\ (Union A1)
then consider n being Element of NAT such that
A1: x in (A (/\) A1) . n by PROB_1:25;
A2: x in A /\ (A1 . n) by A1, Def5;
then x in A1 . n by XBOOLE_0:def 4;
then A3: x in Union A1 by PROB_1:25;
x in A by A2, XBOOLE_0:def 4;
hence x in A /\ (Union A1) by A3, XBOOLE_0:def 4; :: thesis: verum

end;

let x be set ; :: 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)
then x in Union A1 by XBOOLE_0:def 4;
then consider n being Element of NAT such that
A5: x in A1 . n by PROB_1:25;
x in A by A4, XBOOLE_0:def 4;
then x in A /\ (A1 . n) by A5, XBOOLE_0:def 4;
then x in (A (/\) A1) . n by Def5;
hence x in Union (A (/\) A1) by PROB_1:25; :: thesis: verum