let f1, f2 be ManySortedFunction of A,B; :: thesis: ( f1 . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds
f1 . s = F . s ) & f2 . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds
f2 . s = F . s ) implies f1 = f2 )
assume that
A9: ( f1 . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds
f1 . s = F . s ) ) and
A10: ( f2 . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds
f2 . s = F . s ) ) ; :: thesis: f1 = f2

now :: thesis: for x being object st x in I holds
f1 . x = f2 . x

let x be object ; :: thesis: ( x in I implies f1 . b₁ = f2 . b₁ )
assume A11: x in I ; :: thesis: f1 . b₁ = f2 . b₁

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

suppose x = i ; :: thesis: f1 . b₁ = f2 . b₁

hence f1 . x = f2 . x by A9, A10; :: thesis: verum

end;

suppose x <> i ; :: thesis: f1 . b₁ = f2 . b₁

then ( f1 . x = F . x & f2 . x = F . x ) by A9, A10, A11;
hence f1 . x = f2 . x ; :: thesis: verum

end;

end;

end;

hence f1 = f2 ; :: thesis: verum