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

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, PARTFUN1:def 2, RELAT_1:def 18;
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 1 :: 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 A2, A9; :: thesis: verum

end;

end;

end;

then g in Y by A3;
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 1 :: 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 A2, Def4;
then A14: f in Y by A3;
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 A3;
hence e in X . i by A4, A7, Def4; :: thesis: verum

end;

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

end;

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