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 object ; :: 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: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: ( 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:1;
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 object ; :: 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 (b2 +* (j,(b1 . j))) . i = b2 . i by FUNCT_7:32;
then i in G by A4;
hence o in G \/ {j} by ; :: thesis: verum
end;
end;
end;
let o be object ; :: 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 ;
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 :: thesis: not b1 . i = b2 . i
assume A8: b1 . i = b2 . i ; :: thesis: contradiction
then i = j by ;
hence contradiction by A1, A8; :: thesis: verum
end;
hence o in F by A6; :: thesis: verum
end;
end;
end;
now :: thesis: not j in G
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 2;
hence contradiction by A9, FUNCT_7:31; :: thesis: verum
end;
hence diff (b1,b2) = (diff (b1,(b2 +* (j,(b1 . j))))) + 1 by ; :: thesis: verum