let I be set ; :: thesis: for X, y being ManySortedSet of I holds
( X = {y} iff for x being ManySortedSet of I holds
( x in X iff x = y ) )
let X, y be ManySortedSet of I; :: thesis: ( X = {y} iff for x being ManySortedSet of I holds
( x in X iff x = y ) )
thus ( X = {y} implies for x being ManySortedSet of I holds
( x in X iff x = y ) ) :: thesis: ( ( for x being ManySortedSet of I holds
( x in X iff x = y ) ) implies X = {y} )

proof

assume A1: X = {y} ; :: thesis: for x being ManySortedSet of I holds
( x in X iff x = y )
let x be ManySortedSet of I; :: thesis: ( x in X iff x = y )
thus ( x in X implies x = y ) :: thesis: ( x = y implies x in X )

proof

assume A2: x in X ; :: thesis: x = y

now

let i be set ; :: thesis: ( i in I implies x . i = y . i )
assume A3: i in I ; :: thesis: x . i = y . i
then A4: x . i in X . i by A2, PBOOLE:def 4;
X . i = {(y . i)} by A1, A3, Def1;
hence x . i = y . i by A4, TARSKI:def 1; :: thesis: verum

end;

hence x = y by PBOOLE:3; :: thesis: verum

end;

assume A5: x = y ; :: thesis: x in X
let i be set ; :: according to PBOOLE:def 4 :: thesis: ( not i in I or x . i in X . i )
assume i in I ; :: thesis: x . i in X . i
then X . i = {(y . i)} by A1, Def1;
hence x . i in X . i by A5, TARSKI:def 1; :: thesis: verum

end;

assume A6: for x being ManySortedSet of I holds
( x in X iff x = y ) ; :: thesis: X = {y}
then A7: y in X ;

now

let i be set ; :: thesis: ( i in I implies X . i = {y} . i )
assume A8: i in I ; :: thesis: X . i = {y} . i

now

let a be set ; :: thesis: ( a in X . i iff a = y . i )
thus ( a in X . i iff a = y . i ) :: thesis: verum

proof

thus ( a in X . i implies a = y . i ) :: thesis: ( a = y . i implies a in X . i )

proof

assume A9: a in X . i ; :: thesis: a = y . i
A10: dom (i .--> a) = {i} by FUNCOP_1:19;
dom (y +* (i .--> a)) = I by A8, Th1;
then reconsider x1 = y +* (i .--> a) as ManySortedSet of I by PARTFUN1:def 4, RELAT_1:def 18;
i in {i} by TARSKI:def 1;
then A11: x1 . i = (i .--> a) . i by A10, FUNCT_4:14
.= a by FUNCOP_1:87 ;
x1 in X

proof

let q be set ; :: according to PBOOLE:def 4 :: thesis: ( not q in I or x1 . q in X . q )
assume A12: q in I ; :: thesis: x1 . q in X . q

per cases ( i = q or i <> q ) ;

suppose i = q ; :: thesis: x1 . q in X . q

hence x1 . q in X . q by A9, A11; :: thesis: verum

end;

suppose i <> q ; :: thesis: x1 . q in X . q

then not q in dom (i .--> a) by A10, TARSKI:def 1;
then x1 . q = y . q by FUNCT_4:12;
hence x1 . q in X . q by A7, A12, PBOOLE:def 4; :: thesis: verum

end;

end;

end;

hence a = y . i by A6, A11; :: thesis: verum

end;

assume a = y . i ; :: thesis: a in X . i
hence a in X . i by A7, A8, PBOOLE:def 4; :: thesis: verum

end;

end;

then X . i = {(y . i)} by TARSKI:def 1;
hence X . i = {y} . i by A8, Def1; :: thesis: verum

end;

hence X = {y} by PBOOLE:3; :: thesis: verum