let F1, F2 be Function; :: thesis: ( dom F1 = dom f & ( for x being object st x in dom F1 holds
F1 . x = |[(f . x)]| ) & dom F2 = dom f & ( for x being object st x in dom F2 holds
F2 . x = |[(f . x)]| ) implies F1 = F2 )
assume that
A1: dom F1 = dom f and
A2: for x being object st x in dom F1 holds
F1 . x = |[(f . x)]| and
A3: dom F2 = dom f and
A4: for x being object st x in dom F2 holds
F2 . x = |[(f . x)]| ; :: thesis: F1 = F2

now :: thesis: for x being set st x in dom F1 holds
F1 . x = F2 . x

let x be set ; :: thesis: ( x in dom F1 implies F1 . x = F2 . x )
assume A5: x in dom F1 ; :: thesis: F1 . x = F2 . x
hence F1 . x = |[(f . x)]| by A2
.= F2 . x by A1, A3, A4, A5 ;
:: thesis: verum

end;

hence F1 = F2 by A1, A3; :: thesis: verum