let C, D be non empty set ; :: thesis: for d being Element of D

for f being PartFunc of C,D st ( for c being Element of C st c in dom f holds

f /. c = d ) holds

f = (dom f) --> d

let d be Element of D; :: thesis: for f being PartFunc of C,D st ( for c being Element of C st c in dom f holds

f /. c = d ) holds

f = (dom f) --> d

let f be PartFunc of C,D; :: thesis: ( ( for c being Element of C st c in dom f holds

f /. c = d ) implies f = (dom f) --> d )

assume A1: for c being Element of C st c in dom f holds

f /. c = d ; :: thesis: f = (dom f) --> d

for f being PartFunc of C,D st ( for c being Element of C st c in dom f holds

f /. c = d ) holds

f = (dom f) --> d

let d be Element of D; :: thesis: for f being PartFunc of C,D st ( for c being Element of C st c in dom f holds

f /. c = d ) holds

f = (dom f) --> d

let f be PartFunc of C,D; :: thesis: ( ( for c being Element of C st c in dom f holds

f /. c = d ) implies f = (dom f) --> d )

assume A1: for c being Element of C st c in dom f holds

f /. c = d ; :: thesis: f = (dom f) --> d

now :: thesis: for x being object st x in dom f holds

f . x = d

hence
f = (dom f) --> d
by FUNCOP_1:11; :: thesis: verumf . x = d

let x be object ; :: thesis: ( x in dom f implies f . x = d )

assume A2: x in dom f ; :: thesis: f . x = d

then reconsider x1 = x as Element of C ;

f /. x1 = d by A1, A2;

hence f . x = d by A2, PARTFUN1:def 6; :: thesis: verum

end;assume A2: x in dom f ; :: thesis: f . x = d

then reconsider x1 = x as Element of C ;

f /. x1 = d by A1, A2;

hence f . x = d by A2, PARTFUN1:def 6; :: thesis: verum