let I be set ; :: thesis: for A, B being ManySortedSet of I st A c= B holds
union A c= union B
let A, B be ManySortedSet of I; :: thesis: ( A c= B implies union A c= union B )
assume A1: A c= B ; :: thesis: union A c= union B
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or (union A) . i c= (union B) . i )
assume A2: i in I ; :: thesis: (union A) . i c= (union B) . i
then A . i c= B . i by A1;
then union (A . i) c= union (B . i) by ZFMISC_1:77;
then (union A) . i c= union (B . i) by A2, Def2;
hence (union A) . i c= (union B) . i by A2, Def2; :: thesis: verum