let I be non empty finite set ; :: thesis: for b1, b2 being ManySortedSet of
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 ; :: 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 )
assume A1: b1 . j <> b2 . j ; :: thesis: diff b1,b2 = (diff b1,(b2 +* j,(b1 . j))) + 1
{ 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 consider i being Element of I such that
A2: ( a = i & b1 . i <> b2 . i ) ;
thus a in I by A2; :: thesis: verum

end;

then reconsider F = { i where i is Element of I : b1 . i <> b2 . i } as finite set by FINSET_1:13;
set b3 = b2 +* j,(b1 . j);
{ 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 consider i being Element of I such that
A3: ( a = i & b1 . i <> (b2 +* j,(b1 . j)) . i ) ;
thus a in I by A3; :: 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;
A4: 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
A5: ( o = i & b1 . i <> b2 . i ) ;

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

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

then o in {j} by A5, 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 A5;
hence o in G \/ {j} by A5, 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 A6: o in G \/ {j} ; :: thesis: o in F

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

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

then consider i being Element of I such that
A7: ( o = i & 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 A7; :: 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 consider jj being Element of I such that
A9: ( 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 A4, CARD_2:54; :: thesis: verum