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

proof

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

end;

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

proof

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

end;

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

proof

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

proof

let o be set ; :: according to TARSKI:def 3 :: thesis: ( not o in F or o in G \/ {j} )
assume o in F ; :: thesis: o in G \/ {j}
then consider i being Element of I such that
A3: o = i and
A4: b1 . i <> b2 . i ;

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

suppose i = j ; :: thesis: o in G \/ {j}

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

end;

suppose i <> j ; :: thesis: o in G \/ {j}

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

end;

end;

end;

let o be set ; :: according to TARSKI:def 3 :: thesis: ( not o in G \/ {j} or o in F )
assume A5: o in G \/ {j} ; :: thesis: o in F

per cases ( o in G or o in {j} ) by A5, XBOOLE_0:def 3;

suppose o in G ; :: thesis: o in F

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

now

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

end;

hence o in F by A6; :: thesis: verum

end;

suppose o in {j} ; :: thesis: o in F

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

end;

end;

end;

now

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

end;

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