let X, Y be set ; :: thesis:
let B be c=-linear Subset of (PFuncs (X,Y)); :: thesis:
for x being set st x in B holds
x is Function ;
then reconsider f = union B as Function by Th34;

then reconsider D = B as functional non empty set ;

let x be set ; :: thesis:
assume x in { (dom g) where g is Element of D : verum } ; :: thesis:
then consider g being Element of D such that
A2: x = dom g ;
g in PFuncs (X,Y) by TARSKI:def 3;
then ex f being Function st
( g = f & dom f c= X & rng f c= Y ) by PARTFUN1:def 3;
hence x c= X by A2; :: thesis:

end;

let x be set ; :: thesis:
assume x in { (rng g) where g is Element of D : verum } ; :: thesis:
then consider g being Element of D such that
A4: x = rng g ;
g in PFuncs (X,Y) by TARSKI:def 3;
then ex f being Function st
( g = f & dom f c= X & rng f c= Y ) by PARTFUN1:def 3;
hence x c= Y by A4; :: thesis:

end;

rng f = union { (rng g) where g is Element of D : verum } by FUNCT_1:110;
then A5: rng f c= Y by A3, ZFMISC_1:76;
dom f = union { (dom g) where g is Element of D : verum } by FUNCT_1:110;
then dom f c= X by A1, ZFMISC_1:76;
hence union B in PFuncs (X,Y) by A5, PARTFUN1:def 3; :: thesis:

end;

end;