let A, B be non empty set ; :: thesis: for f being Function of A,B
for A0 being non empty Subset of A
for f0 being Function of A0,B st ( for c being Element of A st c in A0 holds
f . c = f0 . c ) holds
f | A0 = f0
let f be Function of A,B; :: thesis: for A0 being non empty Subset of A
for f0 being Function of A0,B st ( for c being Element of A st c in A0 holds
f . c = f0 . c ) holds
f | A0 = f0
let A0 be non empty Subset of A; :: thesis: for f0 being Function of A0,B st ( for c being Element of A st c in A0 holds
f . c = f0 . c ) holds
f | A0 = f0
let f0 be Function of A0,B; :: thesis: ( ( for c being Element of A st c in A0 holds
f . c = f0 . c ) implies f | A0 = f0 )
assume A1: for c being Element of A st c in A0 holds
f . c = f0 . c ; :: thesis: f | A0 = f0
reconsider g = f | A0 as Function of A0,B by Th32;
for c being Element of A0 holds g . c = f0 . c

proof

let c be Element of A0; :: thesis: g . c = f0 . c
thus g . c = f . c by FUNCT_1:49
.= f0 . c by A1 ; :: thesis: verum

end;

hence f | A0 = f0 by Th62; :: thesis: verum