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

per cases ( B <> {} or B = {} ) ;

suppose B <> {} ; :: thesis: union B in PFuncs (X,Y)

then reconsider D = B as functional non empty set ;

A1: now :: thesis: for x being set st x in { (dom g) where g is Element of D : verum } holds
x c= X

let x be set ; :: thesis: ( x in { (dom g) where g is Element of D : verum } implies x c= X )
assume x in { (dom g) where g is Element of D : verum } ; :: thesis: x c= X
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: verum

end;

A3: now :: thesis: for x being set st x in { (rng g) where g is Element of D : verum } holds
x c= Y

let x be set ; :: thesis: ( x in { (rng g) where g is Element of D : verum } implies x c= Y )
assume x in { (rng g) where g is Element of D : verum } ; :: thesis: x c= Y
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: verum

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: verum

end;

suppose A6: B = {} ; :: thesis: union B in PFuncs (X,Y)

{} is PartFunc of X,Y by RELSET_1:12;
hence union B in PFuncs (X,Y) by A6, PARTFUN1:45, ZFMISC_1:2; :: thesis: verum

end;

end;