let V, C be set ; :: thesis: for f being Element of PFuncs V,C
for g being set st g c= f holds
g in PFuncs V,C
let f be Element of PFuncs V,C; :: thesis: for g being set st g c= f holds
g in PFuncs V,C
let g be set ; :: thesis: ( g c= f implies g in PFuncs V,C )
consider f1 being Function such that
A1: f1 = f and
A2: dom f1 c= V and
A3: rng f1 c= C by PARTFUN1:def 5;
assume A4: g c= f ; :: thesis: g in PFuncs V,C
then reconsider g9 = g as Function ;
rng g9 c= rng f1 by A4, A1, RELAT_1:25;
then A5: rng g9 c= C by A3, XBOOLE_1:1;
dom g9 c= dom f1 by A4, A1, RELAT_1:25;
then dom g9 c= V by A2, XBOOLE_1:1;
hence g in PFuncs V,C by A5, PARTFUN1:def 5; :: thesis: verum