let I be set ; :: thesis: for A, B being ManySortedSet of I holds
( A cc= B iff A c= B )
let A, B be ManySortedSet of I; :: thesis: ( A cc= B iff A c= B )
thus ( A cc= B implies A c= B ) :: thesis: ( A c= B implies A cc= B )

proof

assume A1: A cc= B ; :: thesis: A c= B
let i be set ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or A . i c= B . i )
thus ( not i in I or A . i c= B . i ) by A1, Def2; :: thesis: verum

end;

assume A2: A c= B ; :: thesis: A cc= B
thus I c= I ; :: according to ALTCAT_2:def 2 :: thesis: for i being set st i in I holds
A . i c= B . i
thus for i being set st i in I holds
A . i c= B . i by A2, PBOOLE:def 2; :: thesis: verum