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

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