let I be non empty finite set ; :: thesis:
let b1, b2 be ManySortedSet of I; :: thesis:
let j be Element of I; :: thesis:
set b3 = b2 +* (j,(b1 . j));
{ i where i is Element of I : b1 . i <> b2 . i } c= I

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in { i where i is Element of I : b1 . i <> b2 . i } ; :: thesis:
then ex i being Element of I st
( a = i & b1 . i <> b2 . i ) ;
hence a in I ; :: thesis:

end;

then reconsider F = { i where i is Element of I : b1 . i <> b2 . i } as finite set by FINSET_1:1;
{ i where i is Element of I : b1 . i <> (b2 +* (j,(b1 . j))) . i } c= I

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in { i where i is Element of I : b1 . i <> (b2 +* (j,(b1 . j))) . i } ; :: thesis:
then ex i being Element of I st
( a = i & b1 . i <> (b2 +* (j,(b1 . j))) . i ) ;
hence a in I ; :: thesis:

end;

then reconsider G = { i where i is Element of I : b1 . i <> (b2 +* (j,(b1 . j))) . i } as finite set by FINSET_1:1;
assume A1: b1 . j <> b2 . j ; :: thesis:
A2: F = G \/ {j}

proof

thus F c= G \/ {j} :: according to XBOOLE_0:def 10 :: thesis:

proof

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in F ; :: thesis:
then consider i being Element of I such that
A3: o = i and
A4: b1 . i <> b2 . i ;

per cases ;

suppose i = j ; :: thesis:

then o in {j} by A3, TARSKI:def 1;
hence o in G \/ {j} by XBOOLE_0:def 3; :: thesis:

end;

suppose i <> j ; :: thesis:

then (b2 +* (j,(b1 . j))) . i = b2 . i by FUNCT_7:32;
then i in G by A4;
hence o in G \/ {j} by A3, XBOOLE_0:def 3; :: thesis:

end;

end;

end;

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A5: o in G \/ {j} ; :: thesis:

per cases by A5, XBOOLE_0:def 3;

suppose o in G ; :: thesis:

then consider i being Element of I such that
A6: o = i and
A7: b1 . i <> (b2 +* (j,(b1 . j))) . i ;

now :: thesis:

assume A8: b1 . i = b2 . i ; :: thesis:
then i = j by A7, FUNCT_7:32;
hence contradiction by A1, A8; :: thesis:

end;

hence o in F by A6; :: thesis:

end;

suppose o in {j} ; :: thesis:

then o = j by TARSKI:def 1;
hence o in F by A1; :: thesis:

end;

end;

end;

now :: thesis:

assume j in G ; :: thesis:
then A9: ex jj being Element of I st
( jj = j & b1 . jj <> (b2 +* (j,(b1 . j))) . jj ) ;
dom b2 = I by PARTFUN1:def 2;
hence contradiction by A9, FUNCT_7:31; :: thesis:

end;

hence diff (b1,b2) = (diff (b1,(b2 +* (j,(b1 . j))))) + 1 by A2, CARD_2:41; :: thesis: