let n be Nat; :: thesis: for X being set
for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= (Partial_Union A1) . n
let X be set ; :: thesis: for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= (Partial_Union A1) . n
let A1 be SetSequence of X; :: thesis: (Partial_Diff_Union A1) . n c= (Partial_Union A1) . n
( (Partial_Diff_Union A1) . n c= A1 . n & A1 . n c= (Partial_Union A1) . n ) by Th9, Th17;
hence (Partial_Diff_Union A1) . n c= (Partial_Union A1) . n ; :: thesis: verum