let I be set ; :: thesis: for X, Y being ManySortedSet of I st X is non-empty & X [= Y holds
X c= Y
let X, Y be ManySortedSet of I; :: thesis: ( X is non-empty & X [= Y implies X c= Y )
assume that
A1: X is non-empty and
A2: X [= Y ; :: thesis: X c= Y
deffunc H₁( set ) -> set = X . $1;
A3: for i being set st i in I holds
H₁(i) <> {} by A1, Def16;
consider f being ManySortedSet of I such that
A4: for i being set st i in I holds
f . i in H₁(i) from PBOOLE:sch 1(A3);
let i be set ; :: according to PBOOLE:def 2 :: thesis: ( i in I implies X . i c= Y . i )
assume A5: i in I ; :: thesis: X . i c= Y . i
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in X . i or e in Y . i )
deffunc H₂( set ) -> set = IFEQ (i,$1,e,(f . $1));
consider g being Function such that
A6: dom g = I and
A7: 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 A6, PARTFUN1:def 2, RELAT_1:def 18;
A8: g . i = IFEQ (i,i,e,(f . i)) by A5, A7
.= e by FUNCOP_1:def 8 ;
assume A9: 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 A10: 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 A8, A9; :: thesis: verum

end;

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

g . u = IFEQ (i,u,e,(f . u)) by A7, A10
.= f . u by A11, FUNCOP_1:def 8 ;
hence g . u in X . u by A4, A10; :: thesis: verum

end;

end;

end;

then g in Y by A2, Def14;
hence e in Y . i by A5, A8, Def4; :: thesis: verum