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 )
assume A1: g c= f ; :: thesis: g in PFuncs V,C
consider f1 being Function such that
A2: ( f1 = f & dom f1 c= V & rng f1 c= C ) by PARTFUN1:def 5;
reconsider g' = g as Function by A1;
( dom g' c= dom f1 & rng g' c= rng f1 ) by A1, A2, RELAT_1:25;
then ( dom g' c= V & rng g' c= C ) by A2, XBOOLE_1:1;
hence g in PFuncs V,C by PARTFUN1:def 5; :: thesis: verum