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

proof

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

proof

consider k being Nat such that
A3: x in (A1 (\) A) . k by A1, PROB_1:12;
x in (A1 . k) \ A by A3, Def8;
then ( x in A1 . k & not x in A ) by XBOOLE_0:def 5;
hence ex k being Nat st
( x in A1 . k & not x in A ) ; :: thesis: verum

end;

then x in Union A1 by PROB_1:12;
hence x in (Union A1) \ A by A2, XBOOLE_0:def 5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Union A1) \ A or x in Union (A1 (\) A) )
assume A4: x in (Union A1) \ A ; :: thesis: x in Union (A1 (\) A)
then A5: not x in A by XBOOLE_0:def 5;
A6: x in Union A1 by A4, XBOOLE_0:def 5;
ex k being Nat st x in (A1 (\) A) . k

proof

consider k being Nat such that
A7: x in A1 . k by A6, PROB_1:12;
x in (A1 . k) \ A by A5, A7, XBOOLE_0:def 5;
then x in (A1 (\) A) . k by Def8;
hence ex k being Nat st x in (A1 (\) A) . k ; :: thesis: verum

end;

hence x in Union (A1 (\) A) by PROB_1:12; :: thesis: verum