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