let X be set ; :: thesis: for A1 being SetSequence of X st A1 is non-descending holds
Partial_Union A1 = A1
let A1 be SetSequence of X; :: thesis: ( A1 is non-descending implies Partial_Union A1 = A1 )
assume A1 is non-descending ; :: thesis: Partial_Union A1 = A1
then for n being Element of NAT holds (Partial_Union A1) . n = A1 . n by Lm2;
hence Partial_Union A1 = A1 by FUNCT_2:63; :: thesis: verum