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

{ i where i is Element of I : b1 . i <> (b2 +* (j,(b1 . j))) . i } c= I

assume A1: b1 . j <> b2 . j ; :: thesis: diff (b1,b2) = (diff (b1,(b2 +* (j,(b1 . j))))) + 1

A2: F = G \/ {j}

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

then reconsider F = { i where i is Element of I : b1 . i <> b2 . i } as finite set by FINSET_1:1;
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;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

{ i where i is Element of I : b1 . i <> (b2 +* (j,(b1 . j))) . i } c= I

proof

then reconsider G = { i where i is Element of I : b1 . i <> (b2 +* (j,(b1 . j))) . i } as finite set by FINSET_1:1;
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;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

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

assume A5: o in G \/ {j} ; :: thesis: o in F

end;proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in G \/ {j} or o in F )
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 ;

end;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 ;

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;

end;

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 ;

end;A6: o = i and

A7: b1 . i <> (b2 +* (j,(b1 . j))) . i ;

now :: thesis: not b1 . i = b2 . i

hence
o in F
by A6; :: thesis: verumassume A8:
b1 . i = b2 . i
; :: thesis: contradiction

then i = j by A7, FUNCT_7:32;

hence contradiction by A1, A8; :: thesis: verum

end;then i = j by A7, FUNCT_7:32;

hence contradiction by A1, A8; :: thesis: verum

now :: thesis: not j in G

hence
diff (b1,b2) = (diff (b1,(b2 +* (j,(b1 . j))))) + 1
by A2, CARD_2:41; :: thesis: verumassume
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;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