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 Th17
.= Union (Partial_Union A1) by Th22
.= Union A1 by Th17 ; :: thesis: verum