let I be set ; :: thesis: for Y being ManySortedSet of I
for X being V8 ManySortedSet of I st ( for x being ManySortedSet of I holds
( x in X iff x in Y ) ) holds
X = Y
let Y be ManySortedSet of I; :: thesis: for X being V8 ManySortedSet of I st ( for x being ManySortedSet of I holds
( x in X iff x in Y ) ) holds
X = Y
let X be V8 ManySortedSet of I; :: thesis: ( ( for x being ManySortedSet of I holds
( x in X iff x in Y ) ) implies X = Y )
assume A1: for x being ManySortedSet of I holds
( x in X iff x in Y ) ; :: thesis: X = Y
deffunc H₁( set ) -> set = X . $1;
A2: for i being set st i in I holds
H₁(i) <> {} by Def16;
consider f being ManySortedSet of I such that
A3: for i being set st i in I holds
f . i in H₁(i) from PBOOLE:sch 1(A2);

now

let i be set ; :: thesis: ( i in I implies X . i = Y . i )
assume A4: i in I ; :: thesis: X . i = Y . i

now

let e be set ; :: thesis: ( ( e in X . i implies e in Y . i ) & ( e in Y . i implies e in X . i ) )
deffunc H₂( set ) -> set = IFEQ i,$1,e,(f . $1);
consider g being Function such that
A5: dom g = I and
A6: for u being set st u in I holds
g . u = H₂(u) from FUNCT_1:sch 3();
reconsider g = g as ManySortedSet of I by A5, Def3;
A7: g . i = IFEQ i,i,e,(f . i) by A4, A6
.= e by FUNCOP_1:def 8 ;

hereby :: thesis: ( e in Y . i implies e in X . i )

assume A8: e in X . i ; :: thesis: e in Y . i
g in X

proof

let u be set ; :: according to PBOOLE:def 4 :: thesis: ( u in I implies g . u in X . u )
assume A9: u in I ; :: thesis: g . u in X . u

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

suppose u = i ; :: thesis: g . u in X . u

hence g . u in X . u by A7, A8; :: thesis: verum

end;

suppose A10: u <> i ; :: thesis: g . u in X . u

g . u = IFEQ i,u,e,(f . u) by A6, A9
.= f . u by A10, FUNCOP_1:def 8 ;
hence g . u in X . u by A3, A9; :: thesis: verum

end;

end;

end;

then g in Y by A1;
hence e in Y . i by A4, A7, Def4; :: thesis: verum

end;

assume A11: e in Y . i ; :: thesis: e in X . i
g in Y

proof

let u be set ; :: according to PBOOLE:def 4 :: thesis: ( u in I implies g . u in Y . u )
assume A12: u in I ; :: thesis: g . u in Y . u

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

suppose u = i ; :: thesis: g . u in Y . u

hence g . u in Y . u by A7, A11; :: thesis: verum

end;

suppose A13: u <> i ; :: thesis: g . u in Y . u

f in X by A3, Def4;
then A14: f in Y by A1;
g . u = IFEQ i,u,e,(f . u) by A6, A12
.= f . u by A13, FUNCOP_1:def 8 ;
hence g . u in Y . u by A12, A14, Def4; :: thesis: verum

end;

end;

end;

then g in X by A1;
hence e in X . i by A4, A7, Def4; :: thesis: verum

end;

hence X . i = Y . i by TARSKI:2; :: thesis: verum

end;

hence X = Y by Th3; :: thesis: verum