let X be set ; :: thesis: for A1, A2 being SetSequence of X holds Union (A1 (/\) A2) c= (Union A1) /\ (Union A2)
let A1, A2 be SetSequence of X; :: thesis: Union (A1 (/\) A2) c= (Union A1) /\ (Union A2)
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 n being Nat such that
A1: x in (A1 (/\) A2) . n by PROB_1:12;
A2: x in (A1 . n) /\ (A2 . n) by A1, Def1;
then x in A2 . n by XBOOLE_0:def 4;
then A3: x in Union A2 by PROB_1:12;
x in A1 . n by A2, XBOOLE_0:def 4;
then x in Union A1 by PROB_1:12;
hence x in (Union A1) /\ (Union A2) by A3, XBOOLE_0:def 4; :: thesis: verum