let X be set ; :: thesis: for A1 being SetSequence of X holds Union (Partial_Union A1) = Union A1

let A1 be SetSequence of X; :: thesis: Union (Partial_Union A1) = Union A1

thus Union (Partial_Union A1) c= Union A1 :: according to XBOOLE_0:def 10 :: thesis: Union A1 c= Union (Partial_Union A1)

assume x in Union A1 ; :: thesis: x in Union (Partial_Union A1)

then consider n being Nat such that

A3: x in A1 . n by PROB_1:12;

x in (Partial_Union A1) . n by A3, Th13;

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

let A1 be SetSequence of X; :: thesis: Union (Partial_Union A1) = Union A1

thus Union (Partial_Union A1) c= Union A1 :: according to XBOOLE_0:def 10 :: thesis: Union A1 c= Union (Partial_Union A1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union A1 or x in Union (Partial_Union A1) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union (Partial_Union A1) or x in Union A1 )

assume x in Union (Partial_Union A1) ; :: thesis: x in Union A1

then consider n being Nat such that

A1: x in (Partial_Union A1) . n by PROB_1:12;

consider k being Nat such that

k <= n and

A2: x in A1 . k by A1, Th13;

thus x in Union A1 by A2, PROB_1:12; :: thesis: verum

end;assume x in Union (Partial_Union A1) ; :: thesis: x in Union A1

then consider n being Nat such that

A1: x in (Partial_Union A1) . n by PROB_1:12;

consider k being Nat such that

k <= n and

A2: x in A1 . k by A1, Th13;

thus x in Union A1 by A2, PROB_1:12; :: thesis: verum

assume x in Union A1 ; :: thesis: x in Union (Partial_Union A1)

then consider n being Nat such that

A3: x in A1 . n by PROB_1:12;

x in (Partial_Union A1) . n by A3, Th13;

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