let h, g be Function; :: thesis: ( dom h = dom f & ( for c being object st c in dom h holds
h . c = r * (f . c) ) & dom g = dom f & ( for c being object st c in dom g holds
g . c = r * (f . c) ) implies h = g )
assume that
A1: dom h = dom f and
A2: for c being object st c in dom h holds
h . c = H₁(c) and
A3: dom g = dom f and
A4: for c being object st c in dom g holds
g . c = H₁(c) ; :: thesis: h = g

now :: thesis: for x being object st x in dom h holds
h . x = g . x

let x be object ; :: thesis: ( x in dom h implies h . x = g . x )
assume A5: x in dom h ; :: thesis: h . x = g . x
hence h . x = H₁(x) by A2
.= g . x by A1, A3, A4, A5 ;
:: thesis: verum

end;

hence h = g by A1, A3; :: thesis: verum