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 . b1 = f2 . b1 )
assume A11: x in I ; :: thesis: f1 . b1 = f2 . b1
per cases ( x = i or x <> i ) ;
suppose x = i ; :: thesis: f1 . b1 = f2 . b1
hence f1 . x = f2 . x by A9, A10; :: thesis: verum
end;
suppose x <> i ; :: thesis: f1 . b1 = f2 . b1
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