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₃() & ( for c being Element of F₁() st c in dom f holds
f . c = F₄(c) ) ) and
A2: ( dom g = F₃() & ( for c being Element of F₁() st c in dom g holds
g . c = F₄(c) ) ) ; :: thesis: f = g

now

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

end;

hence f = g by A1, A2, PARTFUN1:34; :: thesis: verum