let F be PartFunc of C,REAL; :: thesis: ( F = ||.f.|| iff ( dom F = dom f & ( for c being Element of C st c in dom F holds
F . c = ||.(f /. c).|| ) ) )
thus ( F = ||.f.|| implies ( dom F = dom f & ( for c being Element of C st c in dom F holds
F . c = ||.(f /. c).|| ) ) ) by Def2; :: thesis: ( dom F = dom f & ( for c being Element of C st c in dom F holds
F . c = ||.(f /. c).|| ) implies F = ||.f.|| )
assume that
A4: dom F = dom f and
A5: for c being Element of C st c in dom F holds
F . c = ||.(f /. c).|| ; :: thesis: F = ||.f.||
for e being set st e in dom F holds
F . e = ||.(f /. e).||
proof
let e be set ; :: thesis: ( e in dom F implies F . e = ||.(f /. e).|| )
assume A6: e in dom F ; :: thesis: F . e = ||.(f /. e).||
dom F c= C by RELAT_1:def 18;
then reconsider c = e as Element of C by A6;
thus F . e = ||.(f /. c).|| by A6, A5
.= ||.(f /. e).|| ; :: thesis: verum
end;
hence F = ||.f.|| by A4, Def2; :: thesis: verum