let I, J be set ; :: thesis: for A being ManySortedSet of
for B being ManySortedSet of st A cc= B holds
~ A cc= ~ B
let A be ManySortedSet of ; :: thesis: for B being ManySortedSet of st A cc= B holds
~ A cc= ~ B
let B be ManySortedSet of ; :: thesis: ( A cc= B implies ~ A cc= ~ B )
assume that
A1: [:I,I:] c= [:J,J:] and
A2: for x being set st x in [:I,I:] holds
A . x c= B . x ; :: according to ALTCAT_2:def 2 :: thesis: ~ A cc= ~ B
thus [:I,I:] c= [:J,J:] by A1; :: according to ALTCAT_2:def 2 :: thesis: for b₁ being set holds
( not b₁ in [:I,I:] or (~ A) . b₁ c= (~ B) . b₁ )
let x be set ; :: thesis: ( not x in [:I,I:] or (~ A) . x c= (~ B) . x )
assume x in [:I,I:] ; :: thesis: (~ A) . x c= (~ B) . x
then consider x1, x2 being set such that
A3: ( x1 in I & x2 in I & x = [x1,x2] ) by ZFMISC_1:def 2;
A4: [x2,x1] in [:I,I:] by A3, ZFMISC_1:def 2;
( dom A = [:I,I:] & dom B = [:J,J:] ) by PARTFUN1:def 4;
then ( (~ A) . x1,x2 = A . x2,x1 & (~ B) . x1,x2 = B . x2,x1 ) by A1, A4, FUNCT_4:def 2;
hence (~ A) . x c= (~ B) . x by A2, A3, A4; :: thesis: verum