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 3;
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:11;
then A5: rng g9 c= C by A3;
dom g9 c= dom f1 by A4, A1, RELAT_1:11;
then dom g9 c= V by A2;
hence g in PFuncs (V,C) by A5, PARTFUN1:def 3; :: thesis: verum