let f, g be PartFunc of F₁(),F₂(); :: thesis: ( dom f = F₃() & ( for c being Element of F₁() st c in dom f holds
f /. c = F₄(c) ) & dom g = F₃() & ( for c being Element of F₁() st c in dom g holds
g /. c = F₄(c) ) implies f = g )
assume that
A1: dom f = F₃() and
A2: for c being Element of F₁() st c in dom f holds
f /. c = F₄(c) and
A3: dom g = F₃() and
A4: for c being Element of F₁() st c in dom g holds
g /. c = F₄(c) ; :: thesis: f = g

now :: thesis: for c being Element of F₁() st c in dom f holds
f /. c = g /. c

let c be Element of F₁(); :: thesis: ( c in dom f implies f /. c = g /. c )
assume A5: c in dom f ; :: thesis: f /. c = g /. c
hence f /. c = F₄(c) by A2
.= g /. c by A1, A3, A4, A5 ;
:: thesis: verum

end;

hence f = g by A1, A3, Th1; :: thesis: verum