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

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

thus Union (Partial_Diff_Union A1) = Union (Partial_Union (Partial_Diff_Union A1)) by Th15

.= Union (Partial_Union A1) by Th19

.= Union A1 by Th15 ; :: thesis: verum

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

thus Union (Partial_Diff_Union A1) = Union (Partial_Union (Partial_Diff_Union A1)) by Th15

.= Union (Partial_Union A1) by Th19

.= Union A1 by Th15 ; :: thesis: verum