for f, g being PartFunc of F₁(),F₂() st 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) ) holds
f = g